AlphaProof

"Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning." AlphaZero-inspired agent that learns to prove mathematical statements in Lean. Solved 3 of 5 non-geometry problems at IMO 2024, including the hardest problem (P6). Guarantees 100% correctness via formal verification.

Combined with AlphaGeometry 2, achieved a score equivalent to a silver medal at IMO 2024. Nature 2025. By Hubert, Mehta, Sartran et al. (DeepMind).