Machine-checked Lean proofs for five of six 2025 IMO problems
Harmonic's Aristotle produced formally verified Lean 4 proofs for five of the six 2025 IMO problems, so the gold-medal-standard score rests on a compiler rather than on human graders.
- Lab
- Harmonic
- Model
- Aristotle
- Field
- Mathematics
- Date
- 2025-07-28
What was found
Aristotle drafts an informal proof, breaks it into intermediate lemmas, formalises each in Lean 4, and iterates against the compiler's feedback, which lets it use the large natural-language corpus of mathematics while still emitting machine-checked output. Harmonic published the Lean artifacts for the 2025 problems in a public repository. The announcement came a week after the natural-language gold results from Google DeepMind and OpenAI.
Novelty check
Formal IMO results are not new (AlphaProof solved three 2024 problems in Lean), but a gold-medal-level score with a formal proof for every claimed solution had not been reported. The problems have published official solutions, so this is a capability milestone rather than new mathematics.
Caveats and known objections
Problems had to be stated formally in Lean before the system could attempt them, the same human step that capped AlphaProof's autonomy grade. Answer-construction problems require the answer to appear in the formal statement, a known weakness of formal olympiad evaluation. No IMO-certified grading and no independently enforced contest time limit. The `formal` grade covers the proofs Aristotle produced, not the claim that this equals a human gold medal.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
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 Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2025). Machine-checked Lean proofs for five of six 2025 IMO problems. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2025-07-28-aristotle-imo-leanBibTeX
@misc{whataifound-harmonic-2025-lean,
title = {Machine-checked Lean proofs for five of six 2025 IMO problems},
author = {{whataifound.org}},
year = {2025},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Harmonic. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2025-07-28-aristotle-imo-lean}
}