Google DeepMind's AlphaProof Nexus Cracks 9 Math Problems Unsolved for 56 Years
Google DeepMind's AlphaProof Nexus autonomously cracks 9 open Erdős problems and 44 OEIS conjectures using LLMs paired with Lean formal verification, at just a few hundred dollars per problem.
PRO- Google DeepMind's AlphaProof Nexus autonomously solved 9 of 353 open Erdős problems, including two open since 1970, at a cost of a few hundred dollars per problem.
- The system proved 44 of 492 open OEIS conjectures, settled a 15-year-old algebraic geometry question, and improved a convex optimization convergence bound.
- It pairs Gemini 3.1 Pro with the Lean proof assistant — the LLM proposes proofs, Lean's compiler verifies every step, rejecting anything that doesn't compile.
- Four agent configurations range from a simple generate-compile-repair loop to a full evolutionary system with Elo-rated sketch populations and AlphaProof tool calls.
- Surprisingly, the basic agent replicated all 9 Erdős successes, suggesting the simple agentic loop is already a strong baseline as LLMs improve.
- All formal proofs are open-sourced on GitHub; the system is actively deployed in combinatorics, graph theory, algebraic geometry, and quantum optics research.
For 56 years, a problem posed by Paul Erdős and András Sárközy sat unsolved: does there exist an infinite set of positive integers satisfying a specific divisibility constraint while remaining dense enough to meet a precise growth condition? On May 21, 2026, a Google DeepMind AI agent resolved it autonomously, overnight, at an inference cost of a few hundred dollars. That problem was one of nine. Google DeepMind's AlphaProof Nexus, a system that fuses large language models with the Lean formal proof assistant, has autonomously cracked 9 out of 353 open Erdős problems and proved 44 out of 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS).
The hallucination problem, solved with a compiler
The core challenge with using LLMs for mathematics research has always been reliability. LLMs can produce plausible-sounding proofs that contain subtle logical errors, and verifying them requires expensive expert review. AlphaProof Nexus addresses AI hallucination by pairing an AI model's generative capacity with formal proof-checking through the Lean proof assistant. The AI proposes a proof, and then a separate verification system checks every logical step. If the proof doesn't hold up, it gets rejected.
Lean is a proof assistant where every definition, theorem, and proof step is mechanically verified code. The key primitive is the sorry tactic, which closes a pending goal without actually proving it. A proof is only complete when the compiler reaches a state with no pending goals and zero sorry placeholders. This binary pass/fail signal is what makes the system trustworthy: there's no partial credit, no "looks about right."
Four agents, one framework
AlphaProof Nexus is built around a spectrum of four agent configurations, each adding capabilities on top of the last:
- Basic agent (A): Multiple independent prover subagents run in parallel. Each runs a "Ralph loop" , a multi-turn LLM session (Gemini 3.1 Pro) where the model edits a Lean proof sketch using a search-and-replace tool, gets compiler feedback after each edit, and iterates. As soon as one subagent finds a valid proof, all others stop.
This story is for Pro members
You've reached the end of the free preview. Upgrade to AlphaSignal Pro to read the full article - and everything else behind the paywall.
Comments
