Olympiad-level Formal Mathematical Reasoning with Reinforcement Learning (AlphaProof)

TL;DR

Describes AlphaProof, an AlphaZero-style RL agent that proves competition math in the Lean theorem prover, trained on millions of auto-formalized problems with test-time RL — part of DeepMind’s silver-medal IMO result.