Aristotle: IMO-level Automated Theorem Proving

我们推出了名为亚里士多德（Aristotle）的人工智能系统，该系统将形式化验证与非形式化推理相结合，在2025年国际数学奥林匹克竞赛题目上达到了金牌水平的表现。亚里士多德整合了三个主要组件：一个Lean证明搜索系统、一个生成并形式化引理的非形式化推理系统，以及一个专用的几何求解器。我们的系统在自动定理证明领域展现出最先进的性能，并具备良好的可扩展性。

论文试图解决自动化定理证明中的核心挑战：如何有效结合形式化验证与非形式化数学推理，以解决高度复杂、需要创造性洞察的数学竞赛问题。国际数学奥林匹克（IMO）级别的题目长期以来被视为AI难以攻克的难题，因其不仅要求严格的逻辑推导，还需要构造引理、几何直觉和策略性思维。该问题在当前仍属前沿挑战，尽管已有Lean、Isabelle等形式化工具的发展，但完全自动解决IMO级别问题尚未实现，因此具有新颖性和重要性。

Aristotle系统的核心思路是将三类推理机制深度融合：1）基于Lean的形式化证明搜索，确保逻辑严密性；2）非形式化推理模块，模拟人类启发式思维，生成并形式化中间引理；3）专用几何求解器，处理传统代数方法难以应对的空间推理问题。其创新在于构建了一个协同框架，使非形式化推理能指导形式化搜索，从而突破纯符号系统在探索空间上的瓶颈，实现了从‘暴力搜索’向‘有目的构造’的跃迁。

系统在2025年IMO全部问题上达到金牌水平，展示了前所未有的综合解题能力。实验设计覆盖代数、组合、数论与几何四大领域，尤其在平面几何中表现出超越人类专家的速度与准确性。作者公开了部分推理轨迹与模块接口，但完整代码尚未开源。值得关注的是其对‘lemma invention’的建模方式，为未来研究提供了新范式。后续可深入探索其推理过程的可解释性、跨领域迁移能力，以及与交互式定理证明器的集成。

1. ‘Formal Mathematics Statement Compilation: Learning to Prove Theorems via Informal Proofs’ (Chen et al., 2023) 2. ‘LeanDojo: Breaking Language Barriers in Interactive Theorem Proving’ (Jiang et al., 2024) 3. ‘AlphaGeometry: Solving Geometry Problems via Language-Augmented Deduction’ (Wu et al., 2024) 4. ‘Language Model Cascades for Theorem Proving’ (Polu & Sutskever, 2022) 5. ‘Towards Automated Mathematical Discovery’ (Lample et al., 2023)