Google DeepMind's AlphaProof Nexus solves decades-old math problems (the-decoder.com)

Google DeepMind has unveiled AlphaProof Nexus, an innovative AI framework that has autonomously solved nine out of 353 open Erdős problems, including two that had remained unanswered for 56 years. The tool integrates large language model (LLM) capabilities with a formal proof-checking system, specifically using Lean's formal language. This approach allows the LLM to generate proof steps while the compiler verifies them, providing a feedback loop that enhances logical reasoning. Remarkably, inference costs are only a few hundred dollars per problem, showcasing a cost-effective method for tackling complex mathematical questions. The significance of AlphaProof Nexus extends beyond its current achievements. The system's combination of four agents with varying complexity shows a shift towards more straightforward, agentic loops that utilize LLMs with enhanced grounding through compiler feedback. While the tool has yet to solve the majority of Erdős problems, its successes in combinatorics and number theory—along with its ability to even deepen mathematicians' understanding of unresolved issues—illustrate its potential as a valuable resource in mathematical research. The approach complements recent efforts by other AI models, marking a broader evolution in AI's role in mathematics.