AlphaProof

AlphaProof is DeepMind's formal-mathematics system: a pre-trained language model put through a lifelong reinforcement-learning loop in the Lean proof assistant — proving and disproving theorems, learning from verified results, getting better over time. For the 2024 International Mathematical Olympiad, a Gemini formalizer network translated ~1M informal problems into Lean statements, and the solver searched proof steps AlphaZero-style, with Lean's kernel verifying every tactic. The combined AlphaProof + AlphaGeometry 2 system scored 28/42 at IMO 2024 — silver-medal standard, one point below gold — including Problem 6, the hardest problem, solved by only five human contestants.

The achievement is real but bounded: problem statements were manually formalized by human experts, some solutions took days of compute, and the two combinatorics problems went unsolved. A full Nature paper followed in November 2025. No public weights exist — AlphaProof is a research system, not a product, but it defined the formal-RL paradigm for machine mathematics.