Aristóteles: Demostración Automática de Teoremas a Nivel de la Olimpiada Internacional de Matemáticas
Aristotle: IMO-level Automated Theorem Proving
October 1, 2025
Autores: 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
Resumen
Presentamos a Aristóteles, un sistema de inteligencia artificial que combina verificación formal con razonamiento informal, logrando un rendimiento equivalente a medalla de oro en los problemas de la Olimpiada Internacional de Matemáticas del 2025. Aristóteles integra tres componentes principales: un sistema de búsqueda de pruebas en Lean, un sistema de razonamiento informal que genera y formaliza lemas, y un solucionador de geometría dedicado. Nuestro sistema demuestra un rendimiento de vanguardia con propiedades de escalabilidad favorables para la demostración automática de teoremas.
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.