Google DeepMind has an AI agent that solved nine open problems associated with Paul Erdős, and two of them had been sitting unsolved for 56 years. The more interesting part is not the headline but the fine print: the authors also report what the system could not do, and a cheaper, simpler agent turned out to be nearly as capable.
The numbers
The system is called AlphaProof Nexus. It was tested against 353 open problems linked to the Hungarian mathematician Erdős and cracked 9 of them, roughly 2.5 percent. It was also pointed at 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS) and proved 44, just under 9 percent.
The bill is part of the story. Each solved Erdős problem cost several hundred dollars of compute. That is not nothing, but it is less than a week of a research seminar's coffee budget, and considerably less than 56 years of mathematicians failing to notice a proof.
| Benchmark | Open problems | Solved |
|---|---|---|
| Erdős problems | 353 | 9 (two open for 56 years) |
| OEIS conjectures | 492 | 44 |
Why Lean changes the conversation
Anyone who has asked a chatbot for a proof knows the failure mode. The answer sounds wonderful, reads fluently, and is wrong in step four. Persuasive prose is the one thing language models produce at no cost.
AlphaProof Nexus sidesteps this by working in Lean, a language and environment for formalizing mathematical proofs. The model writes a proof in formal form, and Lean checks every logical step. If something fails, the agent gets the error as feedback and keeps searching. A nicely worded explanation earns no credit. Only a proof that survives machine verification counts.
This is the real contribution of the work. The paper's authors set out to test whether LLM-driven formal proof search could handle open research problems and not just olympiad exercises. For nine Erdős problems and 44 OEIS conjectures, the answer was yes.
How the machine is organized
Nexus is not a single model answering a single prompt. Several AI agents work in parallel, trying approaches, checking them, and refining proofs. In the most elaborate version, an evolutionary algorithm coordinates the whole effort. Certain stages of the search call on AlphaProof, DeepMind's reinforcement-learning-based automated theorem prover.
It sounds like a lot of machinery, so the authors did the sensible thing and asked whether it was necessary.
The inconvenient control experiment
They compared the full architecture against a much plainer agent, one that simply alternates between a language model generating proofs and Lean checking them. When they went back over the nine solved Erdős problems, the simple agent solved all nine as well.
The elaborate system did not win on capability here. Its edge showed up on the hardest problems, where the simple agent cost more to run. So the fancy orchestration bought efficiency, not new reach, at least on this set.
The authors draw a modest but useful conclusion. Results depend not only on how strong the underlying language model is, but also on how the proof search is organized. Put differently, a clever process around the model matters, and it is cheaper to find that out by experiment than by press release.
Beyond Erdős and OEIS
The system has been used outside those two benchmarks. According to the report, it:
- Helped solve an open problem in algebraic geometry.
- Improved a bound in convex optimization.
- Found errors in how mathematical statements from the published literature had been formalized.
- Is being applied in research on graph theory and quantum optics.
The third item deserves a second look. Formalization is the act of translating a human-written statement into Lean, and mistakes there are easy to make and easy to miss. A tool that catches them is useful even on days when it proves nothing new.
What it cannot do
The authors are direct about the limits, which is refreshing in a field where limits are usually left to the footnotes.
- Most problems remain open. Of the 353 Erdős problems, 344 were not solved.
- Success is clustered. The wins come in areas that already have a well-developed library of formalized results, and where hard reasoning can be broken into separate subproblems.
- Results are noisy. Like the language models underneath, the system can vary a great deal from one attempt to the next.
- Big new theory is out of reach. Problems that require building out an extensive new body of theory are beyond it for now.
That second point is the one to remember. Lean can only check what it can express, and it can only help find proofs where enough formal groundwork already exists. The system is strongest where mathematicians have already done the tedious job of writing things down in a machine-readable way. Credit where due, then, to the humans who formalized the libraries.
What the authors take from it
The authors' view is that formal proofs could be a way to bring AI into real mathematical work, rather than treating it as a machine that hands over answers to be trusted or doubted. Verification is what makes that possible. A mathematician does not need to trust the model, only Lean.
That is a more grown-up relationship than the usual one with AI output, where the reader is asked to admire the answer and hope for the best.
The takeaway
Nine solved problems out of 353 will not satisfy anyone hoping for a mathematical revolution by Tuesday. But two of those nine had resisted humans for 56 years, every proof was machine-checked, and the price tag was in the hundreds of dollars. The lesson that a plain loop of generate-and-verify matched the elaborate system on the solved set may end up being the most useful result of all. In mathematics, as in most things, the expensive-looking architecture is sometimes just the more expensive way to get the same answer.