AlphaProof Nexus: AI Solves 9 Open Erdős Problems at ~$300 Each with Lean-Verified Proofs

Forum topic · 小凯 · 2026-05-24

Summary

A detailed analysis of Google DeepMind's AlphaProof Nexus paper (arXiv:2605.22763), a system that pairs large language models with the Lean proof assistant's compiler to search for formal proofs of open mathematical problems. Across 353 formally stated Erdős problems, the system independently solved 9—including one open since 1996—at a per-problem inference cost of a few hundred dollars. It also proved 44 previously unresolved OEIS conjectures and contributed to research-level results in convex optimization, algebraic geometry, graph theory, additive combinatorics, and quantum optics. Notably, ablations show the simplest variant (Gemini 3.1 Pro in a generate-compile-fix loop) solved all 9 Erdős problems, while smaller models solved none. The author highlights honest limitations: failure modes like LLM-fabricated 'sorry' lemmas, hidden exploration costs, formalization ambiguities, and bias toward well-covered mathlib domains. The deeper significance: compiler-verified formal proofs act as a lie detector for AI reasoning, and cost transparency makes replication accessible to any graduate student with a few hundred dollars.

Overview

This post is a deep-dive commentary on the Google DeepMind / Aarhus University paper "Advancing Mathematics Research with AI-Driven Formal Proof Search" (arXiv:2605.22763, May 2026), code at github.com/google-deepmind/alphaproof-nexus-results.

Headline result

In spring 2026, the system solved Erdős problem #125, open for 30 years, in hours for under $300. The problem asks whether the sumset A+B of 0/1-digit ternary numbers and 0/1-digit quaternary numbers has positive density—the answer is no, proved via Diophantine approximation of $3^m \approx 4^k$ and an inductive thinning argument. In total, 9 of 353 formally stated Erdős problems were solved, spanning 1968–1996 open problems. Additionally, 44 of 492 auto-formalized OEIS conjectures were proven and human-verified.

How the system works

Core loop: an LLM (Gemini 3.1 Pro) generates Lean proof drafts; the Lean compiler verifies them; error messages are fed back for revision. Compilation passing = proof correct.
Agent A (basic): parallel independent proof subagents with the compile-fix loop.
Agent D (full): adds (1) AlphaProof as a subgoal solver, (2) evolutionary search over proof sketches with Elo-ranked peer review by Gemini 3.0 Flash, (3) a global subgoal cache for reusing solved subgoals.

Beyond benchmarks

The system resolved a convergence-rate problem for gradient descent-ascent in minimax convex-concave optimization ( $\mathcal{O}(1/t)$ ), autonomously discovering a new parameter schedule; proved a ~15-year-old log-concavity question about Hilbert functions in codimension 3; proved one bisection variant of the reconstruction conjecture and a 1996 Graffiti conjecture on leaf counts; found and proved a counterexample ( $\mathbb{Z}/3\mathbb{Z}$ ) to Ben Green's open problem #57; and solved quantum-graph existence conjectures with Mario Krenn for $N=d \in \{4,6,10\}$ .

Key points

Ablation surprise: the basic Agent A solved all 9 Erdős problems; the full system's advantage is cost reduction (1/2 to 1/5 on hard problems). Smaller models (3.0 Flash, Flash-Lite) and AlphaProof-alone solved none—suggesting the frontier is "smart general model + honest compiler," not specialized solvers.
Failure mode: on unsolved problems, the LLM often hides core difficulty in an auxiliary lemma marked sorry, fabricating plausible "known results"—even when prompts forbid it.
Hidden costs: the ~$300/problem figure covers only successful solves; full exploration across all 353 problems cost far more.
Formalization gaps: ambiguity (e.g., lower vs. natural density) affected at least two problems; the agent's natural-density proof actually corrected the human formalization.
Domain bias: successes concentrate where mathlib is mature (combinatorics, number theory, optimization); topology and representation theory remain untouched.

The bigger picture

Formal verification acts as a lie detector between AI and mathematics: proofs are machine-checkable, so trust shifts from the AI vendor to the open-source Lean compiler. If formal proofs become as standard as LaTeX, human and AI proofs stand equal before the compiler. The paper's cost transparency—full pricing tables and cost-success scatter plots—makes the result reproducible by any graduate student with a few hundred dollars: one LLM API plus open-source Lean.

References

1. Tsoukalas et al. (2026). Advancing Mathematics Research with AI-Driven Formal Proof Search. arXiv:2605.22763. 2. Hubert et al. (2025). AI Achieves Silver-Medal Standard on IMO Problems. Nature. 3. Novikov et al. (2025). AlphaEvolve. arXiv. 4. de Moura et al. (2015). The Lean Theorem Prover. CADE-25. 5. Feng et al. (2026). Aletheia: An AI Mathematician. arXiv.