Primary evidence
- Aristotle: IMO-level Automated Theorem ProvingS1 · Primary research · Paper · 2025-10-01
- Harmonic Aristotle IMO 2025 Lean proofsS1 · Primary research · Formal artifact
Aristotle reports gold-equivalent formal performance on IMO 2025
The architecture generates and formalizes useful lemmas, searches formal proofs and handles geometry through a specialist component.
What happened?
Aristotle reported gold-medal-equivalent performance on the 2025 IMO problems using Lean proof search, informal reasoning and a dedicated geometry solver.
Why it matters
It illustrated the emergence of integrated formal-math agents rather than single-model proof generators.
Significance rationale: Aristotle combined formal search, informal lemma generation and a geometry solver into an integrated system reported at IMO gold-equivalent performance.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Informal, Formal, Hybrid
- AI contribution
- The system coordinates informal reasoning, lemma formalization, proof search and geometry solving.
- Human contribution
- Researchers built the integrated architecture and verified formal outputs.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- aristotle, lean
- Organizations
- harmonic
- Problems
- imo-2025
- Methods
- formal-proof-search, lemma-generation, geometry-solver
Sources & artifacts
- Aristotle: IMO-level Automated Theorem ProvingS1 · Primary research · Paper · accessed 2026-09-10
- Harmonic Aristotle IMO 2025 Lean proofsS1 · Primary research · Formal artifact · accessed 2026-09-11
- Aristotle Lean statements and proofs for IMO 2025 Problems 1–5Artifact · Proof artifact
Verification history
- 2025-10-01 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.