Benchmark · July 25, 2024
Silver at the International Mathematical Olympiad
AlphaProof and AlphaGeometry 2 solved four problems out of six and scored 28 points out of 42, one point below the gold medal threshold.
Why it matters
A machine first got through olympiad mathematics at the level of a strong human contestant, rather than through one section of it.
AlphaProof states the problem in Lean, where every step is machine-checked, and learns by self-play: it generates candidate proofs, checks them, and reinforces on those that pass. AlphaGeometry 2 took the geometry problem. The system solved three problems completely, including the hardest, which only five human contestants managed. The caveat was time: people are given nine hours, and one problem took the system days.
Event record
- Event date
- July 25, 2024
- Timeline date
- Event date
- Verification
- Sources gathered automatically · September 18, 2026
- Lines
- ID
- evt-0306
Announcement of 25 July 2024, on the results of that year's olympiad.
Records that link to this one
- Extends Gold at the International Mathematical Olympiad
The same olympiad a year later: from silver to gold, and now without a formal language.
Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad - Enables The calculus of constructions
AlphaProof states problems in Lean, and Lean's kernel, according to its authors' 2015 paper, provides a version of the calculus of inductive constructions, citing this work.
The Lean Theorem Prover (system description) (Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer), CADE-25, LNCS 9195, 378-388AI achieves silver-medal standard solving International Mathematical Olympiad problems