DescriptionAnnounced by DeepMind in July 2024, this was the first time an AI system had reached medal-level performance on the IMO, historically considered one of the most prestigious tests of mathematical problem-solving talent for pre-university students. AlphaProof, which formalizes and searches for proofs in the Lean proof assistant using reinforcement learning, solved two algebra problems and a number theory problem (including the hardest problem of the competition, solved by only a handful of the human contestants), while AlphaGeometry 2 solved the geometry problem in 19 seconds. Neither system solved either combinatorics problem.
Formal questionGoogle DeepMind's AlphaProof and AlphaGeometry 2 systems together solved 4 of the 6 problems from the 2024 International Mathematical Olympiad, scoring 28 out of 42 possible points — one point short of the gold-medal threshold and equal to a silver-medal score — with solutions graded by official IMO methodology and reviewed by Fields medalist Timothy Gowers and IMO problem coordinator Joseph Myers.
Scope auditDoes your result fit this record?
Change a parameter to stress-test whether a proposed result is still inside the published specification. This is an audit aid, not a proof checker.
This record has no editable parameters. Read the formal question and assumptions before challenging it.
Scope matches the published specificationNo parameters changed
