{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T16:49:26Z","timestamp":1784652566447,"version":"3.55.0"},"reference-count":80,"publisher":"Springer Science and Business Media LLC","issue":"8106","license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T00:00:00Z","timestamp":1773360000000},"content-version":"vor","delay-in-days":121,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Nature"],"published-print":{"date-parts":[[2026,3,19]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    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\n                    <jats:sup>1<\/jats:sup>\n                    offer an interactive environment that grounds reasoning, and reinforcement learning\u00a0(RL) provides a mechanism for learning in such environments. Here we present AlphaProof, an AlphaZero-inspired\n                    <jats:sup>2<\/jats:sup>\n                    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\u2019s most difficult problem. Combined with AlphaGeometry 2\n                    <jats:sup>3<\/jats:sup>\n                    , 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.\n                  <\/jats:p>","DOI":"10.1038\/s41586-025-09833-y","type":"journal-article","created":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T15:28:44Z","timestamp":1763047724000},"page":"607-613","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Olympiad-level formal mathematical reasoning with reinforcement learning"],"prefix":"10.1038","volume":"651","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2209-3933","authenticated-orcid":false,"given":"Thomas","family":"Hubert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rishi","family":"Mehta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5538-8327","authenticated-orcid":false,"given":"Laurent","family":"Sartran","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6928-7423","authenticated-orcid":false,"given":"Mikl\u00f3s Z.","family":"Horv\u00e1th","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9322-6329","authenticated-orcid":false,"given":"Goran","family":"\u017du\u017ei\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0412-4978","authenticated-orcid":false,"given":"Eric","family":"Wieser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2476-9194","authenticated-orcid":false,"given":"Aja","family":"Huang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julian","family":"Schrittwieser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yannick","family":"Schroecker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0861-5665","authenticated-orcid":false,"given":"Hussain","family":"Masoom","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8578-3216","authenticated-orcid":false,"given":"Ottavia","family":"Bertolli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2309-922X","authenticated-orcid":false,"given":"Tom","family":"Zahavy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3412-2634","authenticated-orcid":false,"given":"Amol","family":"Mandhane","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jessica","family":"Yung","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1451-9877","authenticated-orcid":false,"given":"Iuliya","family":"Beloshapka","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3476-9953","authenticated-orcid":false,"given":"Borja","family":"Ibarz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0728-4953","authenticated-orcid":false,"given":"Vivek","family":"Veeriah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8303-3674","authenticated-orcid":false,"given":"Lei","family":"Yu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7208-6307","authenticated-orcid":false,"given":"Oliver","family":"Nash","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6142-9953","authenticated-orcid":false,"given":"Paul","family":"Lezeau","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8997-8632","authenticated-orcid":false,"given":"Salvatore","family":"Mercuri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1871-426X","authenticated-orcid":false,"given":"Calle","family":"S\u00f6nne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7892-7891","authenticated-orcid":false,"given":"Bhavik","family":"Mehta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4917-5234","authenticated-orcid":false,"given":"Alex","family":"Davies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4026-8997","authenticated-orcid":false,"given":"Daniel","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4025-3953","authenticated-orcid":false,"given":"Fabian","family":"Pedregosa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3234-2505","authenticated-orcid":false,"given":"Yin","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3102-196X","authenticated-orcid":false,"given":"Ingrid","family":"von Glehn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8336-6352","authenticated-orcid":false,"given":"Mark","family":"Rowland","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1732-9198","authenticated-orcid":false,"given":"Samuel","family":"Albanie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9641-1020","authenticated-orcid":false,"given":"Ameya","family":"Velingker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simon","family":"Schmitt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8753-0765","authenticated-orcid":false,"given":"Edward","family":"Lockhart","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2434-2334","authenticated-orcid":false,"given":"Edward","family":"Hughes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8541-8112","authenticated-orcid":false,"given":"Henryk","family":"Michalewski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Sonnerat","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2812-9917","authenticated-orcid":false,"given":"Demis","family":"Hassabis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-7997","authenticated-orcid":false,"given":"Pushmeet","family":"Kohli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5197-2892","authenticated-orcid":false,"given":"David","family":"Silver","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"key":"9833_CR1","doi-asserted-by":"crossref","unstructured":"de Moura, L. & Ullrich, S. The Lean 4 theorem prover and programming language. In Automated Deduction\u2013CADE 28: Proc. 28th International Conference on Automated Deduction Proceedings (eds Platzer, A. & Sutcliffe, G.) 625\u2013635 (Springer, 2021).","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"9833_CR2","doi-asserted-by":"publisher","first-page":"1140","DOI":"10.1126\/science.aar6404","volume":"362","author":"D Silver","year":"2018","unstructured":"Silver, D. et al. A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science 362, 1140\u20131144 (2018).","journal-title":"Science"},{"key":"9833_CR3","unstructured":"Chervonyi, Y. et al. Gold-medalist performance in solving olympiad geometry with alphageometry2. J. Mach. Learn. Res. 26, 1\u201339 (2025)."},{"key":"9833_CR4","doi-asserted-by":"crossref","unstructured":"The mathlib Community. The Lean mathematical library. In Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs 367\u2013381 (2020).","DOI":"10.1145\/3372885.3373824"},{"key":"9833_CR5","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-019-0241-0","volume":"6","author":"M Dalgaard","year":"2020","unstructured":"Dalgaard, M., Motzoi, F., S\u00f8rensen, J. J. & Sherson, J. Global optimization of quantum dynamics with AlphaZero deep exploration. npj Quantum Inf. 6, 6 (2020).","journal-title":"npj Quantum Inf."},{"key":"9833_CR6","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1038\/s41586-023-06004-9","volume":"618","author":"DJ Mankowitz","year":"2023","unstructured":"Mankowitz, D. J. et al. Faster sorting algorithms discovered using deep reinforcement learning. Nature 618, 257\u2013263 (2023).","journal-title":"Nature"},{"key":"9833_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1038\/s41586-022-05172-4","volume":"610","author":"A Fawzi","year":"2022","unstructured":"Fawzi, A. et al. Discovering faster matrix multiplication algorithms with reinforcement learning. Nature 610, 47\u201353 (2022).","journal-title":"Nature"},{"key":"9833_CR8","unstructured":"Jaech, A. et al. OpenAI o1 system card. Preprint at https:\/\/arxiv.org\/abs\/2412.16720 (2024)."},{"key":"9833_CR9","doi-asserted-by":"crossref","unstructured":"Guo, D. et al. DeepSeek-R1: incentivizing reasoning capability in LLMs via reinforcement learning. Nature 645, 633\u2013638 (2025).","DOI":"10.1038\/s41586-025-09422-z"},{"key":"9833_CR10","unstructured":"Kavukcuoglu, K. Gemini 2.5: Our most intelligent AI model. Google https:\/\/blog.google\/technology\/google-deepmind\/gemini-model-thinking-updates-march-2025\/ (2025)."},{"key":"9833_CR11","unstructured":"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\u201315 (2025)."},{"key":"9833_CR12","unstructured":"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)."},{"key":"9833_CR13","unstructured":"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)."},{"key":"9833_CR14","first-page":"21573","volume":"36","author":"K Yang","year":"2023","unstructured":"Yang, K. et al. LeanDojo: theorem proving with retrieval-augmented language models. Adv. Neural Inf. Process. Syst. 36, 21573\u201321612 (2023).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR15","unstructured":"Vaswani, A. et al. Attention is all you need. Adv. Neural Inf. Process. Syst. 30, 5998\u20136008 (2017)."},{"key":"9833_CR16","doi-asserted-by":"publisher","first-page":"1092","DOI":"10.1126\/science.abq1158","volume":"378","author":"Y Li","year":"2022","unstructured":"Li, Y. et al. Competition-level code generation with alphacode. Science 378, 1092\u20131097 (2022).","journal-title":"Science"},{"key":"9833_CR17","first-page":"26337","volume":"35","author":"G Lample","year":"2022","unstructured":"Lample, G. et al. Hypertree proof search for neural theorem proving. Adv. Neural Inf. Process. Syst. 35, 26337\u201326349 (2022).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR18","unstructured":"Hubert, T. et al. Learning and planning in complex action spaces. In International Conference on Machine Learning 4476\u20134486 (PMLR, 2021)."},{"key":"9833_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.3233\/ICG-2007-30403","volume":"30","author":"R Coulom","year":"2007","unstructured":"Coulom, R. Computing Elo ratings of move patterns in the game of Go. ICGA J. 30, 198\u2013208 (2007).","journal-title":"ICGA J."},{"key":"9833_CR20","unstructured":"Zheng, K., Han, J. M. & Polu, S. MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations (ICLR) (eds Liu, Y. et al.) https:\/\/openreview.net\/forum?id=9ZPegFuFTFv (OpenReview.net, 2022)."},{"key":"9833_CR21","first-page":"11545","volume":"37","author":"G Tsoukalas","year":"2024","unstructured":"Tsoukalas, G. et al. PutnamBench: evaluating neural theorem-provers on the putnam mathematical competition. Adv. Neural Inf. Process. Syst. 37, 11545\u201311569 (2024).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR22","unstructured":"Team, G. et al. Gemini 1.5: unlocking multimodal understanding across millions of tokens of context. Preprint at https:\/\/arxiv.org\/abs\/2403.05530 (2024)."},{"key":"9833_CR23","unstructured":"Ying, H. et al. InternLM-Math: open math large language models toward verifiable reasoning. Preprint at https:\/\/arxiv.org\/abs\/2402.06332 (2024)."},{"key":"9833_CR24","unstructured":"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)."},{"key":"9833_CR25","unstructured":"Wang, H. et al. Kimina-prover preview: towards large formal reasoning models with reinforcement learning. Preprint at https:\/\/arxiv.org\/abs\/2504.11354 (2025)."},{"key":"9833_CR26","unstructured":"Ren, Z. et al. Deepseek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. Preprint at https:\/\/arxiv.org\/abs\/2504.21801 (2025)."},{"key":"9833_CR27","unstructured":"65th IMO 2024. IMO https:\/\/www.imo-official.org\/year_info.aspx?year=2024 (2024)."},{"key":"9833_CR28","unstructured":"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)."},{"key":"9833_CR29","doi-asserted-by":"crossref","unstructured":"Paulson, L. C. Isabelle: A Generic Theorem Prover (Springer, 1994).","DOI":"10.1007\/BFb0030541"},{"key":"9833_CR30","doi-asserted-by":"crossref","unstructured":"Harrison, J. HOL light: a tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design 265\u2013269 (Springer, 1996).","DOI":"10.1007\/BFb0031814"},{"key":"9833_CR31","unstructured":"Barras, B. et al. The COQ Proof Assistant Reference Manual Version 6, 17\u201321 (INRIA, 1999)."},{"key":"9833_CR32","doi-asserted-by":"crossref","unstructured":"Gonthier, G. The four colour theorem: engineering of a formal proof. In Asian Symposium on Computer Mathematics 333\u2013333 (Springer, 2007).","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"9833_CR33","unstructured":"Leroy, X. et al. CompCert: A formally verified optimizing compiler. In Embedded Real Time Software and Systems (ERTS 2016) (ed. Sifakis, J.) 1\u201310 (SEE, 2016)."},{"key":"9833_CR34","first-page":"1877","volume":"33","author":"T Brown","year":"2020","unstructured":"Brown, T. et al. Language models are few-shot learners. Adv. Neural Inf. Process. Syst. 33, 1877\u20131901 (2020).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR35","unstructured":"The Claude 3 Model Family: Opus, Sonnet, Haiku, Anthropic Technical Report (Anthropic, 2024); https:\/\/www.anthropic.com\/claude-3-model-card"},{"key":"9833_CR36","unstructured":"Team, G. et al. Gemini: a family of highly capable multimodal models. Preprint at https:\/\/arxiv.org\/abs\/2312.11805 (2023)."},{"key":"9833_CR37","unstructured":"Azerbayev, Z., Piotrowski, B. & Avigad, J. ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. In Proc. NeurIPS 2022 Workshop on MATH-AI (eds Polu, S. et al.) (2022)."},{"key":"9833_CR38","unstructured":"Jiang, A. Q., Li, W., Han, J. M. & Wu, Y. LISA: language models of isabelle proofs. In Proc. 6th Conference on Artificial Intelligence and Theorem Proving (eds Douglas, M. et al.) 63\u201365 (2021)."},{"key":"9833_CR39","unstructured":"Bansal, K., Loos, S., Rabe, M., Szegedy, C. & Wilcox, S. HOList: an environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning 454\u2013463 (PMLR, 2019)."},{"key":"9833_CR40","unstructured":"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)."},{"key":"9833_CR41","first-page":"9330","volume":"34","author":"M Wu","year":"2021","unstructured":"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\u20139342 (2021).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR42","unstructured":"Szegedy, C., Rabe, M. & Michalewski, H. Retrieval-augmented proof step synthesis. In Book of Abstracts of the 6th Conference on Artificial Intelligence and Theorem Proving (AITP 2021) (eds Hales, T. et al.) 100\u2013102 (AITP, 2021)."},{"key":"9833_CR43","first-page":"4913","volume":"35","author":"S Welleck","year":"2022","unstructured":"Welleck, S., Liu, J., Lu, X., Hajishirzi, H. & Choi, Y. NaturalProver: grounded mathematical proof generation with language models. Adv. Neural Inf. Process. Syst. 35, 4913\u20134927 (2022).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR44","first-page":"8360","volume":"35","author":"AQ Jiang","year":"2022","unstructured":"Jiang, A. Q. et al. Thor: wielding hammers to integrate language models and automated theorem provers. Adv. Neural Inf. Process. Syst. 35, 8360\u20138373 (2022).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR45","doi-asserted-by":"crossref","unstructured":"First, E., Rabe, M. N., Ringer, T. & Brun, Y. Baldur: Whole-proof generation and repair with large language models. In Proc. 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (eds Chandra, S. et al.) 1229\u20131241 (ACM, 2023).","DOI":"10.1145\/3611643.3616243"},{"key":"9833_CR46","unstructured":"Jiang, A. Q. et al. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (eds Kim, B. et al.) https:\/\/openreview.net\/forum?id=SMa9EAovKMC (OpenReview.net, 2023)."},{"key":"9833_CR47","unstructured":"Zhao, X., Li, W. & Kong, L. Subgoal-based demonstration learning for formal theorem proving. In Proc. 41st International Conference on Machine Learning (eds Salakhutdinov, R. et al.) Vol. 235, 60832\u201360865 (PMLR, 2024)."},{"key":"9833_CR48","doi-asserted-by":"crossref","unstructured":"Wang, H., Wang, W., Yue, W., Sun, X. & Wei, F. DT-Solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proc. 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) (eds Rogers, A. et al.) 12632\u201312646 (2023).","DOI":"10.18653\/v1\/2023.acl-long.706"},{"key":"9833_CR49","unstructured":"Xin, H. et al. DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. In Proc. Thirteenth International Conference on Learning Representations (eds Garg, A. et al.) (2025)."},{"key":"9833_CR50","doi-asserted-by":"crossref","unstructured":"Wang, Q., Kaliszyk, C. & Urban, J. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: Proc. 11th International Conference, CICM 2018 255\u2013270 (Springer, 2018).","DOI":"10.1007\/978-3-319-96812-4_22"},{"key":"9833_CR51","doi-asserted-by":"crossref","unstructured":"Wang, Q., Brown, C., Kaliszyk, C. & Urban, J. Exploration of neural machine translation in autoformalization of mathematics in Mizar. In Proc. 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (eds Blanchette, J. & Hri\u021bcu, C.) 85\u201398 (2020).","DOI":"10.1145\/3372885.3373827"},{"key":"9833_CR52","doi-asserted-by":"crossref","unstructured":"Wu, Y. et al. Autoformalization with large language models. Adv. Neural Inf. Process. Syst. 35, 32353\u201332368 (2022).","DOI":"10.52202\/068431-2344"},{"key":"9833_CR53","unstructured":"Agrawal, A., Gadgil, S., Goyal, N., Narayanan, A. & Tadipatri, A. Towards a mathematics formalisation assistant using large language models. Preprint at https:\/\/arxiv.org\/abs\/2211.07524 (2022)."},{"key":"9833_CR54","unstructured":"Gadgil, S., Tadipatri, A. R., Agrawal, A., Narayanan, A. & Goyal, N. Towards automating formalisation of theorem statements using large language models. In Proc. NeurIPS 2022 Workshop on MATH-AI (eds Polu, S. et al.) 1\u201315 (NeurIPS, 2022)."},{"key":"9833_CR55","first-page":"83600","volume":"37","author":"AQ Jiang","year":"2024","unstructured":"Jiang, A. Q., Li, W. & Jamnik, M. Multi-language diversity benefits autoformalization. Adv. Neural Inf. Process. Syst. 37, 83600\u201383626 (2024).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR56","first-page":"105848","volume":"37","author":"H Ying","year":"2024","unstructured":"Ying, H. et al. Lean workbook: a large-scale lean problem set formalized from natural language math problems. Adv. Neural Inf. Process. Syst. 37, 105848\u2013105863 (2024).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR57","doi-asserted-by":"crossref","unstructured":"Li, Z. et al. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In Proc. 38th International Conference on Neural Information Processing Systems 1697 (Curran Associates Inc., 2024).","DOI":"10.52202\/079017-1697"},{"key":"9833_CR58","unstructured":"Lu, J. et al. Formalalign: automated alignment evaluation for autoformalization. In International Conference on Learning Representations (eds Garg, A. et al.) https:\/\/openreview.net\/forum?id=B5RrIFMqbe (OpenReview.net, 2025)."},{"key":"9833_CR59","first-page":"24824","volume":"35","author":"J Wei","year":"2022","unstructured":"Wei, J. et al. Chain-of-thought prompting elicits reasoning in large language models. Adv. Neural Inf. Process. Syst. 35, 24824\u201324837 (2022).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR60","first-page":"15476","volume":"35","author":"E Zelikman","year":"2022","unstructured":"Zelikman, E., Wu, Y., Mu, J. & Goodman, N. STaR: bootstrapping reasoning with reasoning. Adv. Neural Inf. Process. Syst. 35, 15476\u201315488 (2022).","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"9833_CR61","unstructured":"OpenAI. OpenAI o1 system card. Preprint at https:\/\/arxiv.org\/abs\/2412.16720 (2024)."},{"key":"9833_CR62","unstructured":"OpenAI et al. Competitive programming with large reasoning models. Preprint at https:\/\/arxiv.org\/abs\/2502.06807 (2025)."},{"key":"9833_CR63","unstructured":"Jones, A. L. Scaling scaling laws with board games. Preprint at https:\/\/arxiv.org\/abs\/2104.03113 (2021)."},{"key":"9833_CR64","unstructured":"Sun, Y. et al. Test-time training with self-supervision for generalization under distribution shifts. In International Conference on Machine Learning 9229\u20139248 (PMLR, 2020)."},{"key":"9833_CR65","unstructured":"Hardt, M. & Sun, Y. Test-time training on nearest neighbors for large language models. In Proc. Twelfth International Conference on Learning Representations (eds Chaudhuri, S. et al.) (2024)."},{"key":"9833_CR66","unstructured":"Aky\u00fcrek, E. et al. The surprising effectiveness of test-time training for few-shot learning. In International Conference on Machine Learning (eds Singh, A. et al.) Vol. 267, 942\u2013963 (PMLR, 2025)."},{"key":"9833_CR67","unstructured":"Silver, D. Reinforcement Learning and Simulation-based Search in Computer Go. PhD thesis, University of Alberta (2009)."},{"key":"9833_CR68","unstructured":"Zahavy, T. et al. Diversifying AI: towards creative chess with AlphaZero. Preprint at https:\/\/arxiv.org\/abs\/2308.09175 (2023)."},{"key":"9833_CR69","unstructured":"Zuo, Y. et al. TTRL: test-time reinforcement learning. In Thirty-ninth Annual Conference on Neural Information Processing Systems https:\/\/openreview.net\/forum?id=VuVhgEiu20 (OpenReview.net, 2025)."},{"key":"9833_CR70","unstructured":"Simonds, T. & Yoshiyama, A. LADDER: self-improving LLMs through recursive problem decomposition. Preprint at https:\/\/arxiv.org\/abs\/2503.00735 (2025)."},{"key":"9833_CR71","doi-asserted-by":"crossref","unstructured":"Coquand, T. & Paulin, C. Inductively defined types. In International Conference on Computer Logic 50\u201366 (Springer, 1988).","DOI":"10.1007\/3-540-52335-9_47"},{"key":"9833_CR72","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1038\/s41586-020-03051-4","volume":"588","author":"J Schrittwieser","year":"2020","unstructured":"Schrittwieser, J. et al. Mastering Atari, Go, chess and shogi by planning with a learned model. Nature 588, 604\u2013609 (2020).","journal-title":"Nature"},{"key":"9833_CR73","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D. et al. Mastering the game of Go with deep neural networks and tree search. Nature 529, 484\u2013489 (2016).","journal-title":"Nature"},{"key":"9833_CR74","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1038\/nature24270","volume":"550","author":"D Silver","year":"2017","unstructured":"Silver, D. et al. Mastering the game of Go without human knowledge. Nature 550, 354\u2013359 (2017).","journal-title":"Nature"},{"key":"9833_CR75","doi-asserted-by":"crossref","unstructured":"P\u00f3lya, G. How to Solve It: A New Aspect of Mathematical Method (Princeton University Press, 2014).","DOI":"10.2307\/j.ctvc773pk"},{"key":"9833_CR76","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G. & Mahboubi, A. An introduction to small scale reflection in COQ. J. Formaliz. Reason. 3, 95\u2013152 (2010).","journal-title":"J. Formaliz. Reason."},{"key":"9833_CR77","unstructured":"Hasker, R. W. & Reddy, U. S. Generalization at higher types. In Proc. Workshop on the \u03bbProlog Programming Language (ed. Miller, D.) 257\u2013271 (1992)."},{"key":"9833_CR78","doi-asserted-by":"crossref","unstructured":"Heras, J., Komendantskaya, E., Johansson, M. & Maclean, E. Proof-pattern recognition and lemma discovery in ACL2. In International Conference on Logic for Programming Artificial Intelligence and Reasoning 389\u2013406 (Springer, 2013).","DOI":"10.1007\/978-3-642-45221-5_27"},{"key":"9833_CR79","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1005936130801","volume":"22","author":"E Melis","year":"1999","unstructured":"Melis, E. & Whittle, J. Analogy in inductive theorem proving. J. Autom. Reason. 22, 117\u2013147 (1999).","journal-title":"J. Autom. Reason."},{"key":"9833_CR80","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10817-020-09580-x","volume":"65","author":"T Gauthier","year":"2021","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R. & Norrish, M. TacticToe: learning to prove with tactics. J. Autom. Reason. 65, 257\u2013286 (2021).","journal-title":"J. Autom. Reason."}],"container-title":["Nature"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.nature.com\/articles\/s41586-025-09833-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.nature.com\/articles\/s41586-025-09833-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.nature.com\/articles\/s41586-025-09833-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T06:38:36Z","timestamp":1773902316000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.nature.com\/articles\/s41586-025-09833-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"references-count":80,"journal-issue":{"issue":"8106","published-print":{"date-parts":[[2026,3,19]]}},"alternative-id":["9833"],"URL":"https:\/\/doi.org\/10.1038\/s41586-025-09833-y","relation":{},"ISSN":["0028-0836","1476-4687"],"issn-type":[{"value":"0028-0836","type":"print"},{"value":"1476-4687","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"3 June 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 October 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 November 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}