Aristoteles: Automatisiertes Beweisen auf IMO-Niveau
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
Wir stellen Aristoteles vor, ein KI-System, das formale Verifikation mit informellem Schließen kombiniert und dabei eine Goldmedaillen-äquivalente Leistung bei den Aufgaben der Internationalen Mathematik-Olympiade 2025 erzielt. Aristoteles integriert drei Hauptkomponenten: ein Lean-Beweissuchsystem, ein informelles Schließsystem, das Lemmata generiert und formalisiert, sowie einen spezialisierten Geometrielöser. Unser System demonstriert Spitzenleistungen mit vorteilhaften Skalierungseigenschaften für das automatisierte Beweisen von Theoremen.
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.