AlphaProof and AlphaGeometry 2 reach silver-medal standard at the IMO
The systems scored 28 of 42 points, one short of gold, but took up to three days on some problems against the competition's 4.5-hour limit.
- Models & capabilities
- Benchmarks & progress
- Major
Google DeepMind reported that a pairing of two systems, AlphaProof and AlphaGeometry 2, solved four of the six problems set at the 2024 International Mathematical Olympiad, scoring 28 of the available 42 points. That matched the threshold for a silver medal; gold began at 29 points, a level reached by 58 of the 609 human contestants.
AlphaProof is a reinforcement-learning system that proves statements in the formal language Lean, built by pairing a pre-trained language model with the search algorithm behind AlphaZero. It solved two algebra problems and one on number theory. AlphaGeometry 2, a neuro-symbolic system built on Gemini and trained on substantially more synthetic data than its 2023 predecessor, solved the geometry problem. Both of the competition’s combinatorics problems went unsolved.
DeepMind disclosed two limitations that separated the result from a like-for-like comparison with the human competitors. The IMO problems were manually translated into formal mathematical language before being given to the systems — a step a human contestant does not need and one that itself requires mathematical judgement. And where human competitors work within two 4.5-hour sessions, some AlphaProof solutions took up to three days of computation, though one came within minutes.
Human mathematicians brought in to judge the formalised proofs described the reasoning as genuine rather than a search-and-match trick; one called a construction in the geometry solution “non-obvious” and “very impressive.” The result was among the first concrete demonstrations that reinforcement learning over formal proof search could reach competition-medal standard on problems requiring novel mathematical construction, rather than pattern-matching to seen material — a distinction that mattered because Olympiad problems are written to resist rote solution methods.
The formalisation bottleneck and the compute-time gap were the two objections raised at the time and were addressed a year later: DeepMind’s Gemini Deep Think model reached gold-medal standard at the 2025 Olympiad working directly from the natural-language problem statements within the contest time limit.