What was already known
AlphaProof and AlphaGeometry 2 produced formal solutions for four 2024 IMO problems, for a silver-level score. In 2025, Seed-Prover also announced gold-level formally checked performance, while Gemini Deep Think and OpenAI reported gold-level natural-language solutions. Harmonic identifies Aristotle’s distinct proof-search and lemma-formalization system as its contribution (Harmonic report, §§1, 3.1, 4).
AI involvement
Harmonic reports that people translated only the six contest problem statements; Aristotle generated the solution arguments, auxiliary lemmas and their formalizations, then used compiler feedback. Problem 3 answer candidates were generated by a language model with basic computational tools.
Harmonic reports that people manually translated only the contest problem statements; Aristotle produced proof arguments, auxiliary lemmas and their formalizations.
Importance
The result shows a separate AI system producing five complete formal solutions to known high-level competition problems.
Limitations
The source reports that people translated each original statement into Lean. The solutions are for known contest problems; no open research theorem is resolved. This review inspected the paper and repository listing but did not rebuild the Lean project or audit all dependencies.
Technical verification
Harmonic reports complete machine-checked solutions to the human-formalized statements of Problems 1–5 and publishes the Lean repository. This assessment did not rebuild or audit dependencies.
Formal checking
Harmonic reports complete Lean 4 proofs without sorryAx for Problems 1–5 and publishes the proof repository. Source-reported scope; local build and dependency audit were not done.
- Checker
- Harmonic-reported Lean 4 checker
- Scope
- Human-formalized statements of 2025 IMO Problems 1–5 and the system-generated proofs.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Harmonic’s authors explain the main devices in the non-geometry solutions, including the derangement route for Problem 1 and auxiliary definitions for Problems 3 and 5; the reviewed account gives less explanation of the geometry solution’s central mechanism.
Correction and publication history
Primary-source claim review for the What AI Found discovery index; non-notifying local inclusion.
Read this published revision