Aristotle: Prova Automática de Teoremas em Nível IMO
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
Resumo
Apresentamos Aristotle, um sistema de IA que combina verificação formal com raciocínio informal, alcançando desempenho equivalente à medalha de ouro nos problemas da Olimpíada Internacional de Matemática de 2025. O Aristotle integra três componentes principais: um sistema de busca de provas em Lean, um sistema de raciocínio informal que gera e formaliza lemas, e um solucionador dedicado de geometria. Nosso sistema demonstra desempenho de ponta com propriedades de escalabilidade favoráveis para a prova 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.