DeepMind's AlphaProof and AlphaGeometry 2 score 28 of 42 at 2024 IMO
What was demonstrated
At the 2024 International Mathematical Olympiad, a combined system of AlphaProof and AlphaGeometry 2 scored 28 points out of 42, which the operator described as the top end of silver-medal level. The gold threshold was 29 points. AlphaProof solved three of the five non-geometry problems, including the hardest problem in the competition, which the post says only five human contestants solved. AlphaGeometry 2 solved the geometry problem. The two combinatorics problems remained unsolved. The problems were manually translated by people into the Lean formal language before the systems worked on them. The post says one problem was solved within minutes and others took up to three days. Human experts scored the solutions under IMO point rules.
Why it matters
This result may suggest that a language model paired with formal proof checking can reach near-gold performance on olympiad problems. It also shows where the approach was weaker: the combinatorics problems were not solved, and the formal translation was done by hand.
Caveats
- The score was one point below the gold threshold of 29, and the two combinatorics problems were not solved.
- Problems were manually translated into Lean before solving, so the result does not show full automation from the problem statement.
- The post reports that some problems took up to three days, which is far longer than a competition sitting. It also mentions a natural-language reasoning system but gives no score for it.
- The figures come from a company announcement, not a peer-reviewed report. The DeepMind post says the methodology behind AlphaProof was later published in a Nature article dated 12 November 2025. That article was not checked for this record.
Technology profiles
Sources
- company announcement
AI achieves silver-medal standard solving International Mathematical Olympiad problems
Google DeepMind, 25 Jul 2024.
Last reviewed 21 Oct 2026.