AlphaProof, now in Nature: DeepMind's RL agent in Lean reaches IMO silver-medal level

2026-08-11

Published in Nature, DeepMind's AlphaProof is a 3B-parameter network that learns formal Lean proofs by RL over about 80M auto-formalized problems, scoring 28/42 (silver-medal level) at IMO 2024.

What problem this solves

LLMs write more math than ever, but a natural-language proof cannot be machine-checked, so correctness is a human judgment call and RL gets no clean signal. Formal languages like Lean verify proofs automatically, and RL is a mechanism for learning in a verifiable environment. The question this paper (published in Nature, November 2025) asks is whether the AlphaZero recipe of policy-value networks, self-play, and search transfers to formal mathematical proof at the olympiad level. The scorecard is the 2024 International Mathematical Olympiad (IMO): AlphaProof solved three of the five non-geometry problems, and with AlphaGeometry 2 taking the geometry problem, the combined system scored 4/6 and 28 points, in the silver-medal band and one point short of gold. It is the first AI system to reach medal level at the IMO.

Method

AlphaProof casts proving in Lean as a sequential RL problem it calls the Lean environment: the state is the current Lean tactic state (all hypotheses and open goals), an action is one tactic, each step costs reward negative one to encourage short proofs, and the agent maximizes cumulative return. The pieces:

• Proof network. A 3-billion-parameter encoder-decoder transformer. The encoder reads the tactic state; the decoder is the policy, generating K tactics in parallel; a value head estimates how many steps remain. Pretraining used about 300 billion tokens of code and math, followed by supervised fine-tuning on about 300,000 state-tactic pairs from human-authored Mathlib proofs.
• AlphaZero-style search. The policy-value network guides a PUCT tree through selection, expansion, and backpropagation. Unlike board games, formal proving is a single-player perfect-information game, so a single search never commits to an intermediate action; it runs until a proof is found or the budget is spent.
• Auto-formalization. A fine-tuned Gemini 1.5 Pro translates about 1 million natural-language problems into about 80 million Lean problems as the RL curriculum. Before IMO 2024 it reached 60% pass@1 on 50 IMO problems (algebra 81.3%, number theory 76.9%, combinatorics only 33.3%).
• Main RL loop. A central matchmaker hands problems to distributed actors, each randomly tasked to prove or disprove, and Lean-verified outcomes flow back to a learner that updates the network. The main loop used about 80,000 TPU-days.
• Test-time RL (TTRL). For the hardest problems, more search is not enough. TTRL has Gemini generate a set of variants of the target problem (simpler cases, analogues), then runs a focused RL pass on the original plus its variants. Several IMO 2024 problems were ground out this way over days of compute.

Results

State-of-the-art across the formal benchmarks (miniF2F, formal-imo, PutnamBench-test), competitive even at just 2 TPU-minutes of search per problem and especially strong on PutnamBench-test. formal-imo is a newly curated set of 258 non-geometry historical IMO problems (107 algebra, 77 combinatorics, 74 number theory). The IMO 2024 breakdown:

The total is 4/6 and 28/42, silver-medal band, one point below the gold line. Two caveats matter: the model was frozen before the competition and the proofs were scored by independent experts under official rules, so this is not self-grading; and each AlphaProof problem took days of compute, far beyond a human contestant's 4.5 hours. For answer-style problems the system generated k=500 candidate answers, hit the correct one in every applicable case, and AlphaProof filtered them in a low-compute refutation mode.

Why it matters

This is the first AI system to score at medal level at the IMO, and it shows that learning from grounded, verifiable self-experience generalizes from games to mathematical reasoning. For practitioners, the real signal is that formal languages give RL a clean 0/1 truth reward, sidestepping the old problem that natural-language proofs cannot be auto-judged; TTRL is a concrete recipe that trades compute for per-problem depth, using variants plus specialized training to crack problems a general model cannot. The article is open access (CC BY 4.0), and the corrected miniF2F and the formal-imo benchmark are released.

Limitations

The authors are candid. The compute floor is enormous: about 80,000 TPU-days for the main loop and about 100,000 TPU-days for auto-formalization, a scale that puts the bespoke learning phase out of reach for most academic groups. TTRL takes days of inference per hard problem, so speed is a real constraint. The capability is also bounded: results sit within advanced high-school and undergraduate competition math on a fixed, known concept library with thematic consistency, and generalizing to open research-level math is a considerable next step. Geometry could not even be stated in Lean at the time because of gaps in Mathlib's higher-level geometry library (incircles, congruence), so it went to the separate AlphaGeometry 2. Finally, auto-formalization is the foundation of the whole pipeline, and its 33.3% pass@1 on combinatorics means that error directly caps what can be proved.

Terms

• Lean / Mathlib: Lean is an interactive formal proof language; Mathlib is its community math library of definitions, theorems, and high-level tactics.
• Tactic: a Lean instruction that advances a proof; AlphaProof treats each tactic as one action.
• Formalization: translating a natural-language statement into machine-checkable formal language.
• TTRL (test-time RL): generate variants of a single hard problem, then run a focused RL pass on the original plus variants.
• AlphaZero recipe: policy-value network plus Monte Carlo tree search learning from self-play, first used for Go and chess.
• IMO: the International Mathematical Olympiad, the top high-school math competition, six problems and 42 points max.

Source

• Paper

What people are saying

• AI Excels at Tuning but Fails at Novel Discovery: MLS-Bench Exposes Auto-Research Bottlenecks 青稞AI

All paper explainers