AlphaProof and AlphaGeometry 2 reach IMO silver-medal standard
Google DeepMind's AlphaProof (RL + Lean formal proofs) and AlphaGeometry 2 solved 4 of 6 problems at the 2024 International Mathematical Olympiad, scoring 28/42 — silver-medal level, one point short of gold.
Key facts
- Announced 25 July 2024
- Score: 28/42 (gold cutoff was 29)
- AlphaProof solved two algebra problems and one number theory problem, including the hardest problem
- AlphaGeometry 2 solved the geometry problem
- Some problems took up to three days of compute (humans get 9 hours)
- Full AlphaProof method published in Nature on 12 Nov 2025 (RL on millions of auto-formalised problems plus test-time RL)
Science result
- Field
- mathematics / olympiad problem solving / formal proof
- Problem
- International Mathematical Olympiad 2024 problems
- Result
- Solved 4 of 6 IMO 2024 problems (28/42, one point below gold) with machine-checked Lean proofs (AlphaProof) and AlphaGeometry 2, including the hardest problem (P6).
- AI system
- AlphaProof, AlphaGeometry 2
- Human role
- Humans translated problems into Lean; proofs found autonomously (up to 3 days of compute)
- Verification
- Formal proof in Lean; graded by IMO medalists Timothy Gowers and Joseph Myers
- Status
- confirmed
- Why surprising
- Fields medallist Timothy Gowers, who graded the solutions, publicly described the result as well beyond what he had thought was the state of the art in automated theorem proving.
What happened
DeepMind's systems, operating on problems manually translated into the Lean formal language, were graded by IMO medalists.
Why it matters
First AI to reach medal level at the IMO; a year later, natural-language LLMs reached gold.
Changelog
- 2026-09-29: created
- 2026-09-29: added science block (science & math tab)
Related events
- AI systems reach gold-medal level at the International Mathematical Olympiad ★★★★★
- AlphaGeometry solves olympiad geometry near gold-medallist level without human demonstrations ★★★
- AlphaEvolve: Gemini-powered agent discovers new algorithms ★★★★
Sources (3)
- officialAI achieves silver-medal standard solving International Mathematical Olympiad problems (Google DeepMind)
- paperAlphaGeometry: Solving olympiad geometry without human demonstrations (Nature, DOI)
- paperOlympiad-level formal mathematical reasoning with reinforcement learning (AlphaProof, Nature 2025)
id: 2024-07-25-alphaproof-imo-silver · updated 2026-09-29 · open in the interactive timeline