Aristotle: IMO-level Automated Theorem Proving
Authors: name: Tudor Achim; name: Alex Best; name: Kevin Der; name: Mathïs Fédérico; name: Sergei Gukov; name: Daniel Halpern-Leister; name: Kirsten Henningsgard; name: Yury Kudryashov; name: Alexander Meiburg; name: Martin Michelsen; name: Riley Patterson; name: Eric Rodriguez; name: Laura Scharff; name: Vikram Shanker; name: Vladmir Sicca; name: Hari Sowrirajan; name: Aidan Swope; name: Matyas Tamas; name: Vlad Tenev; name: Jonathan Thomm; name: Harold Williams; name: Lawrence Wu
Published: 2025-10-01 18:21:13

Abstract: We introduce Aristotle, an AI system that combines formal verification with
informal reasoning, achieving gold-medal-equivalent performance on the 2025
International Mathematical Olympiad problems. Aristotle integrates three main
components: a Lean proof search system, an informal reasoning system that
generates and formalizes lemmas, and a dedicated geometry solver. Our system
demonstrates state-of-the-art performance with favorable scaling properties for
automated theorem proving.