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

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.