CoChat
Sign Up
Cited by 23Artificial Intelligence ApplicationsMathematics, Computing, and Information ProcessingArtificial Intelligence in Games

Olympiad-level formal mathematical reasoning with reinforcement learning

Open access
Hubert, Thomas, Mehta, Rishi, Sartran, Laurent, Horváth, Miklós Z., Žužić, Goran, Wieser, Eric, Huang, Aja, Schrittwieser, Julian +31 more·2026·Nature
DOI 10.1038/s41586-025-09833-yPMC PMC12999475
Open this paper in CoChat — free accountOpen PDF

Abstract

A long-standing goal of artificial intelligence (AI) is to build systems capable of complex reasoning in vast domains, a task epitomized by mathematics with its boundless concepts and demand for rigorous proof. Recent AI systems, often reliant on human data, typically lack the formal verification necessary to guarantee correctness. By contrast, formal languages such as Lean 1 offer an interactive environment that grounds reasoning, and reinforcement learning (RL) provides a mechanism for learning in such environments. Here we present AlphaProof, an AlphaZero-inspired 2 agent that learns to find formal proofs through RL by training on millions of auto-formalized problems. For the most difficult problems, it uses test-time RL, a method of generating and learning from millions of related problem variants at inference time to enable deep, problem-specific adaptation. AlphaProof substantially improves state-of-the-art results on historical mathematics competition problems. At the 2024 International Mathematical Olympiad competition, our AI system, with AlphaProof as its core reasoning engine, solved three out of the five non-geometry problems, including the competition’s most difficult problem. Combined with AlphaGeometry 2 3 , this performance, achieved with multi-day computation, resulted in reaching a score equivalent to that of a silver medallist, marking the first time an AI system achieved any medal-level performance, to our knowledge. Our work demonstrates that learning at scale from grounded experience produces agents with complex mathematical reasoning strategies, paving the way for a reliable AI tool in complex mathematical problem solving.

Verified 2026-10-23 · 1 reference not checked yet

AI snapshot

Written from the paper’s full text.

TL;DR

AlphaProof is an AlphaZero-inspired reinforcement learning agent that finds formal proofs in Lean, trained on roughly 80 million auto-formalized problems and augmented by test-time RL (TTRL) on generated problem variants. Combined with AlphaGeometry 2, it solved four of six problems at the 2024 IMO for 28/42 points — silver-medal level, the first medal-level performance by an AI system to the authors' knowledge.

Key findings

  • On benchmarks, AlphaProof achieved 96.3% on miniF2F-test, 33.2% on formal-imo, and 27.9% on PutnamBench-test with just 2 TPU minutes of search per problem; at 500 TPU days with TTRL these rose to 99.6%, 58.3%, and 56.1%, respectively (Table 1), versus prior bests of 88.9% (DeepSeek-Prover-V2) on miniF2F-test and 5.3% on PutnamBench-test.
  • TTRL added about 15 absolute percentage points on both formal-imo and PutnamBench-test beyond a 12 TPU-hours search budget; scaling search from 2 TPU minutes to 12 TPU hours alone gained over 10 points on those benchmarks.
  • Main RL (~80,000 TPU days) improved both strength and efficiency: the final agent solved about 30% of historical IMO problems with only 300 simulations, a level earlier agents could not reach with vastly more search.
  • At IMO 2024, AlphaProof proved P1, P2, and P6 (including the hardest problem, P6, solved by only five human contestants) after 2–3 days of TTRL each; AlphaGeometry 2 solved P4, giving 28/42 points, one below the gold threshold. P3 and P5 (combinatorics) remained unsolved. On formal-imo with TTRL, subject performance was 75.7% (number theory), 72.6% (algebra), 20.3% (combinatorics).

Methods

  • Design: a 3-billion-parameter encoder–decoder transformer (policy + value) guiding an AND–OR AlphaZero-style tree search in a custom Lean 4 RL environment (reward −1 per tactic; return = minimum over independent subgoals), plus a Gemini 1.5 Pro-based auto-formalizer (~1M natural-language problems → ~80M Lean problems) and a test-time RL loop that trains a specialist agent on hundreds of thousands of generated variants per target problem.
  • Data/compute: pretraining on ~300B tokens of code and math text; SFT on ~300,000 Mathlib state–tactic pairs (~10 TPU days); auto-formalization ~100,000 TPU days; main RL ~80,000 TPU days (~1M training steps, distributed actors/matchmaker/learner).
  • Main analysis: solve rates on held-out benchmarks (corrected miniF2F, expert-formalized formal-imo of 258 non-geometry IMO problems, PutnamBench-test of 189 problems) under varying inference budgets, plus a pre-registered-style live evaluation at IMO 2024 with frozen hyperparameters, expert manual formalization, k=500 Gemini answer guesses (refuted at 99%/98%/7% for P1/P2/P6 in low-compute mode), and independent judging by Prof. Sir Timothy Gowers and Dr Joseph Myers.

Limitations

  • Stated: the bespoke learning phase requires a scale of domain-specific training likely beyond most academic groups; TTRL takes multi-day inference for the hardest problems; successes are confined to advanced high-school and undergraduate competition mathematics within a fixed library of concepts, and extension to research mathematics (theory building, "mathematical taste") is open; heavy compute raises accessibility concerns for an open research ecosystem.
  • Evident from text (not framed as such): geometry was excluded from formal-imo and handled by a separate system (AlphaGeometry 2) owing to Mathlib gaps, so the IMO score is not attributable to AlphaProof alone; the 2024 IMO problems were formalized by experts (P5 could not be formalized within the first day) rather than by the system end-to-end; pretraining corpora may have incidentally contained natural-language discussions or solutions to historical problems (Lean code was excluded); benchmark comparisons against other systems carry dataset-version caveats.

Model-written summary. Check it against the paper before relying on it.

Integrity signals

Registry

Crossref · 10.1038/s41586-025-09833-y

Cites

51 of 83 references verified0 citation errors · 31 not checkable

Statistics

Nothing to recompute.

Claims the paper makes

11 of 29 cited sources checked · 4 supported · 0 flagged · accuracy not yet measured

  • Premisecitation

    Before this work, even the most advanced AI systems could typically solve only a small fraction of the easiest historical IMO problems.

    “before this work, even the most advanced AI systems could typically solve only a small fraction of the easiest historical IMO problems13,17,23”
    Quote in the paperSubstantial claim2 of 3 sources checked
    • cites [13] Polu, S. & Sutskever, I. Generative language modeling for automated theorem proving. In 5th Conference on Artificial Intelligence and Theorem Proving (AITP) (eds Hales, T. C. et al.) (2020).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites [17] Lample, G. et al. Hypertree proof search for neural theorem proving. Adv. Neural Inf. Process. Syst. 35, 26337–26349 (2022). source

      Section 7.1.1 (p. 11) reports that the earlier GPT-f system solved 36.6% of the miniF2F test split, supporting the narrower point that a prior prover could not solve most problems on that benchmark. The paper does not characterize that split as the easiest historical IMO problems or establish that advanced systems typically solved only a small fraction of those problems. (LLM, conf=0.79)

      Experimental — accuracy not yet measured
    • cites [23] Ying, H. et al. InternLM-Math: open math large language models toward verifiable reasoning. Preprint at https://arxiv.org/abs/2402.06332 (2024). source

      Section 6.1 (p. 8) reports results on MiniF2F, a benchmark of formalized math problems, but does not identify a subset of the easiest historical IMO problems or report how earlier AI systems performed on it. Searches for IMO and historical International Mathematical Olympiad problems found no passage addressing that claim. (LLM, conf=0.73)

      Experimental — accuracy not yet measured
  • Interpretationcitation

    AlphaProof is an RL agent designed to discover formal mathematical proofs by interacting with a verifiable environment based on the Lean theorem prover.

    “AlphaProof is an RL agent designed to discover formal mathematical proofs by interacting with a verifiable environment based on the Lean theorem prover1.”
    Quote in the paperSubstantial claim1 of 1 sources checked
    • cites [1] de Moura, L. & Ullrich, S. The Lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: Proc. 28th International Conference on Automated Deduction Proceedings (eds Platzer, A. & Sutcliffe, G.) 625–635 (Springer, 2021). source
  • Findingcitation

    The AlphaProof proof network is a 3-billion-parameter encoder-decoder transformer model.

    “The proof network is a 3-billion-parameter encoder–decoder transformer model15, similar to ref. 16.”
    Quote in the paperNot a substantial claim1 of 2 sources checked
    • cites [15] Vaswani, A. et al. Attention is all you need. Adv. Neural Inf. Process. Syst. 30, 5998–6008 (2017).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites [16] Li, Y. et al. Competition-level code generation with alphacode. Science 378, 1092–1097 (2022). source
  • Findingcitation

    The training curriculum for main RL was supplemented by approximately 3,500 manually human-formalized problems from miniF2F-curriculum, auto-formalization training set, and PutnamBench-train.

    “This was supplemented by a small fraction (approximately 3,500 problems) of manually human-formalized problems sourced from: (1) the miniF2F-curriculum benchmark24; (2) the set of problems manually formalized for training the auto-formalization model; and (3) our training split of the Putnam benchmark (PutnamBench-train, derived from ref. 21 by excluding PutnamBench-test).”
    Quote in the paperNot a substantial claim1 of 2 sources checked
    • cites [24] Polu, S. et al. Formal mathematics statement curriculum learning. In International Conference on Learning Representations (eds Kim, B. et al.) https://openreview.net/forum?id=-P7G-8dmSh4 (OpenReview.net, 2023).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites [21] Tsoukalas, G. et al. PutnamBench: evaluating neural theorem-provers on the putnam mathematical competition. Adv. Neural Inf. Process. Syst. 37, 11545–11569 (2024). source
  • Findingown data

    AlphaProof substantially improves state-of-the-art results on historical mathematics competition problems.

    “AlphaProof substantially improves state-of-the-art results on historical mathematics competition problems.”
    Quote in the paperSubstantial claim
  • Classified as probably not a substantial claim. 40
  • May combine two claims. 38
  • The quote only partly states this claim. 1

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation

    The primary method for applying more computation at inference, common in the AlphaZero family of agents, is scaling the tree search and running multiple independent search attempts.

    “The primary method for applying more computation at inference, common in the AlphaZero family of agents2,72, is scaling the tree search and running multiple independent search attempts.”
    Quote in the paperNot a substantial claim2 of 2 sources checked
    • cites [2] Silver, D. et al. A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science 362, 1140–1144 (2018). source

      The Search section (p. 17) describes AlphaZero’s Monte Carlo tree search as a series of simulations, and Configuration (p. 19) specifies 800 simulations per search during training. These passages support using tree search to spend computation on a move, but they do not describe multiple independent search attempts or establish that the two methods are the primary approach across the AlphaZero family. (LLM, conf=0.86)

      Experimental — accuracy not yet measured
    • cites [72] Schrittwieser, J. et al. Mastering Atari, Go, chess and shogi by planning with a learned model. Nature 588, 604–609 (2020). source

      Appendix B Search (p. 12) describes an AlphaZero-like tree search that repeats simulations, and Appendix I Evaluation (p. 19) reports evaluating different numbers of simulations per search. This supports scaling inference-time search, but the simulations update a shared tree; the paper does not describe running multiple independent search attempts or establish that the combined approach is the primary method. (LLM, conf=0.88)

      Experimental — accuracy not yet measured

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Premisecitation

    This approach has led to gold-equivalent performance at the International Olympiad in Informatics and strong performance in the American Invitational Mathematics Examination.

    “This approach has led to gold-equivalent performance at the International Olympiad in Informatics62 and strong performance in the American Invitational Mathematics Examination.”
    Quote in the paperNot a substantial claim1 of 1 sources checked
    • cites [62] OpenAI et al. Competitive programming with large reasoning models. Preprint at https://arxiv.org/abs/2502.06807 (2025). source

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Premisecitation

    OpenAI O1 and DeepSeek R1 demonstrated the effectiveness of scaling RL for LLM reasoning, observing logarithmic scaling with compute at both training and test time.

    “More recently, OpenAI O161 and DeepSeek R19 have demonstrated the effectiveness of scaling RL for LLM reasoning, observing logarithmic scaling with compute at both training and test time.”
    Quote in the paperNot a substantial claim2 of 2 sources checked
    • cites [61] OpenAI. OpenAI o1 system card. Preprint at https://arxiv.org/abs/2412.16720 (2024).

      The Introduction (p. 1) says the o1 series is trained with large-scale reinforcement learning to reason using chain of thought, and §2 (p. 1) describes its reasoning capabilities. The passages do not report logarithmic scaling with training- or test-time compute; a search for that scaling claim found no supporting passage. DeepSeek R1 has a separate citation in the citing sentence and is not assessed here. (LLM, conf=0.85)

      Experimental — accuracy not yet measured
    • cites [9] Guo, D. et al. DeepSeek-R1: incentivizing reasoning capability in LLMs via reinforcement learning. Nature 645, 633–638 (2025). source

      The DeepSeek-R1-Zero section reports that reasoning performance improved during RL training, and the conclusion describes large-scale RL as a means of incentivizing reasoning. The paper mentions test-time scaling behaviour, but the passages in our copy do not establish logarithmic scaling with compute at either training or test time. This source also cannot establish the claim about OpenAI O1. (LLM, conf=0.87)

      Experimental — accuracy not yet measured

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation

    An automated feedback signal from theorem provers for correct proofs has been pivotal for applying large-scale machine learning to theorem proving.

    “An automated feedback signal from theorem provers for correct proofs has been pivotal for applying large-scale machine learning to theorem proving.”
    Quote in the paperNot a substantial claim1 of 4 sources checked
    • cites [13] Polu, S. & Sutskever, I. Generative language modeling for automated theorem proving. In 5th Conference on Artificial Intelligence and Theorem Proving (AITP) (eds Hales, T. C. et al.) (2020).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites [24] Polu, S. et al. Formal mathematics statement curriculum learning. In International Conference on Learning Representations (eds Kim, B. et al.) https://openreview.net/forum?id=-P7G-8dmSh4 (OpenReview.net, 2023).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites [40] Han, J. M., Rute, J., Wu, Y., Ayers, E. & Polu, S. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations (eds Liu, Y. et al.) https://openreview.net/forum?id=rpxJc9j04U (OpenReview.net, 2022).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

    • cites [41] Wu, M., Norrish, M., Walder, C. & Dezfouli, A. TacticZero: learning to prove theorems from scratch with deep reinforcement learning. Adv. Neural Inf. Process. Syst. 34, 9330–9342 (2021). source

      Section 3.1 (p. 6) describes a learning signal: the agent receives a positive reward when it proves a theorem and a negative reward when a proof attempt fails. This supports the role of proof-success feedback in the paper’s approach, but the paper does not establish the broader claim that such feedback has been pivotal to large-scale machine learning for theorem proving. (LLM, conf=0.82)

      Experimental — accuracy not yet measured

  • May combine two claims.

    Findingown data

    TTRL yielded rapid initial gains, solving many new problems within the first 50 TPU days, and continued to find new solutions as training progressed over longer durations.

    “This approach yielded rapid initial gains, solving many new problems within the first 50 TPU days, and continued to find new solutions as training progressed over longer durations.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    AlphaProof achieved 96.3% on miniF2F-test, 33.2% on formal-imo, and 27.9% on PutnamBench-test at 2 TPU minutes.

    “AlphaProof | 2 TPU minutes | 96.3% | 33.2% | 27.9%”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    On formal-imo, TTRL reached particularly strong performance in number theory (75.7%) and algebra (72.6%), and also made progress in combinatorics (20.3%).

    “On formal-imo, TTRL reached particularly strong performance in number theory (75.7%) and algebra (72.6%), and also made progress in combinatorics (20.3%).”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    AlphaProof with TTRL achieved 97.5% on miniF2F-test, 53.9% on formal-imo, and 45.5% on PutnamBench-test at 50 TPU days.

    “AlphaProof with TTRL | 50 TPU days | 97.5% | 53.9% | 45.5%”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    AlphaProof with TTRL achieved 99.6% on miniF2F-test, 58.3% on formal-imo, and 56.1% on PutnamBench-test at 500 TPU days.

    “AlphaProof with TTRL | 500 TPU days | 99.6% | 58.3% | 56.1%”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    This yielded a total score of 28 out of 42 points, placing our AI system's performance within the silver-medal range, one point below the gold-medal threshold.

    “This yielded a total score of 28 out of 42 points (‘Discussion and conclusion’), placing our AI system’s performance within the silver-medal range of the official competition, one point below the gold-medal threshold”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Findingreasoning

    The AlphaProof environment casts the tactic mode of Lean as an RL environment.

    “It is this tactic mode of Lean that we cast as an RL environment”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingreasoning

    The combined AlphaProof and AlphaGeometry 2 performance solved four of the six 2024 IMO competition problems, reaching the same score as a 2024 IMO silver medallist.

    “This combined performance resulted in solving four of the six competition problems, thereby reaching the same score as a 2024 IMO silver medallist.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given

    AlphaProof's solutions required computational time far exceeding that of human contestants.

    “Although its solutions required computational time far exceeding that of human contestants”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    Each of these solutions required 2-3 days of TTRL, demonstrating substantial problem-specific adaptation at inference.

    “Each of these solutions required 2–3 days of TTRL, demonstrating substantial problem-specific adaptation at inference.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    At the 2024 IMO, AlphaProof solved the three algebra and number theory problems, including P6, and AlphaGeometry 2 solved the geometry problem.

    “As part of a complete problem-solving pipeline, AlphaProof successfully solved the three algebra and number theory problems, including the most difficult problem P6, and AlphaGeometry 2 solved the geometry problem.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given

    Many of the custom additions developed for AlphaProof have since been accepted and integrated into the public Mathlib library.

    “many have since been accepted and integrated into the public Mathlib library, underscoring their broad utility and alignment with the library’s development goals.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    The auto-formalization model auto-formalized approximately 1 million natural-language problems into a dataset of around 80 million formal Lean problems, vastly exceeding the scale of all other available datasets.

    “Over the course of the project, this model auto-formalized approximately 1 million natural-language problems into a dataset of around 80 million formal Lean problems, vastly exceeding the scale of all other available datasets.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    Compiling key Mathlib tactics to C code results in some tactics executing six-times faster.

    “Key Mathlib tactics frequently used by the agent (for example, linarith) were compiled to C code. This results in some tactics executing (that is, generating proof terms) six-times faster.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    The final AlphaProof agent solves approximately 30% of problems with only 300 simulations, a level of performance that earlier agents could not reach even with vastly more search.

    “For instance, the final agent solves approximately 30% of problems with only 300 simulations, a level of performance that earlier agents could not reach even with vastly more search.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    TTRL yields comprehensive gains across all benchmarks, with a perfect score on miniF2F-valid and near-perfect scores on the test split.

    “This approach yields comprehensive gains across all benchmarks (Table 1), with a perfect score on miniF2F-valid (Extended Data Table 2) and near-perfect scores on the test split.”
    Quote in the paperSubstantial claim

  • The quote only partly states this claim.

    Findingown data

    Combined with AlphaGeometry 2, this performance resulted in reaching a score equivalent to that of a silver medallist.

    “Combined with AlphaGeometry 23, this performance, achieved with multi-day computation, resulted in reaching a score equivalent to that of a silver medallist”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    AlphaProof achieved 97.7% on miniF2F-test, 43.7% on formal-imo, and 39.4% on PutnamBench-test at 12 TPU hours.

    “AlphaProof | 12 TPU hours | 97.7% | 43.7% | 39.4%”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    The combined system, with AlphaProof solving P1, P2 and P6, and AlphaGeometry 2 solving P4, successfully solved four of the six IMO problems.

    “The combined system, with AlphaProof solving P1, P2 and P6, and AlphaGeometry 2 solving P4, successfully solved four of the six IMO problems.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    At the 2024 International Mathematical Olympiad, the AI system with AlphaProof as its core reasoning engine solved three out of the five non-geometry problems, including the competition's most difficult problem.

    “At the 2024 International Mathematical Olympiad competition, our AI system, with AlphaProof as its core reasoning engine, solved three out of the five non-geometry problems, including the competition’s most difficult problem.”
    Quote in the paperSubstantial claim
    • Rests on an assumption: The 2024 IMO P6 was the most difficult problem at the competition.

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given

    The multi-day computational effort for AlphaProof's solutions significantly exceeds the time constraints faced by human contestants.

    “Although the multi-day computational effort for AlphaProof’s solutions significantly exceeds the time constraints faced by human contestants”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    The main RL training was conducted for approximately 1 million training steps.

    “The RL training was conducted for approximately 1 million training steps (Supplementary Table 6).”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    formal-imo contains 258 problems: 107 algebra, 77 combinatorics and 74 number theory problems.

    “It contains 258 problems: 107 algebra, 77 combinatorics and 74 number theory problems (based on the official subject when available, or classification by domain experts).”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    The main RL training loop learned from the auto-formalized curriculum and spanned approximately 80,000 TPU days.

    “The main RL training loop, which learned from this curriculum, was of a similar scale, spanning approximately 80,000 TPU days (equivalent to, for instance, 4,000 TPUs utilized for 20 days).”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    The SFT stage on the Mathlib dataset was comparatively inexpensive, approximately 10 TPU days.

    “The SFT stage on the Mathlib dataset was comparatively inexpensive (approximately 10 TPU days).”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data

    On the 50 representative Putnam problems, the auto-formalization process achieved a 64% pass@1 rate, with 72.7% in number theory, 61.9% in algebra, and 54.6% in geometry.

    “On the 50 representative Putnam problems, the pass@1 rate was 64%, with strong performance in number theory (72.7%), algebra (61.9%) and geometry (54.6%).”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    Before IMO 2024, the final auto-formalization process achieved a 60% pass@1 success rate on the 50 representative IMO problems, with 81.3% in algebra, 76.9% in number theory, and 33.3% in combinatorics.

    “Before the IMO 2024 competition, the final auto-formalization process achieved a 60% pass@1 success rate on the 50 representative IMO problems, with notable strengths in algebra (81.3%) and number theory (76.9%), and a lower rate for combinatorics (33.3%).”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    The most frequent subjects in PutnamBench-test were algebra (78), analysis (57), number theory (33), geometry (20) and linear algebra (18).

    “The most frequent ones in PutnamBench-test were algebra (78), analysis (57), number theory (33), geometry (20) and linear algebra (18).”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Findingnone given

    Incorrect formalizations were often quickly resolved during main RL or sometimes presented interesting problems in their own right.

    “with incorrect ones often being quickly resolved during main RL or sometimes presenting interesting problems in their own right.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given

    P5 (combinatorics) proved exceptionally challenging to formalize, with initial attempts by experts being unsuccessful within the first day.

    “Notably, P5 (combinatorics) proved exceptionally challenging to formalize, with initial attempts by experts being unsuccessful within the first day.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Findingown data

    The auto-formalization process generated approximately 80 million problem curriculum over the course of the project and required approximately 100,000 TPU days in total.

    “The auto-formalization process, which generated the approximately 80 million problem curriculum over the course of the project, required approximately 100,000 TPU days in total (equivalent to, for instance, 10 runs of 2,000 TPUs utilized for 5 days).”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    For a subset of about 50 problems, experts provided detailed chain-of-thought explanations outlining the formalization steps.

    “For a subset of about 50 of these problems, experts also provided detailed chain-of-thought explanations outlining the formalization steps.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Findingnone given

    The RL training architecture comprises a centralized matchmaker, distributed actors and a centralized learner.

    “The RL training architecture comprises three main components: a centralized matchmaker, distributed actors and a centralized learner.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Findingnone given

    The main RL phase further trains the proof network, initialized from pretraining and SFT.

    “The main RL phase further trains the proof network, initialized from pretraining and SFT.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    In a low-compute refutation mode within a 10-minute tree search per candidate, AlphaProof successfully disproved 99% of incorrect Gemini-generated candidates for P1, 98% for P2 and 7% for P6.

    “AlphaProof was then crucial for efficiently sifting through these numerous proposals; in a low-compute refutation mode (within a 10-minute tree search per candidate), it successfully disproved 99% of incorrect Gemini-generated candidates for P1, 98% for P2 and 7% for P6, thereby isolating promising candidates for the subsequent full proof attempts.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    AlphaProof solved IMO 2024 problems P1, P2 and P6.

    “Solutions generated by AlphaProof (P1, P2 and P6, shown in Extended Data Figs. 7–9) were first verified for correctness by the Lean kernel.”
    • Also stated in: § Evaluation · plain
      “who awarded full points for each solved problem.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data

    The system generated k = 500 answers and successfully guessed the correct answers for all applicable problems.

    “We generated k = 500 answers, successfully guessing the correct answers for all applicable problems.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data

    A side experiment to test the auto-formalization system successfully formalized P1, P2 and P6.

    “Alongside this manual effort, we conducted a side experiment to test our auto-formalization system, which in fact successfully formalized P1, P2 and P6.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Study design and conductown data

    Problems from even-numbered years, 1990 onwards, were reserved as a dedicated held-out test set (PutnamBench-test).

    “For the Putnam benchmark, problems from even-numbered years, 1990 onwards, were reserved as a dedicated held-out test set (PutnamBench-test).”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Interpretationreasoning

    AlphaProof's success in solving three problems from a live IMO competition, including 2024's most difficult P6, demonstrates a profound advance in the potential of AI for mathematical reasoning.

    “AlphaProof’s success in solving three problems from a live IMO competition, including 2024’s most difficult P6, which was solved by only five human contestants, therefore demonstrates a profound advance in the potential of AI for mathematical reasoning”
    Quote in the paperSubstantial claim
    • Rests on an assumption: The 2024 IMO P6 was solved by only five human contestants.
    • Rests on an assumption: The 2024 IMO P6 was the most difficult problem at the competition.

  • May combine two claims.

    Study design and conductreasoning

    Every proof or disproof found by AlphaProof undergoes a final, independent verification step using the standard Lean command-line tool, and a custom command verifies reliance only on three accepted axioms.

    “every proof or disproof found by AlphaProof undergoes a final, independent verification step. This involves executing the standard Lean command-line tool on a .lean file containing the complete theorem statement and the agent-generated proof. A custom command also verifies that the proof only relies on the three commonly accepted axioms built-in to Lean itself”
    Quote in the paperSubstantial claim
    • The authors state this as an assumption: The Lean kernel and the declared axioms are sound.

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Interpretationown data

    The distinct x-axis scales in Fig. 4 highlight the different computational investments and capabilities of these two complementary scaling strategies, with TTRL providing a powerful mechanism for tackling the most challenging problems.

    “The distinct x-axis scales in Fig. 4 (TPU hours for search versus hundreds of TPU days for TTRL) highlight the different computational investments and capabilities of these two complementary scaling strategies, with TTRL providing a powerful mechanism for tackling the most challenging problems.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

    Interpretationnone given

    The significant computational requirements of this work raise important questions about accessibility and the future of an open research ecosystem.

    “The significant computational requirements of this work raise important questions about accessibility and the future of an open research ecosystem.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Premisereasoning

    LLMs trained on informal mathematical text lack guaranteed correctness, limiting their reliability for validating mathematical claims or tackling problems without pre-existing reference points.

    “This lack of guaranteed correctness limits their reliability for validating mathematical claims or tackling problems without pre-existing reference points.”
    Quote in the paperSubstantial claim0 of 2 sources checked
    • cites [11] Petrov, I. et al. Proof or bluff? Evaluating LLMs on 2025 USA Math Olympiad. In Proc. Second AI for MATH Workshop at the 42nd International Conference on Machine Learning (eds Huang, Y. et al.) 1–15 (2025).

      Not checked in the free run.

    • cites [12] Mahdavi, H. et al. Brains vs. bytes: evaluating LLM proficiency in olympiad mathematics. In Conference on Language Modeling (COLM) (eds Artzi, Y. et al.) https://openreview.net/forum?id=uXR2KsA4L9 (OpenReview.net, 2025).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • May combine two claims.

    Interpretationown data

    For peak performance on the most complex problems, TTRL is crucial, extending the state of the art by a significant margin.

    “For peak performance on the most complex problems, TTRL is crucial, extending the state of the art by a significant margin”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Study design and conductnone given

    AlphaProof's miniF2F-test results are reported on a corrected version of the dataset.

    “AlphaProof’s miniF2F-test results are reported on a corrected version of the dataset (see Methods for details).”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

    Interpretationnone given

    The bespoke learning phase required by AlphaProof represents a scale of domain-specific training likely beyond the reach of most academic research groups.

    “the bespoke learning phase required by AlphaProof represents a scale of domain-specific training that is likely beyond the reach of most academic research groups.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

    Interpretationreasoning

    The transition to research mathematics is particularly challenging because it requires moving beyond pure problem solving to theory building-the continuous expansion of the library with new concepts.

    “This transition is particularly challenging as it requires moving beyond pure problem solving to theory building—the continuous expansion of this library with new concepts.”
    Quote in the paperNot a substantial claim
    • Rests on an assumption: Advanced high-school and undergraduate competition mathematics problems operate within a known fixed library of mathematical concepts with a certain degree of thematic consistency.

  • May combine two claims.

    Interpretationnone given

    AlphaProof's TTRL generates a diverse curriculum of relevant formal variants for challenging IMO and Putnam-level problems within Lean and leverages Lean's rigorous verification to guide learning.

    “It achieves this by generating a diverse curriculum of relevant formal variants for challenging IMO and Putnam-level problems within Lean, and leveraging Lean’s rigorous verification to guide learning, ultimately enabling the discovery of complex, validated proofs in this formal setting.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Study design and conductnone given

    For PutnamBench-test, scores for previous work were recalculated based on the publicly available proofs reported by each system, for consistent comparison against our PutnamBench-test split.

    “For PutnamBench-test, scores for previous work were recalculated based on the publicly available proofs reported by each system, for consistent comparison against our PutnamBench-test split”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

    Interpretationnone given

    Problem-specific adaptation allows the agent to fine-tune its learned strategies and potentially discover insights crucial for the target problem.

    “This problem-specific adaptation allows the agent to fine-tune its learned strategies and potentially discover insights crucial for the target problem.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationnone given

    Attempting multiple independent search attempts increases the probability of finding a proof and offers latency benefits via parallelization.

    “Attempting multiple independent search attempts also increases the probability of finding a proof and offers latency benefits via parallelization.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Interpretationreasoning

    The TTRL framework can be concurrently applied to multiple distinct target problems by incorporating all their respective variants into a shared start position dataset for the matchmaker.

    “This framework can be concurrently applied to multiple distinct target problems by incorporating all their respective variants into a shared start position dataset for the matchmaker, allowing for simultaneous TTRL across different target problems as presented in Fig. 4b.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Premisenone given

    Such successes in interactive theorem proving typically demand extensive work from domain experts.

    “However, such successes typically demand extensive work from domain experts.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Premisecitation

    The IMO has so far remained out of reach for current LLMs, with recent studies highlighting their limited proving capabilities.

    “However, the IMO has so far remained out of reach for current LLMs, with recent studies highlighting their limited proving capabilities11,12.”
    Quote in the paperSubstantial claim0 of 2 sources checked
    • cites [11] Petrov, I. et al. Proof or bluff? Evaluating LLMs on 2025 USA Math Olympiad. In Proc. Second AI for MATH Workshop at the 42nd International Conference on Machine Learning (eds Huang, Y. et al.) 1–15 (2025).

      Not checked in the free run.

    • cites [12] Mahdavi, H. et al. Brains vs. bytes: evaluating LLM proficiency in olympiad mathematics. In Conference on Language Modeling (COLM) (eds Artzi, Y. et al.) https://openreview.net/forum?id=uXR2KsA4L9 (OpenReview.net, 2025).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • Classified as probably not a substantial claim.

    Study design and conductown data

    The paired outputs were evaluated by an internal panel of approximately three Lean experts for pointwise correctness and side-by-side preference.

    “These paired outputs were then evaluated by an internal panel of approximately three Lean experts for pointwise correctness and side-by-side preference.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation

    AlphaProof's TTRL methodology was first outlined in ref. 28.

    “AlphaProof’s TTRL methodology (first outlined in ref. 28)”
    Quote in the paperNot a substantial claim0 of 1 sources checked
    • cites [28] AlphaProof and AlphaGeometry teams. AI achieves silver-medal standard solving international mathematical olympiad problems. Google DeepMind https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ (2024).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • Classified as probably not a substantial claim.

    Study design and conductnone given

    An agreement was established with Prof Sir Timothy Gowers and Dr Joseph Myers to serve as independent expert judges for any solutions produced by the AI system, evaluating them according to official IMO point-awarding rules.

    “As part of this, an agreement was established with Prof Sir Timothy Gowers and Dr Joseph Myers to serve as independent expert judges for any solutions produced by our AI system, evaluating them according to official IMO point-awarding rules.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation

    Formal verification tools have enabled significant achievements, including the formal verification of the four-colour theorem and the CompCert C compiler.

    “These tools have enabled significant achievements, including the formal verification of the four-colour theorem32 and critical software such as the CompCert C compiler33.”
    Quote in the paperNot a substantial claim0 of 2 sources checked
    • cites [32] Gonthier, G. The four colour theorem: engineering of a formal proof. In Asian Symposium on Computer Mathematics 333–333 (Springer, 2007). source
    • cites [33] Leroy, X. et al. CompCert: A formally verified optimizing compiler. In Embedded Real Time Software and Systems (ERTS 2016) (ed. Sifakis, J.) 1–10 (SEE, 2016).

      Couldn’t be matched to a paper in Crossref, so it can’t be checked.

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Study design and conductnone given

    Several misformalizations in the original PutnamBench were identified and subsequently corrected upstream.

    “During our work, several misformalizations in the original PutnamBench were identified and subsequently corrected upstream.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation

    The TTRL approach-systematically generating and solving related, often simpler, problem variants to build towards a solution for a complex target problem-is inspired by a core tenet of human mathematical problem solving, as described by Polya.

    “Indeed, this TTRL approach—systematically generating and solving related, often simpler, problem variants to build towards a solution for a complex target problem—is inspired by a core tenet of human mathematical problem solving, as notably described by Polya75.”
    Quote in the paperNot a substantial claim0 of 1 sources checked
    • cites [75] Pólya, G. How to Solve It: A New Aspect of Mathematical Method (Princeton University Press, 2014). source

  • May combine two claims.

    Interpretationown data

    The supervised fine-tuning stage refines the policy head for Lean-specific tactic generation and initializes the value head to estimate the number of remaining steps in a proof.

    “This process refines the policy head for Lean-specific tactic generation and initializes the value head to estimate the number of remaining steps in a proof, based on the structure of the Mathlib proofs.”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Interpretationnone given

    The iterative process of experience generation and network updates progressively enhances the proof network's mathematical reasoning capabilities.

    “This iterative process of experience generation and network updates progressively enhances the proof network’s mathematical reasoning capabilities.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationreasoning

    The auto-formalization sampling process produced multiple distinct formal translations for each natural-language problem, ensuring a higher likelihood of including a correct formalization.

    “this sampling process involved producing multiple distinct formal translations for each natural-language problem. This strategy ensured a higher likelihood of including a correct formalization”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Interpretationreasoning

    The pretraining stage imbued the policy head with a broad understanding of programming syntax, logical structures and mathematical language.

    “This stage imbued the policy head (decoder) with a broad understanding of programming syntax, logical structures and mathematical language.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Study design and conductnone given

    All generated candidate variants are validated for syntactic correctness in Lean.

    “All generated candidates are validated for syntactic correctness in Lean.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationreasoning

    Increasing the number of simulations performed allows the agent to refine initial tactic suggestions, integrate information over deeper reasoning and explore other proof sequences, leading to stronger tactic selection and a higher probability of finding a proof.

    “Increasing the number of simulations performed allows the agent to refine the initial tactic suggestions provided by the proof network, integrate information over more lines of deeper reasoning and explore other potential proof sequences. This enhanced search leads to stronger tactic selection and a higher probability of finding a proof.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim. May combine two claims.

    Study design and conductnone given

    The main RL training of AlphaProof was halted, and all system hyperparameters were frozen before the official release of the IMO 2024 problems.

    “The main RL training of AlphaProof was halted, and all system hyperparameters were frozen before the official release of the IMO 2024 problems.”
    Quote in the paperSubstantial claim
72 of 72

  • The paper relies on this without support.

    The 2024 IMO P6 was solved by only five human contestants.

    “including 2024’s most difficult P6, which was solved by only five human contestants”

  • The paper relies on this without support.

    The 2024 IMO P6 was the most difficult problem at the competition.

    “including the competition’s most difficult problem”
    “including 2024’s most difficult P6”

  • The authors state this as an assumption.

    The Lean kernel and the declared axioms are sound.

    “assuming the soundness of the Lean kernel and the declared axioms”

  • The paper relies on this without support.

    Advanced high-school and undergraduate competition mathematics problems operate within a known fixed library of mathematical concepts with a certain degree of thematic consistency.

    “these problems operate within a known fixed library of mathematical concepts with a certain degree of thematic consistency.”

  • The paper relies on this without support.

    Excluding Lean code and formal proofs from pretraining data is sufficient to prevent benchmark contamination from natural-language discussions or solutions.

    “Although the initial pretraining of the underlying language model utilized a broad web corpus that might have incidentally contained natural-language discussions or solutions to some historical problems, our pretraining pipeline explicitly excluded all Lean code—and critically, the formal proofs corresponding to our evaluation benchmarks—from this pretraining data.”
    “This data separation protocol was designed so that AlphaProof’s performance would reflect learned reasoning capabilities rather than memorization.”
5 of 5

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

Each contradiction between two passages listed here was confirmed by an independent check.

  • Largest value is described as the hardest subgoal

    Minor

    The paper defines a state's value as the negative number of tactics in its longest proof branch. Under that definition, a harder subgoal has a smaller, not larger, value.

1 of 1

Cites

Flagged first, then by citations

32 of the 80 references couldn’t be matched to a known paper.

Research works printed but not linked: 1

  1. OpenAI. OpenAI o1 system card. Preprint at https://arxiv.org/abs/2412.16720 (2024). · arXiv

Cited by

Sorted by citations

Authors
Hubert, T., Mehta, R., Sartran, L., Horváth, M. Z., Žužić, G., Wieser, E., Huang, A., Schrittwieser, J., Schroecker, Y., Masoom, H., Bertolli, O., Zahavy, T., Mandhane, A., Yung, J., Beloshapka, I., Ibarz, B., Veeriah, V., Yu, L., Nash, O., Lezeau, P., Mercuri, S., Sönne, C., Mehta, B., Davies, A., Zheng, D., Pedregosa, F., Li, Y., von Glehn, I., Rowland, M., Albanie, S., Velingker, A., Schmitt, S., Lockhart, E., Hughes, E., Michalewski, H., Sonnerat, N., Hassabis, D., Kohli, P., & Silver, D.
Affiliations
Google DeepMind (United Kingdom) (GB)
Corresponding author
  • Hubert, Thomas
  • Wieser, Eric
ORCID
Venue
Nature
Publisher
Springer Science and Business Media LLC
Published
2025-11-12
Volume
651
Issue
8106
Pages
607-613
ISSN
  • 0028-0836 (ISSN-L)
  • 1476-4687
DOI
10.1038/s41586-025-09833-y
PMC
PMC12999475
OpenAlex
W4416186944
Semantic Scholar
8682a36383e5285e29225b3e2a8618bb034527d4
Cited by
19
References
80
Citations by year
2026: 18 · 2025: 1
FWCI
7.80
Type
journal article
Language
en
Open access
Licence
Locations
  • Nature (publishedVersion, cc-by)
  • PubMed (publishedVersion)
  • PubMed Central (submittedVersion, cc-by)
Funders
DeepMind
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence Applications
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Mathematics, Computing, and Information Processing
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence in Games
Keywords
reinforcement learning, Lean theorem prover, mathematical olympiad problems, automated theorem proving, mathematical problem solving, formal verification
MeSH terms
Artificial Intelligence, Humans, Mathematics, Problem Solving, Reinforcement, Psychology

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Claims read by deepseek-v4.1-flash under definition version 3 (extract-v3) on 2026-10-23.

Classified by jev-1.13-20260917 (gold-guideline-v0.2) on 2026-10-23.

Cited sources are checked by gpt-6-sol.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review