Aristotle: IMO-niveau Automatisch Bewijzen van Stellingen
Aristotle: IMO-level Automated Theorem Proving
October 1, 2025
Auteurs: Tudor Achim, Alex Best, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leister, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, Lawrence Wu
cs.AI
Samenvatting
We introduceren Aristotle, een AI-systeem dat formele verificatie combineert met
informeel redeneren, en daarmee een goudmedaille-equivalente prestatie behaalt op de
problemen van de Internationale Wiskunde Olympiade van 2025. Aristotle integreert drie
hoofdcomponenten: een Lean-bewijszoek systeem, een informeel redeneersysteem dat
lemma's genereert en formaliseert, en een toegewijde geometrie-oplosser. Ons systeem
demonstreert state-of-the-art prestaties met gunstige schaaleigenschappen voor
geautomatiseerde stellingbewijzen.
English
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.