DeepMind's AlphaProof Nexus solves nine Erdős problems Google

Google DeepMind's AlphaProof Nexus solved 9 of the 353 open Erdős problems it tried. Two of them had been open for 56 years. Every proof is checked step by step in the Lean proof language. The paper appeared in Science on October 8, 2026.

The system also proved 44 of 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS), solved two open problems in algebraic geometry, and pinned down the exact convergence rate of an algorithm for min-max optimization.

How it works

• Gemini writes, Lean checks. Gemini 3.1 Pro writes a proof in Lean. After each attempt Lean checks it, and its error message guides the next attempt.
• AlphaProof for hard parts. In the full system, DeepMind's AlphaProof prover fills in missing steps the language model could not finish.
• The simple version was enough. The basic setup, Gemini plus Lean feedback only, also solved all 9 Erdős problems. It cost more on the hardest ones.
• Cost. The full system needed a few hundred dollars of computing per problem.

The results

The proofs are public on GitHub.

Sources

• Science: Advancing mathematics research with AI-driven formal proof search
• arXiv preprint (same paper)
• The proofs on GitHub