What happened?
In July 2024, Google DeepMind reported that two of its AI systems, AlphaProof and AlphaGeometry 2, solved four of the six problems from that year's International Mathematical Olympiad (IMO) DeepMind blog ↗. They scored 28 of 42 points, the top of the silver medal range and one point below gold DeepMind blog ↗. The solutions were scored by two outside mathematicians using official IMO rules DeepMind blog ↗.
The IMO is the hardest maths competition for school students. In 2024, 58 of 609 contestants reached the gold threshold of 29 points DeepMind blog ↗. AlphaProof solved two algebra problems and one number theory problem, including the hardest problem of the contest, which only five human contestants solved Nature paper ↗. AlphaGeometry 2 solved the geometry problem. Neither system solved the two combinatorics problems, which are about counting and arrangements Nature paper ↗.
The grading was done by Sir Timothy Gowers, a Fields Medal winner, and Joseph Myers, chair of the 2024 IMO problem selection committee DeepMind blog ↗. The full method was later published in the peer reviewed journal Nature in November 2025 Nature paper ↗. Outside experts quoted by the Science Media Centre Spain called it an excellent result while pointing to the human effort and computing power involved SMC Spain experts ↗.
What are the two systems?
AlphaProof
Writes proofs in Lean, a formal language in which a computer checks every step Nature paper ↗. It learned by reinforcement learning, meaning trial and error with rewards, on about 80 million formal problems created from about 1 million maths problems Nature paper ↗.
AlphaGeometry 2
An upgraded version of DeepMind's earlier geometry system DeepMind blog ↗. It had solved 83% of IMO geometry problems from the past 25 years, compared with 53% for the first version DeepMind blog ↗.
Because AlphaProof's proofs are written in a language a computer can check, a correct answer here is close to guaranteed, not just plausible.
Leapscope interpretation of the reported result.How did AI help?
The AI systems found the proofs themselves DeepMind blog ↗. But humans first translated the IMO problems by hand from ordinary English into formal language so the systems could work on them DeepMind blog ↗. For problems that ask for a specific answer, candidate answers were suggested by another model, Gemini 1.5 Pro, and then filtered by AlphaProof Nature paper ↗.
Figures from the Google DeepMind announcement DeepMind blog ↗ and the Nature paper Nature paper ↗.
The conditions were very different from a human contestant's. Students get two sessions of 4.5 hours; AlphaProof needed two to three days of computing on each of its hardest problems DeepMind blog ↗ Nature paper ↗. AlphaGeometry 2, by contrast, solved its problem in 19 seconds once it was formalized DeepMind blog ↗. The authors themselves say the scale of training is likely beyond the reach of most academic groups Nature paper ↗.
Which fields could this affect?
The immediate value is in maths and AI research; other uses are possible future value, and these connections are our assessment.
Formal mathematics
AlphaProof works in Lean, a tool mathematicians already use to check proofs by computer Nature paper ↗. The work shows AI can produce proofs that such a checker accepts.
Explore scienceAI research
It is a published example of reinforcement learning applied to mathematical reasoning Nature paper ↗. Other labs can learn from the method even without access to the system.
Checking software
The same kind of formal checking is used to prove that critical software behaves correctly. Whether AlphaProof style systems help there has not been shown.
Explore softwareResearch mathematics
The authors say moving from competition maths to research maths, which needs new theory, is still an open challenge Nature paper ↗. No new theorem was proved in this work.
What has been checked?
The evidence is grading by two outside mathematicians under IMO rules, plus a peer reviewed Nature paper. This was not an official IMO entry. Leapscope reviewed these sources; we did not repeat the experiments.
Shown so far
- Four of six IMO 2024 problems were solved with full marks each, for 28 points DeepMind blog ↗.
- AlphaProof's proofs are written in Lean, where a computer checks every step Nature paper ↗.
- Both combinatorics problems were left unsolved Nature paper ↗.
Still unknown
- Whether the system could solve the problems without humans first translating them into formal language SMC Spain experts ↗.
- How much faster it can become, since the hardest problems took days Nature paper ↗.
- When or whether outside researchers will get wider access; the paper mentions an interactive tool but gives no access details Nature paper ↗.
Evidence status: Research demonstration. Stage: Verified. Solutions were scored by outside mathematicians using competition rules.
From silver to a fair contest
This is our suggested way to follow the work, not a promised timetable.
Can I use it today?
Not really. You can read the Nature paper, which is open access, and the announcement Nature paper ↗ DeepMind blog ↗. AlphaProof itself has not been released as code or a public product.
A few things you might be wondering
Did the AI win a silver medal?
No medal was awarded. Its solutions scored 28 points under IMO rules, which is silver level, but they were graded by two mathematicians for DeepMind, not as an official entry DeepMind blog ↗.
Did it take the exam like a student?
No. Humans translated the problems into formal language first, and some problems took the AI two to three days DeepMind blog ↗ Nature paper ↗.
Can its answers be wrong?
AlphaProof's proofs are checked step by step by Lean, which greatly reduces the risk. One outside expert notes the guarantee depends on the formal system itself being correct SMC Spain experts ↗.
Go straight to the sources
Checked Oct 8, 2026. The first source is the original announcement or research. Later sources add independent context; background pages do not validate the result on their own.
01The developer's announcement with the score, grading and how both systems worked.
The full AlphaProof paper by Hubert and colleagues, with methods, computing costs and limitations.
Reactions from five outside mathematicians and AI researchers to the Nature paper.