大模型让数学变得更容易，让我们提高门槛|定理|推理|数学家|计算机

让我们看看计算机辅助数学能否解决难度显著更高的问题。

作者： Marijn JH Heule

马里恩·赫勒是卡内基梅隆大学计算机科学系的副教授。他的研究方向是自动推理、可信计算和计算机辅助数学。

卡内基梅隆大学计算机科学系的副教授。他的研究方向是自动推理、可信计算和计算机辅助数学。

发布2026年8月21日

五十多年来，计算机证明从最初令人怀疑的对象，一跃成为数学确定性的黄金标准。然而，如何重新表述猜想以便计算机能够对其进行验证，一直是数学领域的一项专业技能，使得大多数数学家无法掌握这项技术。大模型（LLM）项目正在改变这一现状。我从事这个领域的工作已有十年之久，很高兴看到这一壁垒正在被打破。

有些数学问题只需简单的提示即可解决。我们是在见证新的能力，还是学习型模型（LLM）主要只是简化了计算机辅助数学运算？现在回答这个问题还为时过早，而最近的一些公告反而让这个问题变得更加复杂。让我们借此机会提高标准：选择人们真正关心的问题，发布模型，并报告哪些方面失败了，哪些方面成功了。

从不信任到验证

这段历史由两个定理构成框架。

1976 年，Appel 和 Haken 通过将四色定理简化为数千种情况并进行机械验证，证明了该定理。数学家们对此感到不安，因为证明的核心计算无法手动验证。2005 年，Gonthier 通过在 Coq 中形式化整个论证消除了这一疑虑。

1998年，海尔斯宣布证明了开普勒关于球体堆积的猜想，该证明也依赖于大量的计算。一个由12位专家组成的小组花了四年时间审查了该证明，最终表示他们有99%的把握，但无法完全验证其中的计算部分。海尔斯随后将整个证明形式化。经过约20人年的合作，该项目于2014年成功完成。

这些努力的意义远不止于解决了两个定理。此前的反对意见是，庞大的证明无法验证。形式化直接解决了这个问题。审阅论文意味着遵循作者选择记录的步骤，而证明助手则会检查每一个推导，包括数百万条几乎不可能写出来的推导。这些证明之所以无法人工验证，恰恰是机器擅长的。计算机证明从数学中最不可信的东西变成了最可信的东西，但代价极其巨大。

编码瓶颈正在消除

我的研究采用以下策略：将猜想编码为对数学对象（例如着色、团、反例）的搜索，然后让自动推理工具探索该空间。这种方法解决了其他方法难以解决的问题：舒尔数五、毕达哥拉斯三重问题以及七维凯勒猜想。

这些计算耗费了数年的 CPU 时间。一个程序运行数年后却报告说不存在这样的对象，这自然会让人质疑。幸运的是，这些工具并不会止步于给出答案。它们会生成一个证明证书，记录每一次推理过程，供检查器重放。如今，这些检查器都经过了形式化验证。这些证书非常庞大，有些甚至达到数百 TB，而且没有人会去阅读它们。但这并非质疑结果的理由。搜索本身完全可验证，无需像 Hales 的证明那样进行形式化工作。还有一个值得信赖的步骤：编码是否忠实地反映了数学原理。

几十年来，这种方法主要掌握在自动化推理专家手中。搜索技术虽然变得异常强大，但找到一种能够忠实捕捉数学本质的有效编码仍然是个挑战。这一瓶颈限制了这种方法所能解决的问题范围。

偶尔，会有数学家跨越这道障碍。2021年，吉尔斯·加达姆（Giles Gardam）通过将问题编码到SAT求解器中，反驳了卡普兰斯基的单位猜想——这个猜想自20世纪40年代以来一直悬而未决。他是一位群论学家，而非自动化推理专家。他找到的反例很小，可以手动验证，但寻找这个反例的过程却超出了人类的能力范围。他的成果之所以存在，是因为有数学家跨越了这道障碍。而这道障碍的代价，则是所有类似的成果都未能被发现。

这就是LLM最令我兴奋的地方。它们已经能够很好地将非正式数学转化为求解器可以处理的公式，并且在驱动诸如Lean之类的证明辅助工具方面表现出色。生成的编码通常远非最优，但对于许多问题而言，它们也无需最优。

许多问题的编码仍然十分困难，是整个流程中最后一个未经验证的步骤。现在，这一差距可以弥合了：对于凯勒猜想和空六边形定理，我和我的合作者们用 Lean 形式化了复杂的编码，实现了从数学陈述到最终证书的端到端验证。尽管这项工作至今仍然十分艰巨，但 LLM 已经在这方面发挥了作用。

正确还不够

人工智能公司之所以对数学感兴趣，是因为数学是解决该行业核心问题——幻觉——的理想场所。在数学中，你不能随随便便。错误的答案就是错误的。此外，数学被广泛视为推理能力的测试，因此，如果人工智能系统能够超越数学家，就能为其提供一个极具说服力的论断：他们的系统比一些最聪明的头脑还要聪明。

8月初，OpenAI发布了其Astra模型产生的10项数学成果，每一项都旨在解决或推进一个长期存在的开放性问题，这些问题至少十年来都未取得任何进展。这些成果都附有形式化描述。因此，就正确性而言，它们完全符合标准。

然而，正如《科学美国人》报道的那样，米勒认为球体堆积的改进是基于他2016年发表的一篇论文中的论点，并认为缺乏引用这种系统性的做法足以构成学术不端。福尼尔-法西奥发现另一项研究结果融合了两篇未引用论文的观点，并得出结论：这两篇论文的存在意味着该问题从未达到所谓的僵局。未能注明前人的工作是严重的错误，任何证明辅助工具都无法发现。LLM（逻辑逻辑模型）可以综合大量文献中的论点，却无法可靠地保留每个观点的来源。正确性是必要的，署名也同样重要。

不可用且未报告

数学推导可以验证，但其宣称的能力无法验证。由于模型和提示信息均已不可用，公司外部人员无法复现实验。我们也不知道问题是如何选择的，尝试了多少道题，失败了多少道题，以及总计算成本是多少。

如果失败是指经过数周甚至数月的人工努力后放弃的尝试，通常不会公开。然而，计算测试则不同。模型所针对的每个问题都已存在结果。这些失败恰恰是理解方法局限性所必需的信息。在我的领域，隐瞒这些信息是完全不可接受的。几十年来，业界一直在使用完整的基准测试套件来评估其方法，正是因为失败能够告诉我们一种方法能做什么，不能做什么。

对比一下可以进行验证的情况。2022 年，DeepMind 的 AlphaTensor 团队在《自然》杂志上发表了一篇文章，报告称他们利用强化学习找到了改进的矩阵乘法方案，并发布了这些发现的分解方法以及用于验证和基准测试的代码。不到一周，Kauers 和 Moosbauer 就通过传统的计算机搜索超越了其中一项主要结果。 5AlphaTensor 确实找到了一个新的结果，但显然，这个结果也可以通过传统的搜索方法获得。之所以能迅速纠正错误，正是因为有代码可供运行。而对于 Astra 的结果，没有人能够进行这样的比较，因此问题仍然悬而未决：这究竟是全新的能力，还是现有能力的显著简化和成本降低？

这些都不是陌生的标准。“第一证明”项目6月份的基准测试6就证明了这一点：数学家们贡献了他们自己未发表的研究成果中的题目，这些题目在测试前都经过了修复，系统在受控条件下运行，并且所有结果，包括失败的题目，都会被记录下来。

数学界花了五十年时间不断提高计算机生成结论的标准，而自动推理也同样提高了计算结果的标准。让我们用同样的标准来衡量最近的声明。

一千个加尔达姆

在向人工智能公司提出任何问题之前，我们这个群体应该承认一点：我们开发了强大的工具，却没能让其他人使用。这些工具是由专家开发，也只供专家使用。那些真正了解哪些问题至关重要的数学家却被拒之门外。Gardam 是个例外，它揭示了我们正在失去什么。

我们未能做到的事，LLM 正在做到。我们未能降低的门槛正在降低，而且降低速度很快。所有要素首次齐备：能够穷举搜索并证明其搜索结果的求解器、能够检查每一条推论的证明辅助工具，以及现在能够将非正式数学问题导入这套机制的模型，供任何想尝试的人使用。

即使这些底层功能并非全新，但让每位数学家都能使用它们也将带来变革。试想一下，如果有1000个Gardam，每个人都用这些工具研究自己最擅长的问题，并汇报成功与失败。一年下来，这比任何精心策划的公告都更有价值。

这就是我想看到的实验。计算机辅助数学已经变得极其容易。现在让我们看看它能否解决难度更高的问题。

https://cacm.acm.org/blogcacm/llms-make-mathematics-easier-now-raise-the-bar/

参考文献

1. Heule, MJH 和 Kullmann, O. 蛮力科学。通讯60, 8 (2017), 70–79。

2. Gardam, G. 群环单位猜想的一个反例。数学年鉴194, 3 (2021), 967–979。

3. Szeider, S. 通过模型上下文协议连接语言模型和符号求解器。SAT 2025，LIPIcs卷 341，30:1–30:12。