Olympiad-level formal mathematical reasoning with reinforcement learning
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<sup>1</sup> 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<sup>2</sup> 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<sup>3</sup>, 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.
Authors
- Vivek Veeriah
- Demis Hassabis (ORCID: https://orcid.org/0000-0003-2812-9917)
- Aja Huang (ORCID: https://orcid.org/0000-0002-2476-9194)
- Edward Hughes (ORCID: https://orcid.org/0000-0002-2434-2334)
- Pushmeet Kohli (ORCID: https://orcid.org/0000-0002-7466-7997)
- Henryk Michalewski (ORCID: https://orcid.org/0000-0001-8541-8112)
- Miklós Z. Horváth (ORCID: https://orcid.org/0000-0001-6928-7423)
- Borja Ibarz (ORCID: https://orcid.org/0000-0003-3476-9953)
- Tom Zahavy (ORCID: https://orcid.org/0009-0009-2309-922X)
- Rajni Mehta (ORCID: https://orcid.org/0000-0002-3378-5583)
- Nicolas Sonnerat
- Eric Wieser (ORCID: https://orcid.org/0000-0003-0412-4978)
- Ingrid von Glehn
- Daniel Zheng (ORCID: https://orcid.org/0009-0006-4523-6262)
- Laurent Sartran (ORCID: https://orcid.org/0000-0002-5538-8327)
- Hussain Masoom
- Simon Schmitt (ORCID: https://orcid.org/0000-0001-6219-2130)
- Ottavia Bertolli (ORCID: https://orcid.org/0000-0001-8578-3216)
- Amol Mandhane (ORCID: https://orcid.org/0000-0002-3412-2634)
- Oliver Nash (ORCID: https://orcid.org/0000-0001-7208-6307)
- Salvatore Mercuri (ORCID: https://orcid.org/0000-0002-8997-8632)
- Julian Schrittwieser
- Edward Lockhart (ORCID: https://orcid.org/0000-0001-8753-0765)
- Thomas Hubert (ORCID: https://orcid.org/0000-0003-2209-3933)
- Yannick Schroecker
- J.‐Y. Yung
- David Silver (ORCID: https://orcid.org/0000-0002-5197-2892)
- Lei Yu (ORCID: https://orcid.org/0000-0002-7329-4631)
- Alex Davies (ORCID: https://orcid.org/0000-0003-4917-5234)
- Samuel Albanie (ORCID: https://orcid.org/0000-0003-1732-9198)
- Bhavik A. Mehta (ORCID: https://orcid.org/0009-0008-6979-5610)
- Fabián Pedregosa (ORCID: https://orcid.org/0000-0003-4025-3953)
- Mark Rowland
- Yin Li
- Ameya Velingker
- Goran Žužić
- Iuliya Beloshapka
- Paul Lezeau (ORCID: https://orcid.org/0009-0006-6142-9953)
- Calle Sönne (ORCID: https://orcid.org/0009-0008-1871-426X)
Institutions
- Google DeepMind (United Kingdom) (GB)
- Google (United Kingdom) (GB)
Publication Details
- Journal
- Nature
- Published
- 2025-11-12
- DOI
- https://doi.org/10.1038/s41586-025-09833-y
- Citations
- 4
- Primary Topic
- Evolutionary Algorithms and Applications
- Type
- article
- Field-Weighted Citation Impact
- 9.92
Funders
- DeepMind