AlphaProof — AI Reaches Silver-Medal Standard at the Maths Olympiad

AlphaProof is a Google DeepMind system that searches for mathematical proofs in the formal language of the Lean proof assistant. On 25 July 2024 DeepMind announced that AlphaProof, combined with the geometry specialist AlphaGeometry 2, had solved four of the six problems at the 65th International Mathematical Olympiad (IMO) in Bath, England, scoring 28 out of 42. That year's gold threshold was 29, so 28 sat at the top of the silver range. DeepMind presented it as the first time an AI had reached medal level at the IMO.

The conditions were not the same as for humans, though. Experts translated the problems by hand into Lean before the system saw them, and while one problem was solved within minutes, others took up to three days. Human contestants sit two papers of 4.5 hours each. Any account of the result needs both the silver-level headline and that gap.

The result at IMO 2024

According to the official IMO records, the 2024 olympiad was held in Bath from 11 to 22 July, with 609 contestants from 108 countries. The thresholds were 29 points for gold, 22 for silver and 16 for bronze, and 58 contestants won gold.

DeepMind's announcement says AlphaProof solved two algebra problems and one number-theory problem by determining the answer and proving it correct, including the hardest problem in the competition, which only five contestants solved. AlphaGeometry 2 proved Problem 4 within 19 seconds of receiving its formalisation. The two combinatorics problems went unsolved.

The solutions were scored under the IMO's point-awarding rules by Timothy Gowers, an IMO gold medallist and Fields medallist, and Joseph Myers, a two-time IMO gold medallist and chair of the IMO 2024 Problem Selection Committee. Gowers said: "The fact that the program can come up with a non-obvious construction like this is very impressive, and well beyond what I thought was state of the art."

How AlphaProof works: auto-formalisation and reinforcement learning

AlphaProof couples a pretrained language model with the reinforcement-learning algorithm of AlphaZero, which taught itself chess, shogi and Go. A proof written in a formal language can be checked by computer against the rules of logic. The catch is that problems and proofs written by humans in formal languages are orders of magnitude scarcer than those in natural language, the same data bottleneck that AlphaGeometry (January 2024) had faced.

DeepMind got round it with machine translation. It fine-tuned a Gemini-based large language model to turn natural-language problems into formal statements; according to the 2025 Nature paper, about a million problems became a dataset of around 80 million Lean problems. Even a translation that strays from the original is still a valid formal problem to practise on. AlphaProof trained itself by proving or disproving them, with a main reinforcement-learning phase of about 80,000 TPU-days (equivalent, the paper says, to 4,000 TPUs for 20 days).

During the contest it also used what the paper calls test-time reinforcement learning: for a problem it cannot yet solve, it generates and learns from many variants of that problem, adapting to it specifically. According to the paper, Problems 1, 2 and 6 each needed two to three days of this.

AlphaGeometry 2 is a revised version of AlphaGeometry, with a Gemini-based language model trained on an order of magnitude more synthetic data than its predecessor.

What it shows, and what it does not

For researchers in mathematical AI this was a big step. The Nature paper describes it as, to the authors' knowledge, the first medal-level performance by an AI system, achieved with multi-day computation. Because the proofs are formal, any proof the system claims can be checked mechanically by Lean, leaving little room for the hallucinations that afflict language models. In that sense it carried forward, from the AI side, the tradition of formal verification seen in the Kepler conjecture's Flyspeck project (2014).

The comparison needs caveats, however. DeepMind itself summed up the 2024 approach a year later: experts first had to translate the problems from natural language into domain-specific languages such as Lean, and the proofs back again, and it took two to three days of computation. The complete failure on the two combinatorics problems also exposed an uneven profile of strengths and weaknesses.

What changed, and for whom

From this year the olympiad became a public target for measuring AI capability. For the secondary-school students who compete, their problems were now also a stage for corporate research announcements. For mathematicians, mathematics formalised in Lean and its shared library gained value as a foundation for training and checking AI. The Nature paper places Lean and the collaborative library Mathlib on a historical arc of increasing formalisation in mathematics.

A year later, at IMO 2025, DeepMind and OpenAI announced that general-purpose models had reached gold-medal level working in natural language, without human translation, and within the time limit. AlphaProof itself returned in 2026 as a component of the research system AlphaProof Nexus. The thread continues on the AI and mathematics timeline and the DeepMind page.