AlphaProof: olympiad-level formal mathematical reasoning with reinforcement learning

An AlphaZero-inspired reinforcement-learning agent that learns to find formal proofs in Lean by training on millions of auto-formalized problems. At IMO 2024, as the core reasoning engine of Google DeepMind's system, it solved three of the five non-geometry problems; combined with AlphaGeometry 2 this reached a silver-medal-equivalent score.

L3Multi-step tool-using agentic workflow Source Peer-reviewed source Outcome Machine-verified artifacts

Evidence & verification

Source level

Peer-reviewed source
Grounded in a peer-reviewed publication. This describes the source; it does not mean the reported results have been independently reproduced.

Outcome verification

Machine-verified artifacts
Key artifacts (for example, formal proofs) were checked mechanically by a proof checker. Higher-level performance claims remain author-reported.

Sources checked

2026-10-15 (UTC)

Peer-reviewed in Nature (Hubert et al., published online 2025-11-12, DOI 10.1038/s41586-025-09833-y, resolved 2026-10-15). Proofs are formalized in Lean, so they are checked by an independent proof checker; the medal-level performance framing and competition results remain the authors' reported evaluation.

Source-checked does not mean independently reproduced. See the Method page for how these labels are assigned.

Sources (1)

Workflow & human oversight

Multi-step proof search uses Lean feedback and problem-specific adaptation. Humans supply formalized objectives and evaluate relevance. Iteration inside a bounded proof task is not, alone, end-to-end autonomous research.

Workflow level is not an evidence score; higher is not better evidence.

Problem

AI systems for mathematics often lack the formal verification needed to guarantee correctness, and human training data is a bottleneck. Formal environments such as Lean provide grounded feedback, but finding proofs in them is search over enormous spaces.

Approach

AlphaProof learns by reinforcement learning inside Lean against millions of auto-formalized problems. For the hardest problems it uses test-time reinforcement learning: generating and learning from millions of related problem variants at inference time for problem-specific adaptation.

Outcomes (as reported by the originating team)

The authors report that at the 2024 International Mathematical Olympiad the combined system solved three of the five non-geometry problems, including the competition's most difficult problem, reaching a score equivalent to a silver medallist with multi-day computation - the first medal-level AI performance claimed to the authors' knowledge (Hubert et al., Nature, 2026).

Limitations

Requires multi-day compute for competition-level problems and a Lean formalization step for the problem statement. Reported competition performance is an author evaluation; broader mathematical utility beyond olympiad-style problems is not established. Not independently reproduced.

Reproducibility

The publication describes the method; no public code release was verified at source-check time (the repository located during checking returned 404). Reproducing the result would require substantial compute and Lean tooling.

Adoption requirements

Lean 4 environment and auto-formalization tooling; very large compute budgets for training and inference; skills at the intersection of proof engineering and reinforcement learning. Practical today mostly for groups studying automated reasoning.

Comments

No comments yet.

Add a comment

Comments are held for moderation before appearing. Critical or corrective comments are welcome — especially evidence that an entry overstates what has been verified.