AlphaProof and AI-Assisted Theorem Proving

Why This Matters

In July 2024, Google DeepMind announced AlphaProof and AlphaGeometry 2: systems that reached a silver-medal-equivalent score at the 2024 International Mathematical Olympiad. Together they solved four of six problems and scored 28 of 42 points in DeepMind's official report. AlphaProof solved three of the five non-geometry problems in Lean; AlphaGeometry 2 solved the geometry problem.

This was the first reported medal-level AI result at the IMO, but it was not a standard human contest submission. Experts manually formalized the five non-geometry statements and the system used multi-day computation. The 2025 peer-reviewed report describes the result as evidence about formal-theorem-proving capability, not a like-for-like 4.5-hour human contest comparison.

This page covers AlphaProof and related 2024-25 results:

• The AlphaProof / AlphaGeometry 2 architecture.
• The autoformalization pipeline (LLM translates English → Lean 4).
• The reinforcement-learning theorem prover layer.
• The peer-reviewed AlphaProof methodology published in 2025.
• The distinction between AlphaProof's kernel-verified proofs and the separate natural-language IMO result reported in 2025.
• Prior work the line builds on (GPT-f, Polu-Sutskever 2020; LeanDojo / ReProver, Yang et al. 2023).
• Open problems and limitations as of 2026.

Formal theorem-proving systems

The pattern is consistent: every system in this table separates a fast, fallible proposer from a slow, sound verifier such as a Lean kernel, Coq kernel, custom DSL, or SMT solver. The proposer is trained to generate proof attempts; the verifier rejects anything that does not type-check. This is the AlphaZero pattern (Silver et al. 2018) lifted to mathematics: search, neural-network policy, and ground-truth verification.

The AlphaProof Architecture

DeepMind's peer-reviewed methodology was published in November 2025. It describes the following architecture:

1. Autoformalization layer (LLM). A specialized language model translates mathematical prose into a Lean statement. The training pipeline expanded roughly one million natural-language problems into about 80 million formal Lean problems. Correct Lean syntax is not the same as fidelity to the original problem, which is why statement review remains necessary.

2. Search layer (RL theorem prover). A 3-billion-parameter proof network guides a specialized AND-OR tree search over Lean tactic states. It learns from the formalized curriculum and Lean-verified search outcomes. For especially difficult targets, test-time reinforcement learning trains on generated variants of that target.

3. Verifier layer (Lean kernel). Every candidate proof is checked by Lean 4's kernel. If the proof type-checks, the problem is considered solved. No reliance on the model's confidence, kernel verification is the trust layer.

Proposition

Kernel-Verified Soundness Reduction

Statement

For an AlphaProof-style pipeline that emits a Lean term $t$ as a candidate proof of a theorem $T$, the soundness of the end-to-end system reduces to the soundness of the Lean 4 kernel. Concretely: if kernel.check t T returns true, then $T$ is a theorem of Lean's logic (under the imported environment); the AI components — autoformalizer, RL proposer, retrieval — are not in the trust base.

Intuition

The AI is a guesser; the kernel is the judge. A guess that fails to type-check is rejected and contributes nothing. A guess that type-checks is, by definition, a Lean proof of $T$. The AI's training process, biases, and even active deception cannot produce a wrong "proof" that the kernel accepts, because acceptance by the kernel is the definition of correctness. This is the same trust-base argument that makes Coq's small kernel design valuable: by minimizing the trusted code, you minimize what can go wrong.

Why It Matters

This is the architectural reason AlphaProof is qualitatively different from a chain-of-thought language model that emits "proofs" as English. Chain-of-thought proofs require human review for correctness; kernel-checked Lean proofs require human review only of the theorem statement. The autoformalization step is therefore the remaining trust hole: if the autoformalizer mistranslates "for all $n \geq 0$" as "for all $n \in \mathbb{Z}$," the kernel will happily verify the wrong theorem.

Failure Mode

Soundness fails if (a) the kernel itself has a bug, (b) an imported axiom is inconsistent (e.g., a buggy axiom declaration in user code), or (c) the autoformalized statement diverges from the human-intended statement. (a) and (b) are also failure modes for human Lean users; (c) is specific to the AI pipeline and is the active research frontier.

report a correction →

The 2024 result used multi-day computation per target. It demonstrates that a formal environment can supply a useful learning signal, but does not establish real-time interactive theorem proving.

The architectural pattern is the same as AlphaZero (Silver et al. 2018) applied to theorem proving: search + neural-network policy + ground-truth verifier. The kernel plays the role of the chess-rule verifier; the RL agent plays the role of MCTS-guided move selection.

2025 Benchmark Update

In 2025, Google DeepMind reported that an advanced version of Gemini Deep Think solved five IMO problems perfectly, scoring 35/42 within the 4.5-hour contest limit. The system produced natural-language proofs, so the result is distinct from AlphaProof's Lean-based pipeline and does not provide the kernel-verification guarantee of a formal proof.

The AlphaGeometry 2 Track

AlphaGeometry 2 is the geometry-specific system; it solved IMO 2024 Problem 4 (a synthetic-geometry problem about a triangle and its circumcircle). Its predecessor, AlphaGeometry (Trinh et al., Nature 2024), was IMO-bronze level on a held-out olympiad-geometry test set.

The architecture differs from AlphaProof:

• Symbolic engine. A custom geometry solver applies classical geometric construction rules (extending lines, drawing circles, etc.).
• LLM proposer. A language model proposes auxiliary constructions that guide the symbolic engine toward a solution.
• Synthetic training. Trained from 100M synthetic geometry problems generated programmatically; no human proofs needed.

This is a neuro-symbolic hybrid rather than a pure RL+kernel system. The symbolic engine plays the same role as Lean's kernel: a ground-truth verifier the LLM cannot fool. AlphaGeometry 2's improvements over the original include better synthetic data and a stronger LLM proposer.

Background: GPT-f and the LLM Theorem-Proving Line

The AlphaProof line builds on a decade of work on neural theorem proving:

• GPT-f (Polu and Sutskever, 2020): the first GPT-style Transformer trained on Metamath proofs. Showed that language models could generate proof scripts above chance, but performance was modest.
• Lean theorem proving with HOList (Bansal et al. 2019): early supervised learning on Coq + HOL.
• PACT (Han et al. 2022): co-training on autoformalization and theorem proving for Lean.
• HyperTree Proof Search (Lample et al. 2022): tree search on tactic sequences combined with LLM proposers.
• LeanDojo + ReProver (Yang et al., NeurIPS 2023): retrieval-augmented theorem prover; selects relevant Mathlib lemmas as context for the LLM. Open-source.
• Llemma (Azerbayev et al. 2024): a 7B / 34B parameter language model trained on math-heavy text + code, designed as a base for theorem-proving fine-tuning.

The published methodology attributes AlphaProof's advance to autoformalization-based synthetic data and reinforcement learning on the proof-search layer. It reports the system architecture, training data, and contest evaluation in detail.

Autoformalization

The bottleneck for AlphaProof and similar systems is getting the problem statement into Lean 4 in the first place. This is autoformalization, translating mathematical English into a formal statement in a proof assistant.

Definition

Autoformalization$\mathrm{AF}:\mathrm{ENG}\to \mathrm{LEAN}$

Autoformalization is the task of translating a natural-language mathematical statement (definition, lemma, theorem) into a syntactically valid term in a formal proof assistant such as Lean 4, Coq, or Isabelle/HOL. Concretely: given an English sentence such as "every continuous function on a compact metric space attains its maximum," produce the corresponding Lean 4 term, typically of the shape theorem extreme_value_theorem ... : ... := by ..., with the type signature filled in (proof body left as sorry for a downstream prover to complete). Modern pipelines also include an autoinformalization loop: translate Lean back to English and check semantic agreement. Autoformalization rates on undergraduate exercises were around 30-40% in 2022 (Wu et al.) and have climbed past 60% on definitions / 50% on theorem statements by 2025 with retrieval-augmented frontier models. Proofs remain unreliable.

The state of autoformalization in 2026:

• Granite-3-Mathlib (IBM, 2024): a fine-tuned Llama-2 70B model trained on Mathlib4 + retrieval. Reports 60-70% accuracy on autoformalizing real-analysis exercises.
• ByT5-Mathlib (Wu et al. 2022, updated through 2024): byte-level transformer for autoformalization with improved accuracy on definitions vs. theorems.
• Wu et al. 2022 ("Autoformalization with Large Language Models"): the foundational paper; showed Codex and PaLM could autoformalize undergraduate math at moderate rates.
• draft + verify pipelines: LLM produces a draft Lean statement; kernel + targeted retests verify it; human or another LLM corrects errors.

For now, autoformalization is reliable for definitions and basic theorem statements but unreliable for proofs. The AlphaProof pipeline succeeds because the proof-search component is the heavy lifter; the autoformalization just has to nail the statement.

What This Means for Mathematicians

Several practical consequences in 2026:

• Lean users can combine proof search, retrieval, and interactive assistance. Lean Copilot and related tools are useful aids, but their output still needs kernel checking and, for a natural-language task, statement review.

• Olympiad-level results now come from different technical routes. AlphaProof's 2024 score used formal statements and multi-day compute; Deep Think's 2025 score used natural-language proofs under the contest limit. The headline scores are not evidence that the two systems provide the same verification properties.

• Research formalization remains a separate test. Olympiad benchmarks are valuable, but they do not establish dependable performance on open-ended research mathematics.

• Neuro-symbolic systems beyond geometry. AlphaGeometry 2 does not establish comparable systems for combinatorics, number theory, or analysis. Extending the proposer-and-verifier pattern to those domains is a research direction; each needs an appropriate formal or symbolic substrate.

• Statement fidelity remains a human responsibility. A kernel can verify a mistranslated statement perfectly, so formalization quality remains part of mathematical review.

Limitations and Open Problems

Despite the IMO result, several practical limitations remain:

• Compute cost. The 2024 result used multi-day computation; it is not evidence of real-time interactive use.
• Formalization fidelity. Before the 2024 evaluation, the autoformalizer achieved 60% pass@1 on a 50-problem representative IMO set and 64% on a representative Putnam set in the peer-reviewed methodology. Those measurements do not justify a general reliability claim, and the official IMO evaluation used expert formalizations.
• Scope of evidence. The published evaluation covers formal competition benchmarks. It does not establish reliable performance on open-ended research mathematics.
• Human interpretability. Kernel validity establishes that a Lean statement follows in the imported environment; it does not establish that the formal statement matches a human request or that the proof is the most useful explanation.

The Path-Network Connection

For TheoremPath and the path-network domains:

• ProofsPath: AI-assisted theorem proving is the natural successor to traditional olympiad coaching. The craft of mathematical proof writing remains valuable; the AI becomes another collaborator at the proof.
• TheoremPath: ML theorems formalized in Lean 4 (via the formalizing-ml-theorems-in-lean-and-coq page) form the substrate that AlphaProof and similar systems can prove against.
• ComputationPath: the architecture of AlphaProof illustrates the RL on a verifiable substrate pattern that defines modern AI-for-math; it sits naturally in the computability + verification toolkit.
• DSAPath: tree search and retrieval are core algorithmic primitives that AlphaProof relies on.

Common Mistakes

Watch Out

Treating AlphaProof as a 'theorem-proving GPT'

AlphaProof is not just an LLM. It's an AlphaZero-style RL agent with the Lean kernel as the verifier. The LLM component (autoformalization, proposal generation) is necessary but not sufficient.

Watch Out

Confusing IMO performance with general theorem proving

IMO problems are short, well-specified, and have clean solutions. AlphaProof's success on IMO doesn't mean it can prove arbitrary research mathematics, those proofs are longer, more open-ended, and require domain-specific mathematical insight.

Watch Out

Assuming the Lean kernel can be tricked

The Lean kernel is the trust layer; AlphaProof cannot "convince" it of false claims. Any proof AlphaProof produces is a correct proof in Lean 4, the AI's job is to find the proof, not to be trusted about the proof.

Watch Out

Overestimating autoformalization reliability

For research-level statements, autoformalization is still unreliable. Robust pipelines combine LLM drafting with human review (or with a verifier loop that retries on type-checking failure). Pure LLM autoformalization is not production-ready.

Exercises

ExerciseCore

Problem

Why is the Lean kernel the trust boundary for AlphaProof, not the RL agent or the LLM?

Hint

Reveal Solution

ExerciseAdvanced

Problem

Sketch how an AlphaGeometry-style approach (LLM proposer + symbolic engine) might be adapted to combinatorial olympiad problems, where the symbolic substrate is less obvious.

Hint

Reveal Solution

Cross-Network Links

• TheoremPath: theorem-proving-in-lean is the foundational prerequisite. ML-theorem case studies, a Lean tactic cookbook, and a treatment of reasoning-data curation (reasoning-data-curation) are planned companion pages.
• ProofsPath (forthcoming, content/proofspath-topics/): olympiad technique pages cover the human-style techniques AlphaProof must learn (induction, pigeonhole, vieta jumping, invariants and monovariants, the extremal principle). The Lean 4 wrappers landing in TheoremPath via PRs #185-#188 are the bridge between the human craft and the AI prover.
• ComputationPath (parked): the architecture of AlphaProof is the canonical RL on a verifiable substrate pattern. Until ComputationPath ships, the relevant overview lives on TheoremPath at theorem-proving-in-lean.

References

Canonical:

• Hubert et al., "Olympiad-level formal mathematical reasoning with reinforcement learning". Nature 651, pp. 607-613 (2026). Published online November 12, 2025. Peer-reviewed AlphaProof methodology, including the 80M formal-problem curriculum and test-time RL.
• Google DeepMind. "AI achieves silver-medal standard solving International Mathematical Olympiad problems". Blog post, July 25, 2024. The original AlphaProof / AlphaGeometry 2 announcement.
• Google DeepMind. "Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad". Blog post, July 21, 2025. A distinct natural-language IMO result.
• Trinh, Wu, Le, He, Luong. "Solving olympiad geometry without human demonstrations." Nature 625 (2024) 476-482, doi link. The AlphaGeometry (predecessor) paper; describes the symbolic-engine + LLM-proposer architecture and the synthetic-data pipeline that AlphaGeometry 2 inherits.
• Polu and Sutskever. "Generative Language Modeling for Automated Theorem Proving." arXiv:2009.03393 (2020). GPT-f, the foundational paper for the LLM-as-proof-script-generator line.
• Silver et al. "A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play." Science 362 (2018), pp. 1140-1144. The AlphaZero paper; the AlphaProof RL-plus-verifier pattern is its direct descendant.

Current:

• Yang et al. "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models." NeurIPS 2023, project page. Open-source retrieval-augmented theorem prover; the public benchmark for LLM-driven Lean proving.
• Azerbayev et al. "Llemma: An Open Language Model for Mathematics." ICLR 2024, arXiv:2310.10631. 7B / 34B base model trained on Proof-Pile-2; the standard open-weight starting point for theorem-proving fine-tuning.
• Song et al. "Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean." arXiv:2404.12534 (2024). The Lean Copilot tactic suite (select_premises, suggest_tactics, search_proof).
• Wu et al. "Autoformalization with Large Language Models." NeurIPS 2022, arXiv:2205.12615. The first systematic study of Codex / PaLM autoformalization rates on undergraduate math.
• Mathlib Community. "Mathlib4: The Lean Mathematical Library." leanprover-community.github.io, ongoing. The substrate every modern Lean-based theorem prover targets; over 1.2M lines as of 2026.
• Tao. "Formalizing the proof of PFR in Lean 4 - a personal account." Blog post, December 2023. The Polynomial Freiman-Ruzsa formalization; case study for what AI assistance can shorten in research-level formalization.

Frontier:

• DeepSeek-Prover team. "DeepSeek-Prover-V2." arXiv:2504.14589 (2025). Open-weight RL-trained prover competitive with proprietary frontier on miniF2F; 7B and 671B-MoE variants.
• Goedel-Prover team. "Goedel-Prover-V2." arXiv:2502.07640 (2025). Self-correction-driven Lean prover; reaches state-of-the-art miniF2F-test pass rates without RL on a held-out set.
• PutnamBench. "Multilingual Competition Mathematics Benchmark for Formal Theorem-Proving." arXiv:2407.11214 (2024). The Putnam-level evaluation harness across Lean, Coq, Isabelle.

Related Topics

• Theorem proving in Lean
• Reasoning data curation
• Mechanistic interpretability