Aristotele: Dimostrazione Automatica di Teoremi a Livello IMO
Aristotle: IMO-level Automated Theorem Proving
October 1, 2025
Autori: 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
Abstract
Presentiamo Aristotle, un sistema di intelligenza artificiale che combina verifica formale con ragionamento informale, raggiungendo prestazioni equivalenti a una medaglia d'oro sui problemi delle Olimpiadi Internazionali di Matematica del 2025. Aristotle integra tre componenti principali: un sistema di ricerca di dimostrazioni in Lean, un sistema di ragionamento informale che genera e formalizza lemmi, e un risolutore dedicato per la geometria. Il nostro sistema dimostra prestazioni all'avanguardia con proprietà di scalabilità favorevoli per la dimostrazione automatica di teoremi.
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.