At the 2024 International Mathematical Olympiad (IMO) held in Bath, England, Google DeepMind introduced groundbreaking AI programs that demonstrated remarkable capabilities in generating complex mathematical proofs. This year’s competition saw over 600 students from nearly 110 countries, while the Paris 2024 Olympic preparations unfolded in parallel.
Chinese student Haojia Shi excelled individually, securing first place with a perfect score. The U.S. team emerged as the top performer in the national rankings. However, the highlight of the event was DeepMind’s AI programs, AlphaProof and AlphaGeometry 2, which participated alongside human competitors.
The AI programs tackled four out of six problems, achieving a total score of 28 out of 42 points, a performance comparable to that of a silver medalist. This achievement was noted by mathematician and Fields Medalist Timothy Gowers, who highlighted that only around 60 human participants scored higher.
AlphaProof operates similarly to algorithms used in games like chess and Go, employing reinforcement learning. The AI iterates through multiple solutions, learning from each attempt to improve its performance. For mathematical problem-solving, AlphaProof integrates proof assistants—algorithms that validate each logical step in the solution.
Traditionally, proof assistants have been limited by the scarcity of formal mathematical data. To address this, DeepMind’s team utilized a large language model, Gemini, to translate a million problems from natural language into the Lean programming language, enabling AlphaProof to train effectively.
When faced with a problem, AlphaProof generates potential solutions and verifies them through proof steps in Lean, gradually refining its ability to handle increasingly complex mathematical challenges.
