Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning

Google DeepMind introduces AlphaProof, an AlphaZero-inspired reinforcement learning agent that learns to find formal mathematical proofs within the Lean theorem prover, achieving the first-ever medal-level performance at the International Mathematical Olympiad by solving three problems including the competition's most difficult challenge. - Auto-formalization at scale: Developed a Gemini-based auto-formalization system that translated approximately 1 million natural language mathematical problems into approximately 80 million formal Lean statements. This achieves 60% pass@1 success on representative IMO problems with particularly strong performance in algebra (81.3%) and number theory (76.9%). - AlphaZero-inspired RL with tree search: The 3-billion parameter proof network combines an encoder-decoder transformer with a specialized tree search adapted for formal theorem proving, featuring AND-OR tree structures. The main RL phase trains on the auto-formalized curriculum using a matchmaker system that adaptively assigns problems and compute budgets. - Test-Time RL for problem-specific adaptation: For intractable problems, AlphaProof employs TTRL by generating hundreds of thousands of synthetic problem variants, then running focused RL on this bespoke curriculum. This enables deep problem-specific adaptation, solving additional 15 percentage points of problems beyond extensive tree search alone. - Historic IMO 2024 achievement: At the 2024 International Mathematical Olympiad, AlphaProof solved three of five non-geometry problems, including P6 (the competition's hardest problem solved by only 5 human contestants). This combined performance scored 28 out of 42 points, achieving silver medal standard and marking the first time an AI system has attained any medal-level performance at the IMO.