AlphaProof: Search and Self-Play for Formal Mathematics

Executive summary

Question	Answer
What is AlphaProof?	A Google DeepMind reinforcement-learning prover for formal mathematics, operating in the Lean theorem prover environment.
Core stack	Lean 4 + Mathlib, a 3B-parameter proof network, AlphaZero/Sampled MuZero-style tree search, Gemini-based autoformalization and variant generation, and Lean-kernel verification.
Main 2024 result	AlphaProof solved IMO 2024 Problems 1, 2, and 6; AlphaGeometry 2 solved Problem 4; Problems 3 and 5 were not solved.
Score	28/42, equivalent to a silver medal at IMO 2024, one point below the gold threshold of 29.
Main methodological claim	The important pattern is not “LLM writes proof,” but learned search + formal verifier + self-generated curriculum + test-time adaptation.
Main limitation	The recipe works where candidate reasoning traces can be cheaply and reliably checked. It does not by itself solve open-ended natural-language reasoning, theory formation, judgment, or domains without crisp verifiers.

AlphaProof matters because it pushes Formal Verification and Reinforcement Learning into a domain where correctness is unusually non-negotiable. A Lean proof either checks, or it does not. This changes the epistemology of AI reasoning: instead of trusting a model’s verbal confidence, the system produces an object that a small trusted kernel can verify. In the Nature paper published after the original blog announcement, DeepMind describes AlphaProof as an RL agent that discovers formal proofs by interacting with a verifiable Lean environment, with components for proof-state representation, tree search, autoformalization, main RL, and test-time reinforcement learning. (DeepMind Nature AlphaProof paper) Nature

The key point for an AI-engineering wiki is that AlphaProof is best read as part of a lineage: AlphaGo/AlphaZero showed that search plus self-play can master games; AlphaTensor and AlphaDev showed that single-player search in a formally scored environment can discover useful algorithms; AlphaProof shows that something similar can work for formal theorem proving when the environment is a proof assistant rather than a game board or assembly simulator. (AlphaZero Science paper, AlphaTensor Nature paper, AlphaDev Nature paper) Science+2Nature+2

Background: why formal mathematics changes the problem

Informal mathematical reasoning is easy for language models to imitate and hard for them to make reliable. A natural-language proof can contain a subtle gap, a quantifier error, an illicit use of a lemma, or a false “obvious” step. In Formal Mathematics, the statement and proof are expressed in a formal language such as Lean; the proof assistant checks whether the proof term really inhabits the theorem type. The AlphaProof paper emphasizes that Lean’s kernel verifies the generated proof term and that this transforms mathematics into an interactive, verifiable domain suitable for simulation, experimentation, and learning. (Lean 4 paper, Lean documentation) Nature

That distinction is central. AlphaProof is not merely “Gemini doing math.” It is a system where a model proposes actions in a proof environment; Lean executes or rejects those actions; tree search explores alternatives; verified proofs and disproofs become training data; and the system improves from its own successful interactions. The verifier is the anchor. Without it, reinforcement learning on mathematical text risks rewarding plausible explanations. With it, the reward can be grounded in actual proof validity.

Lean itself is well suited to this style because it supports both interactive proving and executable automation. The Mathlib library gives the prover access to a large corpus of formalized mathematics and tactics; DeepMind used Mathlib both as a library during proof search and as a supervised fine-tuning source, extracting about 300,000 state–tactic pairs from human-written proofs. (Mathlib paper) Nature

The architecture: a theorem prover recast as a single-player game

AlphaProof formulates theorem proving as a sequential decision problem. The state is the current Lean tactic state: hypotheses plus remaining goals. The action is a Lean tactic represented as text. The transition is Lean attempting to run that tactic and returning a new proof state, an error, or a completed proof. The episode ends when a full proof is found or a compute budget is exhausted. DeepMind used a reward of −1 per tactic, pushing the system toward shorter proof branches. Nature

This framing gives a direct analogy to AlphaZero, but with an important twist. Board games have a canonical starting distribution: the initial board. Formal theorem proving does not. Each theorem is a different starting state, and the space of possible theorems is enormous. AlphaProof therefore needed a curriculum of many formal statements rather than a single game generator. DeepMind’s solution was large-scale autoformalization: a Gemini-based model translated roughly one million informal math problems into about 80 million Lean problem statements, creating a vast training curriculum even when the formalizations did not perfectly preserve the original informal problem. Nature

Component map

Component	Role in AlphaProof	Why it matters
Lean environment	Executes tactics, updates proof states, verifies final proof terms.	Supplies the ground truth reward signal.
Proof network	A 3B-parameter encoder–decoder transformer with policy and value heads.	Suggests tactics and estimates proof-state difficulty.
Tree search	AlphaZero/Sampled MuZero-inspired search over Lean tactic states.	Converts local model suggestions into deeper proof exploration.
Autoformalizer	Gemini 1.5 Pro-based formalization model.	Converts natural-language problem sources into a large Lean curriculum.
Main RL loop	Distributed actors attempt proofs/disproofs; verified successes update the network.	Moves beyond imitation of Mathlib proofs.
Test-time RL	Generates target-specific variants and trains on them at inference time.	Enables problem-specific adaptation on hard problems.
Lean final check	Re-runs completed proof files through Lean.	Ensures final proof validity, modulo Lean’s trusted kernel and axioms.

The proof network is a 3-billion-parameter encoder–decoder transformer. The encoder reads the pretty-printed tactic state; the decoder acts as a policy by generating candidate tactics; and a value head estimates the expected return, interpreted roughly as how many steps remain to solve the current branch. During search, AlphaProof samples candidate tactics, runs them through Lean, discards invalid tactics, merges duplicates that lead to equivalent proof states, and backs up values through the search tree. Nature

Tree search is not a cosmetic add-on. In one-step proof generation, the model must emit a complete proof or next tactic and hope it works. In AlphaProof, the model proposes local continuations while search allocates compute to promising branches. For multi-goal Lean states, AlphaProof introduces AND nodes: if a tactic splits a theorem into several subgoals, the proof is complete only when all subgoals are solved. The search therefore prioritizes unresolved or difficult subgoals rather than treating the proof as a flat sequence. Nature

The final verification step is deliberately conservative. DeepMind reports that each proof or disproof undergoes a final independent Lean command-line check, and a custom command verifies that the proof relies only on the standard Lean axioms used in the work: propositional extensionality, global choice, and quotient soundness. This is the “verifier as judge” pattern in its purest form. Nature

Training: from imitation to self-generated proof experience

AlphaProof’s training pipeline has three major phases.

First, the proof network is pretrained on roughly 300 billion tokens of public code and mathematical text. This gives the model general facility with programming syntax, formal-looking expressions, and mathematical language. It is not yet a Lean prover.

Second, the network is supervised fine-tuned on Mathlib state–tactic pairs. This teaches Lean-specific tactic behavior: what a proof state looks like, what tactics are syntactically plausible, and what human-written formal proof steps often look like. DeepMind reports about 300,000 state–tactic pairs from Mathlib in this phase. Nature

Third, the main RL loop begins. A “matchmaker” assigns autoformalized problems and compute budgets to distributed actors. Actors use tree search guided by the current proof network to attempt proofs or disproofs. Lean-verified successes are stored; failed attempts are filtered out; the learner updates the policy and value heads from a replay buffer containing verified proof/disproof experience, with a fixed mixture of Mathlib SFT examples. Nature

This is why “self-play” is an approximate but useful phrase. In Go, self-play means the agent plays both sides of the same game and learns from the final outcome. In AlphaProof, there is no opponent and no universal initial state. The analogue is self-generated interaction with a verifier: the prover attempts many formal statements, receives grounded feedback from Lean, and trains on the verified traces it discovers. DeepMind explicitly notes this difference: proving lacks the single universal initial state of board games, so AlphaProof needs a vast and varied corpus of theorem statements as starting points. Nature

The computational scale was large. DeepMind reports that autoformalization required about 100,000 TPU days over the project, while the main RL loop was of similar order, about 80,000 TPU days. This matters for interpreting the result: AlphaProof is a proof of capability, not yet an easily reproducible academic baseline. Nature

Test-time reinforcement learning: learning around the target problem

The most distinctive part of AlphaProof is Test-Time Reinforcement Learning. Standard test-time scaling gives the prover more search compute on the target theorem. AlphaProof adds a second mechanism: generate many formal variants around the target problem, train on those variants, and then return to the original theorem with a more specialized policy.

DeepMind describes TTRL as a focused learning procedure using a problem-specific curriculum of variants. Gemini generates variants by emulating heuristics such as simplification, generalization, lemma proposal, analogy, and proof-step simulation; programmatic transformations add systematic local variations. These variants are checked for Lean syntax, filtered, and then used for additional RL. Nature

This is methodologically important because it blurs the boundary between inference and training. AlphaProof does not merely “think longer” at test time; for hard problems, it learns a small local mathematics around the problem. DeepMind reports that scaling tree search from 2 TPU minutes to 12 TPU hours improved solve rates by more than 10 absolute percentage points on formal-IMO and PutnamBench-test, while TTRL added another 15 absolute percentage points beyond 12 TPU-hour search on those benchmarks. Nature

A useful way to read TTRL is as machine-generated scratchwork under formal constraints. Human solvers try special cases, prove lemmas, simplify hypotheses, generalize the statement, and search for analogous problems. AlphaProof operationalizes some of those moves as formal variants, then uses Lean to turn them into verified learning signals.

IMO 2024: what exactly happened

The 65th IMO was held in Bath, United Kingdom, July 11–22, 2024. The official IMO site records 108 participating countries, 609 contestants, a maximum score of 42, and medal cutoffs of 29 for gold, 22 for silver, and 16 for bronze. IMO Official

DeepMind applied its combined system to the six IMO 2024 problems. AlphaProof handled the non-geometry problems in algebra, number theory, and combinatorics. AlphaGeometry 2 handled the dedicated geometry problem because, at the time, Mathlib’s planar geometry support made it impractical to state some IMO-style geometry problems in Lean. The five non-geometry problems were manually formalized into Lean by experts immediately after the problem release. Problems requiring an answer, such as “find all” questions, used candidate-answer generation from Gemini 1.5 Pro with Python tool use; AlphaProof then refuted most incorrect candidates and attempted full proofs for promising ones. Nature

The judging protocol matters. DeepMind’s blog says the solutions were scored under IMO point-awarding rules by Sir Timothy Gowers and Joseph Myers. The Nature paper states that AlphaProof’s formal proofs were first verified by the Lean kernel and then judged according to official IMO rules, with full points awarded for the solved problems. Google DeepMind

IMO 2024 performance table

IMO 2024 problem	Domain	System	Outcome	Notes
P1	Algebra	AlphaProof	Solved	Answer: α is an even integer.
P2	Number theory	AlphaProof	Solved	Answer: only (a, b) = (1, 1).
P3	Combinatorics	AlphaProof	Not solved	One of two unsolved combinatorics problems.
P4	Geometry	AlphaGeometry 2	Solved	Geometry handled outside Lean/AlphaProof.
P5	Combinatorics	AlphaProof	Not solved	Formalization itself was difficult; initial expert attempts were unsuccessful within the first day.
P6	Algebra / functional equation	AlphaProof	Solved	Hardest problem of the contest; solved by only five human contestants.

The solved problem pages are revealing. For P1, the DeepMind solution page gives the informal statement, the generated answer “α is an even integer,” and a rendered Lean proof with hand-inserted comments explaining the approach. For P2, the answer is (1, 1). For P6, the answer is c = 2, and the page shows the Lean theorem proving leastness of that value. (DeepMind IMO 2024 solution pages) Google Cloud Storage+2Google Cloud Storage+2

The result was 28/42: full marks on four solved problems, no marks on the two unsolved combinatorics problems. That score was within the 2024 silver-medal range and one point below the gold cutoff. DeepMind’s blog also notes that AlphaProof solved two algebra problems and one number theory problem, including the contest’s hardest problem, while AlphaGeometry 2 solved the geometry problem. Google DeepMind

The caveats are substantial. AlphaProof did not read the contest paper end-to-end and output natural-language proofs under human time constraints. The non-geometry problems were manually formalized into Lean; the formal proofs had to be translated back into judgeable mathematical arguments; and AlphaProof’s solutions required two to three days of TTRL per solved hard problem, far beyond the 4.5-hour session limits imposed on contestants. DeepMind’s own 2025 IMO writeup later contrasted this with Gemini Deep Think, noting that the 2024 AlphaProof/AlphaGeometry systems required expert translation into domain-specific languages and two to three days of computation. (Google DeepMind Gemini Deep Think IMO 2025 writeup) Google DeepMind

Relationship to AlphaGeometry

AlphaGeometry is the closest predecessor and sibling system. The original AlphaGeometry paper framed olympiad geometry as a neuro-symbolic problem: a neural language model proposes auxiliary constructions, while a symbolic deduction engine performs rule-bound geometric reasoning. It generated synthetic geometry data rather than relying on human proof demonstrations, solving 25 of 30 IMO-style geometry problems in the benchmark, compared with 10 for the previous state of the art, Wu’s method. (AlphaGeometry Nature paper) Nature

AlphaGeometry 2 strengthened that line. DeepMind’s 2024 blog says AlphaGeometry 2 used a Gemini-based language model trained from scratch on much more synthetic data, a symbolic engine two orders of magnitude faster than the predecessor, and a knowledge-sharing mechanism across search trees. Before IMO 2024, it could solve 83% of historical IMO geometry problems from the previous 25 years, compared with 53% for the predecessor; the later JMLR paper reports 84% across IMO 2000–2024 geometry problems and improved formal-language coverage from 66% to 88%. (AlphaGeometry 2 JMLR paper) Google DeepMind

AlphaProof and AlphaGeometry therefore occupy different points in the same design space.

Dimension	AlphaProof	AlphaGeometry / AlphaGeometry 2
Formal environment	Lean 4 + Mathlib	Specialized geometry language and symbolic engine
Main mathematical scope	Algebra, number theory, combinatorics, some non-classical geometry where Lean libraries suffice	Classical Euclidean olympiad geometry
Neural role	Generate Lean tactics and guide proof search	Generate auxiliary geometric constructions
Verifier	Lean kernel	Symbolic geometry engine / formalized geometric deduction pipeline
Training signal	Lean-verified proofs/disproofs	Synthetic geometry proofs and symbolic deduction outcomes
2024 IMO role	Solved P1, P2, P6	Solved P4

The relationship is not “AlphaProof replaces AlphaGeometry.” It is closer to: AlphaGeometry demonstrated the neuro-symbolic search pattern in a geometry-specific formalism; AlphaProof generalized the idea into Lean, where a much broader fragment of mathematics can be represented, at the cost of a much more complex proof-search problem.

Why the result is methodologically significant

The AlphaProof recipe can be compressed into four steps:

1. Put reasoning inside a formal environment.

2. Use a learned model to guide search through that environment.

3. Use the verifier as the reward signal.

4. Generate more verified experience than humans could label.

This is an instance of Verifier-Guided Learning. The verifier changes the learning problem from “imitate plausible reasoning” to “discover actions that compile into truth-preserving proof objects.” In domains where a verifier is available, the model’s failures are cheap data. Invalid tactics, dead-end searches, disproved candidates, and verified lemmas all become signals.

The broader DeepMind lineage is visible. AlphaZero learned from self-play in games where the rules are exact and outcomes are definite. AlphaTensor turned matrix multiplication into a single-player tensor-decomposition game with provably correct algorithm discovery. AlphaDev turned small assembly-program synthesis into a game where the reward combined correctness and speed, discovering sorting routines later integrated into LLVM libc++. AlphaProof moves this strategy into formal mathematics, where the “game state” is a proof state and the “win condition” is a Lean-checked proof. PubMed+2Nature+2

This is more general than Go, but not arbitrarily general. The hidden commonality is not games; it is closed-loop search with reliable evaluation. If a domain can be encoded as states, actions, and verifier-checked terminal conditions, then AlphaZero-like methods can become engines of discovery. Formal mathematics is unusually favorable because proof assistants provide exact feedback, theorem variants can be generated synthetically, and correctness does not depend on human taste once the theorem statement is fixed.

The methodological contribution is therefore conditional: AlphaProof shows that RL plus search can scale in a rich symbolic domain when there is a powerful verifier and enough synthetic problem generation. It does not show that ordinary natural-language reasoning, philosophical judgment, legal interpretation, scientific taste, or strategic planning have been solved by the same recipe.

Position in the formal-math AI literature

AlphaProof sits on top of roughly a decade of neural theorem-proving work, and more than half a century of automated theorem proving. The immediate neural lineage includes GPT-f, miniF2F, PACT, LeanDojo/ReProver, expert-iteration systems, and newer Lean-prover models such as DeepSeek-Prover.

GPT-f showed that transformer language models could guide formal proof search in Metamath, even contributing new short proofs accepted into the Metamath library. MiniF2F created a cross-system benchmark of 488 olympiad-level formal problem statements targeting systems such as Metamath, Lean, Isabelle, and HOL Light. PACT attacked the data scarcity problem by extracting self-supervised tasks from kernel-level proof terms. LeanDojo emphasized reproducibility and premise selection, offering an open-source Lean playground, benchmarks, and the retrieval-augmented ReProver model. (GPT-f paper, miniF2F paper, PACT paper, LeanDojo paper) arXiv+3arXiv+3arXiv+3

Formal Mathematics Statement Curriculum Learning was especially close in spirit: it used expert iteration, meaning proof search interleaved with learning, and found that this outperformed proof search alone at fixed compute while creating curricula of increasingly difficult formal statements without ground-truth proofs. DeepSeek-Prover-V1.5, published at ICLR 2025, likewise used Lean feedback, online RL, and a Monte-Carlo-tree-search-like method to improve formal proof generation. (Formal Mathematics Statement Curriculum Learning, DeepSeek-Prover-V1.5) OpenReview

AlphaProof’s distinguishing features are scale, integration, and performance on a live IMO. It combined a large proof network, a huge autoformalized curriculum, distributed RL, specialized proof search, and TTRL. It also used a complete competition pipeline: answer generation, Lean formalization, refutation of wrong candidates, proof search, and expert judging. The achievement is not that no prior system used any of these ideas; it is that DeepMind assembled them at sufficient scale to solve live olympiad problems previously beyond automated systems.

What AlphaProof does not prove

AlphaProof’s limitations are not footnotes; they define the scope of the result.

First, formalization remains a bottleneck. IMO 2024’s non-geometry problems were manually formalized into Lean, and the geometry problem was handled by AlphaGeometry 2 because Mathlib’s geometry library did not yet make it practical to state the problem in Lean. DeepMind’s Nature paper notes that P5 was especially difficult to formalize, with initial expert attempts unsuccessful within the first day. Nature

Second, the system is expensive. The main RL and autoformalization phases consumed large TPU budgets, and the hardest IMO problems required multi-day TTRL. This is far from a lightweight assistant that a typical mathematician or academic lab can reproduce. DeepMind explicitly acknowledges that the bespoke learning phase is likely beyond most academic groups and that the multi-day inference time highlights the need for more efficient strategies. Nature

Third, AlphaProof is tuned for formal-math-shaped problems. IMO problems are hard, but they are also unusually well-posed: fixed statements, known background domains, crisp correctness criteria, and short final proofs relative to research mathematics. DeepMind itself says the current successes are primarily in advanced high-school and undergraduate competition mathematics, which operate within a known library of concepts and thematic regularity. Nature

Fourth, the system does not automatically perform theory building. Proving a stated theorem in Lean differs from deciding what definitions matter, what conjectures are interesting, what abstractions clarify a field, or which research direction has taste. AlphaProof can generate lemmas and variants around a target theorem, but that is not the same as expanding a mathematical theory in the way human researchers do.

Fifth, the system does not transfer automatically to open-ended reasoning. Many real-world domains lack Lean-like verifiers. In law, strategy, ethics, philosophy, product design, and empirical science, the “correct answer” is often underdetermined, value-laden, probabilistic, or dependent on future observations. A verifier can sometimes be engineered for subproblems—unit tests for code, simulations for physics, proof obligations for protocols—but the existence of a verifier is the exception, not the default.

Does the AlphaProof recipe generalize?

The honest answer is: partially, under strong conditions.

AlphaProof gives strong evidence for a general engineering pattern:

Condition	Why it matters	Domains where it plausibly applies
Crisp verifier	Prevents reward hacking by plausible text.	Formal proofs, code tests, hardware verification, some symbolic math.
Cheap environment interaction	Allows millions of attempts.	Theorem proving, programming contests, game-like design spaces.
Searchable action space	Lets policy + value + tree search improve over sampling alone.	Tactic proving, program synthesis, algorithm discovery.
Synthetic curriculum	Reduces dependence on human-labeled data.	Geometry, formal statements, generated programming tasks.
Variant generation	Supports test-time adaptation.	Math lemmas, code refactorings, constrained design.
Meaningful final object	Produces something independently checkable.	Proof term, executable program, circuit, algorithm.

Where those conditions hold, the AlphaProof recipe is powerful. In AI for Code, unit tests and formal specs can play a Lean-like role. In verified hardware or protocol design, proof obligations can create reward signals. In algorithm discovery, correctness tests plus performance metrics can guide search. In symbolic scientific modeling, simulators and conservation laws can sometimes act as partial verifiers.

Where those conditions fail, the recipe weakens. Open-ended research often needs problem formulation before proof. Engineering often involves ambiguous tradeoffs. Philosophy and ethics lack canonical formal reward functions. Even empirical science can only partially verify a hypothesis until experiments are run, and experimental feedback is slower, noisier, and more expensive than Lean checking.

So AlphaProof is not evidence that “self-play solves reasoning.” It is evidence that self-improvement becomes much more real when reasoning is embedded in a reliable environment. The general lesson is architectural: build agents around tools that can falsify them.

A compact mental model

AlphaProof can be summarized as:

Natural-language math corpus        ↓Gemini-based autoformalization        ↓Large Lean theorem curriculum        ↓Proof network + tree search interacts with Lean        ↓Lean-verified proofs/disproofs become training data        ↓Main RL improves general prover        ↓For hard targets: Gemini generates variants        ↓TTRL adapts prover to the target        ↓Lean checks final proof        ↓Human judges assess competition credit

The decisive feature is the loop. A static language model is bounded by its training distribution and its ability to sample plausible continuations. AlphaProof is instead an interactive system: it proposes, tests, searches, verifies, trains, and repeats. That is why the system belongs in the same conceptual family as AlphaZero, even though the environment is a proof assistant rather than a board game.

Selected sources

Companion entries

Core theory: Formal Mathematics, Lean 4, Mathlib, Automated Theorem Proving, Interactive Theorem Proving, Proof Assistants, Verifier-Guided Learning, Reinforcement Learning, AlphaZero, Monte Carlo Tree Search, Test-Time Reinforcement Learning

Systems and lineage: AlphaProof, AlphaGeometry, AlphaGeometry 2, AlphaGo, AlphaTensor, AlphaDev, Gemini, DeepSeek-Prover, LeanDojo, miniF2F, GPT-f

Engineering patterns: Self-Play, Synthetic Data Generation, Autoformalization, Search-Guided Generation, Policy-Value Networks, Tree Search for Program Synthesis, Formal Verification as Reward Signal, Tool-Augmented Reasoning

Practice: Using Lean for AI Reasoning, Designing Verifiable AI Environments, Building Proof-Search Agents, Evaluating Formal Theorem Provers, Test-Time Compute Scaling, Curriculum Learning for Reasoning Systems

Limitations and counterarguments: Formalization Bottleneck, Verifier Availability Problem, Reward Hacking in Formal Systems, Limits of Competition Math Benchmarks, Reasoning Versus Theory Building, Open-Ended Reasoning, AI Mathematical Taste