Second, the proofs -- I understand the Lean 4 proofs to be refereed by Fable, and generated by Chat 5.6 Sol. Unlike the leaked proof of the Cycle Double Cover Conjecture last week which had a very nicely readable nearly humanlike writeup, the proof summaries (from Fable) read like Claude tends to read to me these days - real difficulty with the theory of mind of the reader, they are filled with technical phrases, acknowledgment of hard bits and oblique reference to solutions. In short, they suck. I didn't see the word load-bearing, but I bet it's there.
That said, a Lean 4 proof is a pretty compelling output artifact. I find it interesting that it's an additional type of effort to turn these into human readable / appreciable / beautiful / non-shitty proofs.
To those who say who cares -- indeed. But. One of the major reasons things like the Erdos problems are valuable is that they can at times spur new techniques and concepts. The best of these concepts are applied elsewhere, advancing the frontier. While we gain a lot from solving these problems, we'll gain even more from that next step of distillation / explanation into something humans and computers can grok together. I'd hope that with so many tentatively marked 'solved' we will see some new techniques / ontology / concepts. If not, still pretty amazing.
Are you running tool calls that include inference with local fine tunes? And fast math packages? Controlled by the frontier model agents?
Is there a way folks can contribute to this?
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 that.
I also had this sort of thoughts when finishing my master's degree. I guess what breaks the cycle is that proofs (like other artefacts in other human activities) deliver aesthetic bliss.
I still like doing maths by pen and paper, but this is fun too.
What was really interesting is that during the process it was able to find lemmas or theorems that might be related or relevant to be published.
While I was doing that I was also trying to use Aristotle to do the Lean formalization and I have a WIP system to do that at https://github.com/aconsapart/thesisus/
"He is currently CTO at Xinobi AI, a Japan-based startup developing personal AI agents."
How many of these are you paying for out of pocket??
If you built yourself out of used parts you could do it for under a grand back then too.
(Or millions of disconnected stakeholders with different incentives collectively built modern civilization, but who wants to put that on a bumper sticker)
GPT-5.6 is a closed source model and this seems to be a personal project and not something done by OpenAI.
Unfortunately P vs NP, on the other hand, is going to have to wait for GPT 7
If it were really just about funding people who like math to have fun then it's easy to do forever: just don't have them look at the results and keep paying.
Otherwise they’ll be the ones like Erdős who pose the questions in the first place.
Either way it will always be humans who decide what matters. AI is speaking our languages, not the other way around. We’re in charge. It’s impossible for us not to be, unless we can train an AI from dolphin data or other natural phenomenon.
The AIs intelligence is tuned to us and in 300 years we’ll need new training runs for the update from human zeitgeist language and the 2200 century famous mathematicians.
AI companies are accruing power by virtue of its knowledge and ability to do work. If endowed with agency, which seems likely at this rate, it is the AI itself that will be powerful. And we'll be in charge because AI is trained on human language? I can't fathom the logic behind this.
An automatic proof solver doesn't make mathematicians obsolete any more than the excel sheet made accountants obsolete.