Silver-medal standard at the 2024 International Mathematical Olympiad
Silver-medal standard at the 2024 International Mathematical Olympiad is graded independently checked on whataifound.org, with the AI's role graded ai-led.
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.
- Verification
- Independently checked
- Autonomy
- AI-led
- Lab
- Google DeepMind
- 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.
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
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 ↗
Sources
Community discussion
How this is graded
whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is independently checked and ai-led. Full definitions are in the methodology.
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-imo