Machine-checked Lean proofs for five of six 2025 IMO problems
Machine-checked Lean proofs for five of six 2025 IMO problems is graded formally verified on whataifound.org, with the AI's role graded ai-led.
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.
- Verification
- Formally verified
- Autonomy
- AI-led
- 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
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.
Sources
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 formally verified and ai-led. Full definitions are in the methodology.
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-lean