Harmonic团队开发的Aristotle：IMO数学竞赛金牌水平的自动定理证明系统

这项由Harmonic团队开发的突破性研究成果发表于2025年10月，论文编号为arXiv:2510.01346v1。感兴趣深入了解的读者可以通过该论文编号查询完整的技术细节和实验数据。

在人工智能的众多应用领域中，数学推理一直被认为是最具挑战性的任务之一。毕竟，数学不仅需要逻辑思维，还需要创造性的洞察力。然而，Harmonic团队最近开发的一个名为Aristotle的人工智能系统，竟然在2025年国际数学奥林匹克竞赛中达到了金牌水平的表现，成功解决了6道题目中的5道。这就像是让一个机器人参加高考数学考试，不仅答对了大部分题目，而且每个答案都能通过最严格的数学验证。

Aristotle系统的独特之处在于它不仅能解题，还能生成完全符合数学严格标准的正式证明。这意味着它的每一步推理都经过了计算机的严格验证，就像是每道菜都经过了最挑剔的美食评委的认可。传统的数学证明往往依赖人类的直觉和经验，而Aristotle则将这种直觉与机器的精确性完美结合。

这个系统由三个主要部分组成，它们协同工作就像一个精密的乐团。第一个组成部分是基于Lean编程语言的证明搜索算法，它使用蒙特卡洛图搜索技术，配备大型变换器作为策略和价值函数。这个组件就像一个极其细致的侦探，能够在庞大的证明空间中寻找正确的推理路径。第二个部分是基于引理的非正式推理系统，它能生成数学陈述的非正式证明，将这些证明分解为引理，并将每个引理形式化为Lean语言。这个过程类似于将复杂的烹饪过程分解为一个个简单的步骤，每个步骤都能被精确执行。第三个部分是专门的几何求解器，它使用基于AlphaGeometry的方法在Lean环境之外解决平面几何问题。

在2025年国际数学奥林匹克竞赛的评估中，Aristotle展现出了令人瞩目的表现。该系统成功解决了代数、数论、几何和组合数学等各个领域的问题，只有最后一道被普遍认为是最困难的问题没有解决。更重要的是，与其他也达到金牌水平的人工智能系统不同，Aristotle提供的是经过严格验证的正式解答，而不是仅仅用自然语言描述的解题思路。

一、突破性的混合推理架构

Aristotle的核心创新在于它将两种截然不同的推理方式巧妙地结合在一起。一方面，它具备人类数学家那样的直觉性思维，能够理解问题的本质，提出创新的解题思路。另一方面，它又具备计算机那样的严谨性，确保每一步推理都经得起最严格的逻辑检验。

这种混合架构的工作原理就像是一个经验丰富的建筑师与一个精确的工程师合作建造大楼。建筑师负责构思整体设计方案，提出创新的建筑理念，而工程师则负责将这些创意转化为精确的施工图纸，确保每个细节都符合物理定律和安全标准。在Aristotle系统中，非正式推理部分扮演着建筑师的角色，它能够理解数学问题的深层含义，提出解题的大致思路。正式证明搜索部分则像工程师一样，将这些思路转化为严格的数学证明。

这种设计的巧妙之处在于它充分利用了两种推理方式的优势。人类的数学直觉往往能够跳跃式地发现问题的关键所在，但这种直觉有时会出错或不够严谨。计算机的逻辑推理虽然严格可靠，但往往缺乏创造性的洞察力。Aristotle通过让这两种方式相互补充，既保持了创造性，又确保了准确性。

在实际工作过程中，系统首先使用非正式推理来理解问题并生成解题思路。这个过程就像是数学家在草稿纸上涂涂画画，尝试不同的方法和思路。然后，系统会将这些思路转化为一系列更小的、更容易证明的引理。这就像是将一个复杂的烹饪过程分解为许多简单的步骤，每个步骤都能够独立完成和验证。

二、蒙特卡洛图搜索的证明发现机制

Aristotle的证明搜索算法采用了一种名为蒙特卡洛图搜索的技术，这种技术最初在围棋人工智能中大放异彩。就像围棋选手需要在每一步棋中考虑无数种可能的走法一样，数学证明也需要在每一步推理中选择最合适的策略。

这个搜索过程可以比作一个探险家在茂密的森林中寻找宝藏。森林中有无数条小径，每条小径都可能通向目标，但也可能是死胡同。探险家不能盲目地尝试每一条路径，因为时间和资源都是有限的。聪明的做法是根据已有的经验和线索，优先探索那些看起来最有希望的路径。

Aristotle的搜索算法正是采用了这样的策略。它使用一个大型神经网络来评估每个推理步骤的"希望值"，就像探险家根据地形和天气来判断哪条路径更有希望成功。当系统遇到一个需要证明的数学陈述时，它会生成多个可能的证明策略，然后根据这些策略的成功概率来分配搜索资源。

这种方法的优势在于它能够在庞大的搜索空间中高效地找到正确的证明路径。传统的证明搜索方法往往采用暴力搜索，就像是在森林中毫无目标地乱闯。而Aristotle的方法更像是一个经验丰富的向导，知道如何根据蛛丝马迹找到正确的方向。

在搜索过程中，系统还采用了一种称为"图搜索"的技术。这意味着当系统发现两条不同的推理路径实际上到达了相同的中间状态时，它会将这些路径合并，避免重复工作。这就像是发现森林中的两条小径最终汇合到同一个地点，那么探险家就不需要重复探索相同的区域。

三、引理生成与形式化的创新流程

Aristotle系统最令人印象深刻的能力之一是它能够自动生成和形式化数学引理。这个过程就像是一个经验丰富的厨师将复杂的菜谱分解为一系列简单易懂的步骤，每个步骤都有明确的目标和具体的操作方法。

这个流程的第一步是生成问题的非正式证明。系统会像人类数学家一样，用自然语言描述解题的总体思路和关键步骤。这个阶段充满了创造性，系统需要理解问题的本质，找到合适的数学工具和技巧。这就像是建筑师在设计建筑时，首先要理解客户的需求，然后构思整体的设计方案。

接下来，系统会将这个非正式证明分解为一系列相互关联的引理。每个引理都是一个相对简单的数学陈述，它们组合在一起就能够支撑整个证明。这个过程类似于将一个宏大的建筑项目分解为许多具体的施工任务，比如挖掘地基、浇筑混凝土、安装钢筋等等。每个任务都有明确的目标和可行的执行方案。

然后，系统会将每个引理的陈述转化为Lean编程语言的正式表达。Lean是一种专门用于数学证明的编程语言，它要求每个数学概念和逻辑步骤都必须严格定义。这个转化过程就像是将建筑师的设计图纸转化为工程师的施工图，每个细节都必须精确无误。

在这个过程中，系统还会与Lean编译器进行交互，及时发现和纠正形式化过程中的错误。当编译器报告某个引理的陈述有语法错误或逻辑问题时，系统会自动修正这些问题。这种反馈机制确保了生成的引理既符合数学逻辑，又符合Lean语言的严格要求。

最后，系统会使用前面提到的证明搜索算法来逐一证明这些引理。已经证明的引理可以作为后续证明的基础，就像是建筑工程中已完成的部分可以为后续工作提供支撑。如果某些引理无法证明，系统会重新修改和完善引理的陈述，或者生成新的辅助引理。

四、专门的几何问题解决方案

几何问题在数学竞赛中往往具有独特的挑战性，它们需要空间想象能力和几何直觉，这些能力很难直接转化为纯粹的代数运算。因此，Aristotle系统专门开发了一个基于AlphaGeometry技术的几何求解器，名为Yuclid。

Yuclid的工作原理就像是一个极其精密的工程制图软件。当面对一个几何问题时，它首先会构建一个数值化的几何图形，将所有的点、线、角度等几何元素转化为精确的数值表示。这就像是将一个手绘的建筑草图转化为计算机辅助设计的精确图纸。

然后，Yuclid使用一种称为演绎数据库和代数推理的混合方法来解决问题。演绎数据库部分负责管理几何关系和定理，就像是一个包含所有几何知识的巨大图书馆。当系统需要使用某个几何定理时，它可以迅速从这个"图书馆"中找到相关的信息。代数推理部分则将几何关系转化为代数方程组，然后使用高斯消元法等数值方法来求解。

Yuclid的一个重要创新是它的性能优化。传统的几何求解器往往速度较慢，无法在合理的时间内处理复杂的问题。Yuclid通过多种技术优化，将运行速度提高了数百倍。这些优化包括数值规则匹配、语句去重、代数推理优化和内存管理等方面。

数值规则匹配技术能够在运行主要推理循环之前，快速找到所有在数值上匹配的规则。这就像是在烹饪前预先准备好所有需要的食材和调料，避免在烹饪过程中临时寻找。语句去重技术则确保系统不会重复证明相同的几何陈述，这类似于避免重复做相同的工作。

代数推理部分使用高斯消元法来解决线性方程组，并通过多种优化技术来避免重复计算。系统会存储当前的阶梯形式，每当建立新的陈述时就更新这个形式。对于每个待证明的陈述，系统还会存储其当前的简化形式，这样下次尝试证明相同陈述时就可以从上次的进度开始。

五、在国际数学奥林匹克竞赛中的卓越表现

2025年国际数学奥林匹克竞赛包含了六道涵盖代数、数论、几何和组合数学的题目。Aristotle系统在这次竞赛中的表现堪称突破性，它成功解决了其中的五道题目，达到了金牌水平的标准。更重要的是，这些解答都是经过严格验证的正式证明，而不是仅仅用自然语言描述的解题思路。

在第一道题目"阳光线问题"中，Aristotle展现了它独特的创造性思维。这道题目涉及通过三角形内格点的直线问题，大多数人类数学家的解法都会使用这样的事实：一条直线最多只能穿过凸体的两条边。虽然这个事实在几何上很直观，但在Lean语言中形式化和证明却相当复杂。Aristotle选择了一个完全不同的方法，它开发了一个更加代数化的证明，研究了问题中隐含出现的某些错位排列。最终，它通过检查n等于5的具体情况找到了一个明确的反例，从而排除了所有更大n值的构造。

第三道题目"Bonza函数"要求刻画满足特定同余关系的函数。在解决这个问题的早期阶段，Aristotle开始用一个特定的集合S来刻画这些函数，它将S定义为所有质数p的集合，使得f(p)大于1。这个集合在最终的几个引理证明中都有使用，但它并不是问题陈述直接定义或建议的。这展示了Aristotle定义和使用新的辅助定义的能力，就像人类数学家会做的那样。

第四道题目涉及正除数的递归关系序列。Aristotle开发的论证使用了与典型人类解答相同的逻辑，但在形式化过程中展现了它纠正非正式推理中错误的能力。在Aristotle的一个非正式证明中，推理在严格递减序列、弱递减序列和在某点递减的序列之间产生了混淆，在周围的文本中将所有这三种情况都称为"递减序列"。这种微妙的语言错误很好地体现了验证人工智能生成的自然语言证明的挑战。然而，在随后的形式化过程中，Aristotle修复了这个错误，使用了有缺陷的非正式证明中的关键思想，但根据需要填补了逻辑空白。

第五道题目"Inekoalaty游戏"需要识别两个玩家在特定游戏中的最优策略，并证明在什么条件下它们能强制获胜和平局。Aristotle不仅识别了适当的策略并在Lean中形式化了它们的定义，还引入了与证明相关但问题陈述本身并未建议的辅助定义。具体来说，它定义了函数f(k) = k√2/(2k-1)，这在证明过程中成为了一个有用的不变量。

在这个问题中，Aristotle还展示了它对超越国际数学奥林匹克竞赛所需概念的高级主题的熟练程度。它对引理lemBazzaObjectiveUpperBound的初始证明使用微积分来从另一个辅助量Φ(k,q) = √((k-1)q) + √(2k-q)的极值中获得某个有用的上界，通过计算关于q的导数。后来，它用使用nlinarith策略的更直接的证明替换了这个基于微积分的证明。另一个例子是它意外地使用了filter_upwards策略，这个策略用于过滤器的操作，通常不在本科数学课程中出现，但在Mathlib中用于极限的底层定义。

六、在实际数学研究中的重要贡献

除了在竞赛数学中的出色表现外，Aristotle还在实际的数学研究中做出了重要贡献。在训练过程中，这个系统证明了几个Mathlib中缺失的重要定理，包括尼文定理、高斯-卢卡斯定理、特征值是特征多项式根的事实，以及其他技术引理。这些贡献展示了Aristotle在解决实际数学问题方面的实用价值。

Mathlib是Lean编程语言的数学库，包含了大量已经形式化的数学定理和定义。Aristotle能够为这个库贡献新的定理，说明它不仅能够解决人为设计的竞赛问题，还能够在真正的数学研究中发挥作用。这就像是一个新的研究员不仅能够通过考试，还能够为科学知识的积累做出实质性的贡献。

更令人印象深刻的是，Aristotle还解决了涉及本科生甚至研究生水平数学的问题。研究团队提供了两个例子，展示了它证明涉及同调代数和艾森斯坦级数的基本陈述的能力。这些主题远远超出了竞赛或本科水平的数学，表明Aristotle具有更广泛的数学推理能力。

Aristotle还为其他几个开源项目做出了贡献。它为多项式Freiman Ruzsa形式化项目贡献了两个引理，还为广义量子斯坦因引理项目贡献了几个引理。这种跨项目的贡献能力表明Aristotle具有适应不同数学背景和符号系统的灵活性。

在一个特别有趣的案例中，Aristotle被用来验证陶哲轩的基于Lean的实分析教科书的重要部分。在处理该书的几个章节时，Aristotle发现了四个错误的练习题，并提供了明确的反例。对于所有其他呈现给它的练习，Aristotle都能够证明，并且对于其中两个练习，它注意到给学生的假设之一对于完成证明是不必要的。这个例子展示了Aristotle作为数学验证工具的潜在价值，它能够发现人类可能忽略的错误和冗余假设。

七、测试时训练的动态学习能力

Aristotle系统的一个重要特性是它的测试时训练能力，这使得它能够在推理过程中从自己的经验中学习。这种能力就像是一个学生在考试过程中不断总结经验，调整解题策略，而不是仅仅依赖考前的准备。

这个动态学习过程包含两个交替进行的步骤。首先，系统会尝试解决主要问题以及由外部推理循环生成的许多引理。然后，如果主要问题仍未解决，系统会基于这些尝试中提取的搜索轨迹重新训练模型。这就像是一个研究者在解决复杂问题时，会根据每次尝试的结果调整研究方法和思路。

在国际数学奥林匹克竞赛之前和期间，研究团队观察到测试时训练既提高了Aristotle在给定问题上尝试的效率，也增强了它的专门化能力。在竞赛之前，他们发现使用测试时训练使Aristotle能够在相同的搜索预算下解决原本无法解决的困难问题。测试时训练还与Aristotle的引理生成流程特别有建设性的相互作用，允许来自不同证明草图的引理之间的交叉传播，并加速了Aristotle在评估期间处理引理的速度。

另一个方向是，测试时训练有助于处理新的Lean抽象概念，或者Mathlib中不常见的抽象概念，这些概念只有基本的应用程序接口。证明涉及这些概念的陈述需要以临时方式从复杂的基本命令链中合成更高级的构造。测试时训练在允许模型从其以这种方式链接基本命令的初始尝试中学习方面是无价的，有效地让它在后续尝试中访问更强大的应用程序接口。

这种学习能力的重要性在于它使Aristotle能够适应具体问题的特殊性。每个数学问题都有其独特的特点和挑战，通用的方法可能不是最有效的。通过测试时训练，Aristotle能够为特定问题开发专门的技能和策略，就像专业运动员会针对特定对手调整训练计划一样。

八、与其他系统的比较和技术路线

在达到国际数学奥林匹克竞赛金牌水平的人工智能系统中，Aristotle并不是唯一的一个。ByteDance公司最近也发布了一个名为Seed-Prover的系统，同样在2025年国际数学奥林匹克竞赛中达到了金牌水平的正式解答。OpenAI和Google DeepMind也发布了达到金牌水平表现的系统，但它们提供的是自然语言解答而不是正式解答。

这些系统之间的一个重要差异在于它们采用的技术路线。Seed-Prover和Aristotle都具有一些共同元素，比如几何问题的专门子系统、非正式推理与正式反馈的结合、问题分解为引理和猜想，以及使用已解决的引理作为后续推理的上下文。这种趋同演化表明，使用自然语言推理将问题分解为更简单的子问题，结合基于Lean编译器正式反馈的强化学习，是实现高水平正式数学推理的关键工具。

Seed-Prover和Aristotle之间最根本的差异在于，Seed-Prover为给定的正式陈述生成完整的证明，然后迭代地改进它直到被Lean编译器验证，而Aristotle使用非正式推理模型来指导树搜索，一次开发一步证明。值得注意的是，两种方法都在同一时间达到了金牌水平的国际数学奥林匹克竞赛表现。实际上，在过去两年中，其他自动定理证明基准的领先者在逐步和整体证明系统之间来回变换。

OpenAI使用的是通用推理模型，DeepMind使用的是为数学推理进行微调的Gemini Deep Think的高级版本。这些都是前沿模型推理能力的令人印象深刻的演示。然而，验证复杂的自然语言证明对人类来说几乎与创建证明一样具有挑战性，因此研究团队继续相信，开发正式验证的自动数学推理对于数学和科学研究中的潜在应用至关重要。

九、未来发展前景和潜在影响

Aristotle系统的成功不仅仅是人工智能技术的一个里程碑，更重要的是它预示着数学研究和教育领域即将发生的深刻变革。这种变革的影响范围远远超出了数学竞赛的范畴，可能会重塑整个科学研究的方式。

在数学研究方面，Aristotle这样的系统可能会成为数学家们的重要助手。复杂的数学证明往往需要处理大量繁琐的细节，这些细节虽然重要但往往会分散研究者对核心思想的注意力。有了Aristotle这样的助手，数学家们可以专注于提出创新的想法和整体的证明策略，而将具体的形式化和验证工作交给机器来完成。这就像是有了一个永不疲倦、极其细致的助理，能够帮助处理所有的文书工作和细节检查。

在数学教育领域，这种技术也可能带来革命性的变化。学生们可以使用这样的系统来验证自己的数学推理，获得即时的反馈和指导。这不仅能够提高学习效率，还能够帮助学生培养更严谨的数学思维。传统的数学教育往往依赖教师的主观判断，而这种系统提供的是绝对客观和准确的评价。

在更广泛的科学研究中，正式验证的重要性正在日益凸显。随着科学研究变得越来越复杂，人为错误的风险也在增加。Aristotle这样的系统能够确保推理过程的每一步都是正确的，这对于需要高度可靠性的科学领域（如医学研究、工程设计等）具有重要意义。

然而，这种技术的发展也带来了一些需要思考的问题。随着机器在数学推理方面变得越来越强大，人类数学家的角色可能会发生变化。未来的数学研究可能更多地依赖于人机协作，而不是纯粹的人类创造力。这种变化既带来了机遇，也带来了挑战。

从技术发展的角度来看，Aristotle的成功表明了将不同人工智能技术有机结合的重要性。它的成功不是依靠某一种单一的技术突破，而是通过巧妙地组合搜索算法、神经网络、符号推理等多种技术实现的。这种混合方法可能会成为未来人工智能发展的一个重要方向。

说到底，Aristotle系统的出现标志着人工智能在数学推理领域达到了一个新的高度。它不仅能够解决复杂的数学问题，还能够提供经过严格验证的证明，这在以往是只有最优秀的人类数学家才能做到的事情。虽然机器还无法完全替代人类的创造力和直觉，但它们已经成为了强有力的助手和工具。

对于普通人来说，这项技术的发展意味着未来我们可能会有更加智能和可靠的数学辅导系统，更加精确的科学研究工具，以及更加严谨的逻辑推理助手。虽然我们可能永远不会直接使用这样的高级系统，但它们的影响将通过各种应用程序和服务渗透到我们的日常生活中。这就像互联网技术最初只是科研机构使用的工具，但最终改变了每个人的生活方式一样。Aristotle的出现预示着一个更加智能、更加精确的未来正在向我们走来。

Q&A

Q1：Aristotle是什么？它和其他AI数学系统有什么不同？

A：Aristotle是由Harmonic团队开发的AI自动定理证明系统，它在2025年国际数学奥林匹克竞赛中达到了金牌水平。与其他系统最大的不同是，Aristotle提供的是经过计算机严格验证的正式数学证明，而不是仅仅用自然语言描述的解题思路，这意味着它的每一步推理都经过了最严格的逻辑检验。

Q2：Aristotle怎么解决数学问题的？它的工作原理是什么？

A：Aristotle采用三部分协同工作的架构。首先用非正式推理理解问题并生成解题思路，就像数学家在草稿纸上构思一样。然后将复杂问题分解为简单的引理，每个引理都能独立证明。最后使用蒙特卡洛图搜索算法在庞大的证明空间中寻找正确路径，就像有经验的探险家根据线索找到宝藏一样。

Q3：普通人能使用Aristotle吗？这个技术对我们有什么影响？

A：目前Aristotle还不是面向普通用户的产品，但可以在Harmonic公司网站注册早期体验。这项技术的影响是深远的：未来我们可能有更智能的数学辅导系统、更精确的科学研究工具，就像互联网最初只是科研工具但最终改变了每个人的生活一样。