Аристотель: Автоматизированное доказательство теорем уровня IMO
Aristotle: IMO-level Automated Theorem Proving
October 1, 2025
Авторы: 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
Аннотация
Мы представляем Aristotle — систему искусственного интеллекта, которая сочетает формальную верификацию с неформальными рассуждениями, достигая уровня, эквивалентного золотой медали, на задачах Международной математической олимпиады 2025 года. Aristotle объединяет три основных компонента: систему поиска доказательств на основе Lean, систему неформальных рассуждений, которая генерирует и формализует леммы, а также специализированный решатель геометрических задач. Наша система демонстрирует передовые результаты с благоприятными свойствами масштабируемости в области автоматического доказательства теорем.
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.