Google DeepMind has presented research results showing its research agent, AlphaProof Nexus, capable of solving not just Olympiad problems, but open research-level mathematical challenges. The system solved 9 out of 353 open problems associated with the Hungarian mathematician Paul Erdős, with two of them remaining unsolved for 56 years. In addition, the agent proved 44 out of 492 open conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS). According to the authors, computing costs for each solved Erdős problem amounted to a few hundred dollars.
Nine Erdős Problems and 44 OEIS Conjectures
The work focuses on using large language models to find formal proofs. The authors deliberately went beyond standard competition tasks and tested the approach on genuinely open problems that mathematics has struggled with for years. Success in 9 Erdős problems and 44 OEIS conjectures demonstrates that the approach is suitable for exploratory mathematics, rather than just educational and competitive examples. Importantly, the agent failed to solve most open Erdős problems: current successes are concentrated in areas with an existing developed library of formalized results where complex reasoning can be broken down into separate subproblems.
Formal Verification Instead of a Convincing Explanation
The key difference between AlphaProof Nexus and a regular chatbot is its use of Lean, a language and environment for formalizing mathematical proofs. The AI proposes a proof in formal format, after which Lean checks every logical step. If the check detects an error, the agent receives feedback and continues the search. A convincingly written explanation is not enough: the result must pass machine verification according to strict logical rules. It is this "generation-verification-correction" loop that makes the process suitable for real mathematics rather than generating plausible text.
Architecture: Multiple Agents and an Evolutionary Algorithm
In AlphaProof Nexus, multiple AI agents search for solutions, verify approaches, and refine proofs in parallel. In the most complex configuration, their work is coordinated by an evolutionary algorithm, while AlphaProof—an automated theorem-proving system developed by Google DeepMind and based on reinforcement learning—is used for specific search stages. This multi-agent architecture allows the search to be distributed across different strategies and select the most promising proof branches.
A Simple Agent Succeeded Too — But at a Higher Cost
The authors separately compared the complex architecture with a simpler agent that simply alternates proof generation by the language model with verification in Lean. Upon re-analyzing the nine solved Erdős problems, the simpler agent also succeeded in all nine. However, on the most difficult problems, its use was more expensive. This indicates that the outcome depends not only on the capabilities of the language model itself, but also on the organization of the proof search: the complex architecture saves computation on difficult cases.
Horizons and Limits
The system's capabilities are not limited to Erdős problems and OEIS conjectures. AlphaProof Nexus helped solve an open problem in algebraic geometry, improve bounds in convex optimization, and detect errors in the formalization of mathematical statements found in scientific literature. It is also used in graph theory and quantum optics research. At the same time, the system inherits the limitations of language models: search results can vary wildly from attempt to attempt, and problems requiring the development of extensive new theory remain beyond its capabilities. The authors believe that formal proofs can become a way to integrate AI into genuine mathematical work rather than just getting answers from it.
