AlphaProof used reinforcement learning in Lean for formal proof search, while AlphaGeometry 2 handled the geometry problem with a faster neuro-symbolic system. The 2024 workflow required experts to translate problems into formal representations and used up to several days of computation.
AlphaProof solved three non-geometry IMO 2024 problems and AlphaGeometry 2 solved the geometry problem. The four perfect solutions totaled 28/42 points, equivalent to the top end of the silver-medal range and one point below the gold threshold that year.
The result connected formal proof search with a recognizable external benchmark at medal level and became a reference point for later end-to-end natural-language olympiad systems.
Significance rationale: The combined system was reported as the first AI system to achieve medal-level performance on a full set of current IMO problems, while also exposing the practical trade-offs of manual formalization and multi-day computation.
—
—
Google DeepMind published the competition result and described external scoring by mathematicians.
The AlphaProof methodology and IMO 2024 result were published in a peer-reviewed Nature article.
No corrections recorded.
