A new large language model (LLM)-based artificial intelligence framework called AlphaProof Nexus can autonomously tackle select math problems, seeking proofs and using verification to ensure the resulting solutions are logically sound, researchers report. The system solved dozens of previously open problems across several mathematical fields, suggesting that artificial intelligence (AI) could become a useful tool for automated mathematical discovery and research. “[The authors report] that even unsuccessful proof attempts by AI could help them understand the problems better and make progress on solving them,” write Jeremy Avigad and Matthew Ballard in a related Perspective. “This underscores that an essential goal of developing AI for mathematics is to support mathematicians in the search for knowledge and understanding that lead to further advances.” Large language models (LLMs) have demonstrated growing ability to solve difficult mathematical problems, but their tendency to produce subtle logical errors or “hallucinations” makes them unreliable for research without extensive human expert review. One promising way to mitigate these issues is to have AI agents generate mathematical proofs in formal programming languages such as Lean, which automatically verifies each logical step and prevents errors from going unnoticed. While this approach has been successfully applied to competition mathematics and in the human-aided formalization of natural language arguments, its potential in solving open research-level mathematical problems remains unknown.
To address this gap, George Tsoukalas and colleagues developed AlphaProof Nexus, a framework that uses multiple AI agents to search for mathematical proofs with feedback from the Lean compiler. Tsoukalas et al. also developed a more advanced, full-featured agent that coordinated subagents through an evolutionary algorithm to use AlphaProof as a specialized proof tool. In tests, the system was able to solve nine of the 353 attempted Erdős problems, including two that had remained unsolved for more than 50 years. It was also able to solve 44 of 492 open On-Line Encyclopedia of Integer Sequences (OEIS) conjectures as well as several other research-level problems in fields such as algebraic geometry, optimization, quantum optics, and graph theory.
