Primary evidence
- Advancing Mathematics Research with AI-Driven Formal Proof SearchS1 · Primary research · Paper · 2026-05-21
- AlphaProof Nexus ResultsS1 · Primary research · Formal artifact
AlphaProof Nexus scales Lean-based agents to hundreds of open research problems
AlphaProof Nexus organized frontier LLM subagents around the Lean compiler and escalated proof search with specialized tools and evolutionary search.
What happened?
The paper reported that the most capable AlphaProof Nexus agent autonomously resolved 9 of 353 open Erdős problems and proved 44 of 492 OEIS conjectures, while also contributing to research problems in algebraic geometry, optimization, graph theory and quantum optics.
AlphaProof Nexus organized frontier LLM subagents around the Lean compiler and escalated proof search with specialized tools and evolutionary search. The project released Lean proofs for successful Erdős, OEIS and research-collaboration cases together with human-readable proof writeups for selected results.
Why it matters
The scale and open-problem setting changed the evidentiary standard for formal AI4Math: generated research claims could be paired directly with kernel-checkable proof artifacts rather than only prose reasoning or benchmark scores.
Significance rationale: AlphaProof Nexus was reported as the first large-scale evaluation of LLM-driven formal proof search on open research problems, moving Lean-based agents from benchmark theorems to hundreds of active mathematical conjectures with public proof artifacts.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- New result
- Interface
- Formal, Symbolic, Hybrid
- AI contribution
- LLM agents generated and revised Lean proofs using compiler feedback and search; accepted formal proofs were mechanically checked, while researchers curated problems and assessed their research interpretation.
- Human contribution
- Researchers designed the agent hierarchy and search methods, formalized or curated open problems, supplied domain context in collaborative deployments, and analyzed whether formal solutions matched the intended mathematical questions.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- alphaproof-nexus, lean, gemini
- Organizations
- google-deepmind, university-of-texas-at-austin
- Problems
- erdos-problems, oeis-conjectures, research-mathematics
- Methods
- formal-proof-search, llm-agents, compiler-feedback, evolutionary-search, lean
Sources & artifacts
- Advancing Mathematics Research with AI-Driven Formal Proof SearchS1 · Primary research · Paper · accessed 2026-09-10
- AlphaProof Nexus ResultsS1 · Primary research · Formal artifact · accessed 2026-09-10
- AlphaProof Nexus generated Lean proofsArtifact · Proof artifact
Verification history
- 2026-05-21 · Paper released · E2 · Research record
The preprint reported the open-problem evaluation and research deployments.
- 2026-05-21 · Paper released · E3 · Inspectable artifact
Google DeepMind released a repository of generated Lean proofs and natural-language writeups, with instructions for rebuilding the formal artifacts.
Corrections
No corrections recorded.