Aristotle: IMO-level Automated Theorem Proving
Artificial Intelligence
2025-10-14 v2 Computation and Language
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.
Keywords
Cite
@article{arxiv.2510.01346,
title = {Aristotle: IMO-level Automated Theorem Proving},
author = {Tudor Achim and Alex Best and Alberto Bietti and Kevin Der and Mathïs Fédérico and Sergei Gukov and Daniel Halpern-Leistner and Kirsten Henningsgard and Yury Kudryashov and Alexander Meiburg and Martin Michelsen and Riley Patterson and Eric Rodriguez and Laura Scharff and Vikram Shanker and Vladmir Sicca and Hari Sowrirajan and Aidan Swope and Matyas Tamas and Vlad Tenev and Jonathan Thomm and Harold Williams and Lawrence Wu},
journal= {arXiv preprint arXiv:2510.01346},
year = {2025}
}