Aristote : Démonstration Automatisée de Théorèmes de Niveau IMO
Aristotle: IMO-level Automated Theorem Proving
October 1, 2025
papers.authors: 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
papers.abstract
Nous présentons Aristotle, un système d'intelligence artificielle qui combine la vérification formelle avec le raisonnement informel, atteignant des performances équivalentes à une médaille d'or sur les problèmes de l'Olympiade Internationale de Mathématiques de 2025. Aristotle intègre trois composants principaux : un système de recherche de preuves Lean, un système de raisonnement informel qui génère et formalise des lemmes, et un solveur de géométrie dédié. Notre système démontre des performances de pointe avec des propriétés d'évolutivité favorables pour la démonstration automatique de théorèmes.
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.