Gold at the Mathematical Olympiad

The International Mathematical Olympiad is the hardest examination that teenagers sit, six proof problems over two days, and in July 2025 it was held on Australia's Sunshine Coast. Google DeepMind entered an experimental version of Gemini with what it called Deep Think, working in ordinary English rather than a formal proof language, under the same four-and-a-half-hour limits as the students. It solved five of the six problems for 35 points, a gold medal, and the organisers graded and confirmed the result on 21 July. OpenAI had announced two days earlier that an unreleased model of its own had scored the same, graded by former medallists, and was criticised for pre-empting the students' ceremony.

A year earlier DeepMind's AlphaProof had won silver in the formal language Lean, with days per problem. The 2025 result was in prose, in time, and from general-purpose reasoning models rather than a system built for mathematics.

It is on this timeline as the moment a milestone that forecasters in 2021 had put at 2030 or later was passed, and as the clearest evidence that the reasoning methods of o1 and R1 generalised. Whether a machine that proves olympiad theorems can do mathematics remained, in the profession, an argument.