one year on
DeepMind achieves silver-medal standard at International Mathematical Olympiad with AlphaProof and AlphaGeometry 2
AI systems solve four of six IMO 2024 problems, scoring 28 out of 42 points and matching the performance of a silver medalist in the competition for the first time.
Google DeepMind announced today that its AI systems, AlphaProof and AlphaGeometry 2, have achieved a silver-medal standard in the 2024 International Mathematical Olympiad (IMO), solving four of six problems and scoring 28 out of a possible 42 points. The systems score 28 points, one point shy of the gold-medal threshold; 58 of 609 contestants reach gold at 29 points.
AlphaProof, a new reinforcement-learning based system for formal math reasoning that couples a pre-trained language model with the AlphaZero reinforcement-learning algorithm, solves problems by translating natural language into the formal proof language Lean, then searching for verifiable proofs. AlphaGeometry 2, an improved neuro-symbolic system, solved Problem 4 within 19 seconds after receiving its formalization. Both systems were evaluated by prominent mathematicians including Fields Medalist Sir Timothy Gowers and two-time IMO gold medalist Joseph Myers.
Notably, AlphaProof solved the competition’s hardest problem, a feat accomplished by only five human contestants. However, the two combinatorics problems remained unsolved, and the systems took up to three days to solve the others, while students submit answers in two sessions of 4.5 hours each. The problems were manually translated into formal mathematical language for the systems to understand.
Gowers says, “The fact that the program can come up with a non-obvious construction like this is very impressive, and well beyond what I thought was state of the art.”
The record
Described the program's ability to produce a non-obvious construction as very impressive and beyond what he thought was state of the art.
One year later — open only if you can handle spoilers
DeepMind later published the AlphaProof methodology in Nature in November 2025. The one-point gap to gold would be closed in subsequent years, but the underlying question of what constitutes machine reasoning remained central to the field, with o1 and similar systems pushing the debate further.