AlphaProof Paper

Thu 13 November 2025

I'm very excited to finally be able to share more details about how AlphaProof works! AlphaProof is the system that we used to discover the Lean proofs for the International Mathematical Olympiad 2024, reaching silver medal performance. Our full paper Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning has now been published in Nature.

: The work described was done from the beginning of 2022 to July 2024, while I was still at Google DeepMind.

The International Mathematical Olympiad, or IMO for short, is a yearly contest in mathematics amongst the 6 ...