Gold at the Olympiad: what it means when a model does the maths

The International Mathematical Olympiad is a two-day examination for school students: six problems, three per day, four and a half hours a day, seven points a problem, no calculators. The 2025 edition ran on the Sunshine Coast in Australia from 10 to 20 July with 630 contestants, and the gold-medal cutoff was 35 points.^[1] Within a day of the closing ceremony two AI labs said their systems had reached it. This briefing sets out what each of them showed, what the independent tests of public models showed, and where the disagreement among mathematicians actually lies.

Two announcements, two days apart

On Saturday 19 July OpenAI's Alexander Wei posted that an experimental reasoning model had scored 35 of 42, solving five of the six problems. The conditions matched the human exam: two sessions of four and a half hours, no tools and no internet, with proofs written in natural language rather than a formal system. Three former IMO medallists graded each proof independently and finalised scores by consensus. The model, OpenAI said, was not the one it was about to release and would not be available for months.^[2]

On Monday 21 July Google DeepMind announced the same score for an advanced version of Gemini with Deep Think, and one difference that mattered: its solutions had been graded and certified by the IMO's coordinators, the people who grade the students, and the IMO's president said they had found them clear and precise. The system worked end to end in natural language inside the four-and-a-half-hour limit.^[3] A year earlier DeepMind's AlphaProof and AlphaGeometry 2 had reached silver, 28 points, but with the problems translated by hand into a formal language and with some solutions taking days of computation.^[4] Going from that to a certified gold in plain language in twelve months is the real headline of the week.

The two announcements also produced a small dispute. The IMO had asked labs to hold results until the students had had their moment; DeepMind waited for certification, OpenAI did not, and a DeepMind researcher argued publicly that under the official marking guide OpenAI's unofficial submission would have scored silver rather than gold.^[3] That claim is not testable from the outside. What is testable is that one result was certified by the competition and the other was not.

What the mathematicians said

Terence Tao, who is as close to a neutral authority as the field has, made two points over the weekend that are worth carrying. The first is that a score depends on the conditions: how much time is allowed, what tools are permitted, how many attempts are made and whether the best is selected, and how much a human steers. Change any of them and the same model produces a different number, so a result under one set of conditions cannot be lined up against a student's under another.^[5] The second is that there was no official, controlled competition for AI systems at the 2025 IMO; the labs submitted informally, with no regulation of compute or human assistance, and he hoped a controlled track would exist the following year.^[6] The sceptical end of the commentary went further, arguing that competition maths is a narrow, well-trained-for skill that says little about mathematical research.^[7] Both positions are compatible with the results being genuine.

What the public models could do

The gap between the labs' internal systems and what anyone could buy in July 2025 was large. MathArena, an independent evaluation group, ran the public models on the same paper with four human judges of IMO standard. Gemini 2.5 Pro did best at 13 points, six short of a bronze; o3, Grok 4 and DeepSeek-R1 averaged under seven; none would have medalled.^[8] A UCLA group published a paper the same week claiming that Gemini 2.5 Pro could reach five of six with a careful pipeline of self-verification and refinement around it; that was self-reported and not independently graded, and it illustrates Tao's point about conditions rather than contradicting the MathArena result.^[9] Problem 6, a combinatorics question, was solved by none of the AI systems.^[8]

Formal proofs: the other gold

A natural-language proof is checked by a human reading it. A formal proof is written in a language such as Lean and checked by software, line by line, so that if it compiles it is correct. Two systems reached gold-medal level that way in the same fortnight. Harmonic said on 28 July that its Aristotle system had produced machine-verified Lean proofs for five of the six problems.^[10] ByteDance's Seed-Prover team published a paper on 31 July describing a system that proved five of six formally, iterating on feedback from the Lean checker.^[11] Formal proofs are a stronger guarantee and a different discipline: the problem has to be stated formally first, and the output is a certificate rather than an argument a person would write. Both routes matter. The formal one is what makes a machine's mathematics trustworthy without a referee; the natural-language one is what makes it usable by a mathematician.

What this tells a business, and what it does not

Competition mathematics is close to an ideal case for a reasoning model: the problems are closed, the answers are checkable, and there is a large corpus of past problems to train on. Almost nothing a business does has those properties. A model that can hold a proof together across four and a half hours is not thereby a model that can be trusted to negotiate a contract or reconcile a ledger, and the labs did not claim it was. What does transfer is the underlying capability: sustained chains of reasoning, checking one's own intermediate steps, and recovering from dead ends. Those show up in code, in structured analysis and in planning, which is where reasoning models had already begun to earn their keep. The other thing to notice is the cost curve. In July 2025 these were unreleased, compute-heavy systems. The history of this field is that what is unreleased in July is on a price list within a year.