colin7snyder

I don't disagree with you zingar. I think Erdős problems are great for testing a system's capability on genuinely hard math, which has value as a benchmark in itself, and maybe as a stepping stone toward more real-world impact. Your sentiment is well put.

To answer your question directly: most Erdős problems don't have practical applications on their own; the value is the techniques and the machine-checked proofs they leave behind. But there's more real world value in solving some of the FrontierMath Open Problems or Millennium Problems. There's a Venn diagram of "hard problems" and "real world impact" for sure.

Thank you for bringing this up pfdietz. No, not defective. The Lean proofs behind both are machine-checked and unchanged. I withdrew them over framing, not correctness.

1) For #129 a couple people pointed out that the report was very confusing. And I agree. So I'm currently attempting to improve it.

2) For #130, a person pointed it out as being a partial solution. This seems correct, so I'm currently working on making it fully end to end.

These are put out as "proposed solutions" for the mathematics community to scrutinize, and the scrutiny worked exactly like it should. Happy to take any feedback and make them better.

thank you very much for catching this. just fixed

I haven't come across this before. I will spend time on comparator. thank you very much for the suggestion.

Thank you for the questions echelon.

1) As far as the AI models go, we used GPT 5.6 Sol, Fable 5, and Gemini-2-embeddings across the system

2) Yes, the agents are given bash tools that allows them to interact with the preinstalled mathematics packages/dependencies that are on the VMs

3) This was a setup as a relatively quick project without much thought for future contributions, I will spend some time thinking about how i could make it more open.

I haven't played around with Aristotle at all, thanks for bringing it up & (also your codebase, thesisus, is very solid!)

apologies, bad wording/explanation. As addressed in another comment: "Poor wording on my end, thanks for flagging. I pull the OAuth refresh token from each Codex account into a custom broker, which mints short-lived access tokens per request and load-balances across the pool."

yeah, im currently running the system on navier-stokes (making real progress).

Unfortunately P vs NP, on the other hand, is going to have to wait for GPT 7

Poor wording on my end, thanks for flagging. I pull the OAuth refresh token from each Codex account into a custom broker, which mints short-lived access tokens per request and load-balances across the pool.

Thank you for the kind words! I agree, it's exciting that we can now build advanced AI systems for solving novel math (but i still love pen & paper too)

This is great feedback (thank you for taking the time), & you especially bring up a fair point on the writeups needing to be more human readable. I'll work on that

This is a self funded weekend project for me. It's not associated with any employer (: