亚里士多德：国际数学奥林匹克级别的自动定理证明

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，这是一个将形式化验证与非形式推理相结合的AI系统，在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.