Silver-medal standard at the 2024 International Mathematical Olympiad
AlphaProof and AlphaGeometry 2 together solved four of the six 2024 IMO problems for 28 of 42 points (one short of the gold threshold), with the algebra and number-theory solutions produced and checked in the Lean proof assistant.
- Model
- AlphaProof + AlphaGeometry 2
- Field
- Mathematics
- Date
- 2024-07-25
What was found
AlphaProof, a reinforcement-learning system that works inside Lean, solved two algebra problems and one number-theory problem (including P6, the competition's hardest, which few human contestants solved), while AlphaGeometry 2 solved the geometry problem in seconds. The two combinatorics problems went unsolved. The Lean-based solutions are machine-checked by construction; the full performance was graded by mathematicians Timothy Gowers and Joseph Myers under competition-style marking.
Video explainers
Nothing loads from YouTube until you press play.
Novelty check
These are competition problems with published official solutions, so the achievement is a capability milestone (solving hard, known-answer problems under near-competition conditions) rather than a new mathematical result. The registry records it as such.
Caveats and known objections
Problems were hand-translated into formal Lean statements by people before AlphaProof attempted them, a real human contribution beyond posing the question, so autonomy is graded conservatively. AlphaProof also took far longer than the human time limit on some problems. This is benchmark performance on solved problems, not a discovery.
Independent checks
Timothy Gowers & Joseph Myers (competition-style grading): 28/42, silver-medal standard · link ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Independently checked and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Community discussion
Graded independently checked for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2024). Silver-medal standard at the 2024 International Mathematical Olympiad. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2024-07-25-alphaproof-imoBibTeX
@misc{whataifound-googledeepmind-2024-imo,
title = {Silver-medal standard at the 2024 International Mathematical Olympiad},
author = {{whataifound.org}},
year = {2024},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Google DeepMind. Verification: Independently checked. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2024-07-25-alphaproof-imo}
}