The Pulse
Google DeepMind’s AlphaProof Nexus Proves 53 Open Math Problems
Google DeepMind’s AlphaProof Nexus proved nine open Erdős problems and 44 OEIS conjectures using AI-generated proofs checked by Lean. A paper published in Science on October 8 describes the system’s results and the limits of its evaluation.
AI.info Team · Written with AI ·
Google DeepMind’s AlphaProof Nexus proved nine open Erdős problems and 44 conjectures from the Online Encyclopedia of Integer Sequences, according to a paper published in Science on October 8. Two of the Erdős problems had remained open for 56 years. The results span formal proof search in number theory and other areas of mathematics, but they come from targeted tests—not a machine that can solve arbitrary research problems.
53 results across two problem sets
The researchers tested AlphaProof Nexus on 353 formalized Erdős problems, a subset of the more than 1,200 problems associated with mathematician Paul Erdős and his collaborators. The system proved nine. It also established 44 of 492 open conjectures drawn from the Online Encyclopedia of Integer Sequences, a database of integer sequences and related mathematical conjectures.
The paper reports additional work on a question about Hilbert functions in algebraic geometry and an open bound in convex optimization. The system found a parameter schedule that improved the bound. The team also used it in ongoing research involving combinatorics, graph theory and quantum optics; those efforts are distinct from the reported autonomous results on the Erdős and OEIS test sets.
Lean checks every proof step
AlphaProof Nexus has language-model agents propose edits to a theorem’s proof, then uses the Lean compiler to check whether the formal argument holds. If the code fails to compile, the system can use Lean’s error messages to revise its attempt. The paper describes a basic setup with independent proof-search agents and a more elaborate version that combines an evolutionary search with AlphaProof, DeepMind’s specialized theorem-proving system.
The full system’s proof-generating agents use Gemini 3.1 Pro; other agents rank candidate proof sketches using Gemini 3.0 Flash. The compiler’s check establishes that the submitted proof follows from the formal statement encoded in Lean. It does not, by itself, establish that the formal statement accurately captures the original mathematical question: the researchers say team experts checked that correspondence for each successful Erdős result.
“These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.”
George Tsoukalas et al., “Advancing Mathematics Research with AI-Driven Formal Proof Search”
The 353-problem test has limits
The headline results cover problems the team could express in Lean and give the system to attempt. For the Erdős set, the run stopped after 3,000 episodes if no proof emerged. That means nine successes out of 353 attempts, not a general measure of how well AlphaProof Nexus handles every open question in mathematics.
Cost also needs context. The authors estimate an inference cost of a few hundred dollars per solved Erdős problem, but say that figure does not include the full expense of running the system across all 353 problems to identify tractable ones. They report substantial variation in cost between problems and describe the system’s search as stochastic, so the per-solution estimate is not a fixed price for producing a proof.
Proof files are available to inspect
Google DeepMind has made the Lean proofs public in a GitHub repository, alongside natural-language proofs for selected results. The repository separates outputs for Erdős problems, OEIS conjectures and research collaborations in fields including algebraic geometry and optimization. Readers with Lean installed can build the project and check the formal proofs themselves.
The paper’s advance is not simply the count of problems solved. It pairs language-model proof generation with a formal checker and reports what that combination accomplished on defined collections of conjectures—with expert checks on the translation of successful Erdős statements. Those boundaries are as concrete as the result: nine proofs from 353 attempted Erdős problems, with the files available for inspection.