Artificial intelligence coped with the most difficult task of the International Mathematics Olympiad

The artificial intelligence systems AlphaProof and AlphaGeometry 2 have achieved a silver medal level at the International Mathematical Olympiad (IMO) by solving four out of six problems.

The IMO is the most prestigious competition for young mathematicians, held annually since 1959. Participants devote thousands of hours to preparing for complex problems in algebra, combinatorics, geometry, and number theory. Many winners of the Fields Medal, one of the highest honors in mathematics, have competed in this olympiad.

The AI systems were evaluated by leading mathematicians: Professor Sir Timothy Gowers, an IMO gold medalist and Fields Medal recipient, and Dr. Joseph Myers, a two-time IMO gold medalist and chair of the IMO 2024 Problem Selection Committee.

Gowers noted, "The capability of the application to create non-obvious constructs is astonishing and significantly surpasses what I considered to be the current level of development."

AlphaProof solved two algebraic problems and one from number theory, determining the answer and proving its correctness. The system tackled the most difficult problem of the olympiad, solved by only five participants in the current IMO. AlphaGeometry 2 proved a geometric problem, while the two combinatorial problems remained unsolved.

AlphaProof is a system that learns to independently prove mathematical statements in the formal language of Lean. It combines a pre-trained language model with the reinforcement learning algorithm AlphaZero, which previously mastered chess, shogi, and go.

AlphaGeometry 2 is an enhanced version of the previous system. Its language model is based on Gemini and has been trained on a significantly larger set of synthetic data. This has enabled the system to tackle more complex geometric problems, particularly involving the movement of objects and equations relating to angles, ratios, or distances.

The developers continue to explore various approaches to enhancing the mathematical reasoning of AI. They aim to create a future where mathematicians collaborate with AI tools to investigate hypotheses, find new approaches to long-standing problems, and rapidly perform labor-intensive aspects of proofs.

Source: Deepmind.google