International Mathematical Olympiad
In plain wordsThe world's top math competition for high-school students. Because its problems demand creative written proofs, not just answers, earning a gold medal there became a famous test of AI reasoning, first passed in 2025.
AI evaluation
An annual competition, held since 1959, in which teams of up to six pre-university students from over 100 countries sit two four-and-a-half-hour papers of three problems each in algebra, combinatorics, geometry and number theory; each problem is worth 7 points (42 in all), and roughly the top twelfth of contestants win gold. Because the problems are new and demand rigorous proofs, an AI gold medal became a milestone for machine reasoning. In July 2024 Google DeepMind's AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time. and AlphaGeometryAlphaGeometry, prop. n.: A Google DeepMind system from 2024 that solves olympiad geometry problems nearly as well as top human competitors, by pairing a language model that suggests constructions with a logic engine that checks every step. 2 reached silver-medal standard (28 of 42) with formal proofs — AlphaProof's in LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs. — working from hand-translated problems for up to three days. In July 2025 an advanced Gemini Deep Think model, graded under an arrangement with the IMO, and an experimental OpenAIOpenAI, prop. n.: The American company that makes ChatGPT and the GPT models. It began in 2015 as a nonprofit research lab and is now a for-profit company overseen by a nonprofit foundation. reasoning model, graded by former medalists, each scored 35 of 42, gold-medal standard, writing natural-language proofs within the time limits; Harmonic's Aristotle and ByteDance's Seed-Prover reported formal results at gold and silver level. At the 2026 IMO in Shanghai, several AI systems were reported to achieve the first perfect scores (42 of 42), among them entries from Huawei and from Xiaohongshu (RedNote), which said its proofs were graded through the official process.
An IMO gold used to be the headline goal for math AI; now the question is research-level problems.
Origin
The first IMO was held in Romania in 1959 with seven countries. Its use as an AI target was formalized by the IMO Grand Challenge, proposed in 2019 by Daniel Selsam, Leonardo de Moura and colleagues, which asked for a system to win gold in a formal-to-formal setting in Lean. Since 2024, AI laboratories have announced results on each year's problems within days of the contest.
Usage note
Results are not strictly comparable: systems differ in formal versus natural-language output, time and compute, human translation of problems, and who graded them. OpenAI's 2025 claim, announced immediately after the contest and graded outside the official process, drew criticism, and organizers noted that they could not verify the compute or human involvement behind AI entries.
Related
- AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time.
- AlphaGeometryAlphaGeometry, prop. n.: A Google DeepMind system from 2024 that solves olympiad geometry problems nearly as well as top human competitors, by pairing a language model that suggests constructions with a logic engine that checks every step.
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
- miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- reasoning modelreasoning model, n.: An AI model trained to work through a problem step by step in hidden 'thinking' text before it answers. Letting it think longer generally makes it better at math, coding and planning.
- FrontierMathFrontierMath, prop. n.: Several hundred new math problems, kept unpublished so AI systems cannot have trained on them, written by professional mathematicians to check whether machines can do advanced, even research-level, mathematics.
- benchmark saturationbenchmark saturation, n.: When the best AI systems score so close to the maximum on a test that it can no longer tell them apart or show further progress.
Sources
- Selsam, D., de Moura, L. et al. (2019). The IMO Grand Challenge. Project website.
- Luong, T. & Lockhart, E. (2025). Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad. Google DeepMind blog, 21 July 2025.
- The Standard (Kenya) (2026). AI catches up with humans to score 100pc at top maths contest. July 2026. standardmedia.co.ke/sci-tech/article/2001553533/ai-catches-up-with-humans-to-score-100pc-at-top-maths-contest
Mentioned in
miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically., PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics.