Olympiad-level formal mathematical reasoning with reinforcement learning (www.nature.com)

Researchers introduced AlphaProof, an AlphaZero-inspired reinforcement learning agent that learns to construct formally verified proofs in the Lean theorem prover by training on millions of auto-formalized problems. Using a policy/value network with search-like RL (AlphaZero-style) and a novel Test-Time RL procedure—where millions of related problem variants are generated and used to adapt at inference—the system substantially improves state-of-the-art formal reasoning. AlphaProof, combined with a geometry component (AlphaGeometry), solved three of five non-geometry problems at the 2024 IMO, including the hardest problem, and achieved overall performance equivalent to an IMO silver medallist after multi-day computation—marking the first time an AI reached medal-level performance in that competition. Significance lies in demonstrating that grounded learning in an interactive formal environment can yield complex, verifiable mathematical reasoning strategies beyond pattern-matching LLMs. Key technical innovations are large-scale auto-formalization to convert natural problems into Lean, RL training on millions of formal problems, and Test-Time RL for deep problem-specific adaptation. Benchmarks and supplementary material (PutnamBench proofs, hyperparameters, pseudocode) show robust gains but also highlight heavy compute costs and remaining challenges in generalization and efficiency. The work points toward reliable, formally verified AI assistants for advanced mathematics while underscoring practical limits around resource intensity and autoformalization quality.