亞里士多德：國際數學奧林匹克級別的自動定理證明

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

摘要

我們介紹亞里士多德，這是一個結合形式驗證與非形式推理的人工智慧系統，其在2025年國際數學奧林匹克競賽問題上達到了金牌等級的表現。亞里士多德整合了三大核心組件：一個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.