AI自动验证数学证明的技术突破

当AI开始核查数学家的工作

数学领域可能即将迎来一个新时代——这也是许多研究者长久以来的愿望。数学家们很快就能借助计算机快速且严谨地验证证明，确保已发表的证明正确无误，并为后续进展奠定基础。这样的工具可以帮助专家应对数学研究日益加快的步伐和不断增加的数量。

能够核查数学论证（如证明）的计算机程序已经存在了几十年。但将人工编写的证明转换成计算机严格的编程语言——这是用现有工具验证证明的前提条件——极其耗时。这种称为“形式化”的转换有时需要数月甚至数年。

随着首个大语言模型的发展，数学家们的希望燃起：或许有朝一日机器可以自动完成这种转换。然而，与人类语言不同，形式化编程语言不允许任何偏差，每个术语、符号和引用都必须精确定义。

如今，一家名为“某机构”的初创公司报告称在证明形式化方面取得了初步成功。其名为“Gauss”的人工智能已经成功形式化了数学家Maryna Viazovska提出的与高维空间中球体排列相关的两项复杂证明。Viazovska于2022年因其中一项证明获得菲尔兹奖。然而，数学界对Gauss形式化结果的反应较为冷淡，部分原因是该项目并未像许多专家希望的那样展开。随着其他AI与数学相结合的初创公司也在探索形式化，这一案例为数学家们在不远的未来可能面临的情况提供了线索。

堆积难题

2016年，Viazovska通过解决一个困扰数学界数十年的难题而成为核心人物：如何以最节省空间的方式排列球体？要找到唯一的最高效空间解决方案，必须首先证明其他无限多种球体排列方式都需要更多空间。直到1998年，人们才证明金字塔形排列——就像超市里堆放的橙子——确实是三维空间中的最密堆积方式。

但在更高维度中，球体排列变得极其复杂，因为存在更多排列方式和对称性。Viazovska使用了一个特别优雅的解法，该解法仅存在于八维和二十四维空间中：将三维空间中最节省空间的排列方式转移到这些高维空间，然后证明转移过程中产生的间隙恰好足以在每个间隙中容纳一个额外的球体。

她首先攻克了八维空间的证明，并因此获得2022年菲尔兹奖。她的同事、某机构数学家Henry Cohn说服她与几位合作者——包括某机构的Stephen Miller、某机构的Danylo Radchenko以及某机构的Abhinav Kumar——共同开发二十四维空间的证明。他们在一周内就取得了成功。

但这些证明能否被计算机形式化和验证呢？2023年，Viazovska结识了Sidharth Hariharan，当时他正在某机构攻读数学硕士学位，并参与一个名为Lean的形式化项目。他们开始交流想法。“我们只是两个好奇的人，想学点东西——事情就是这样开始的，”他说。

两人决定通过将Viazovska证明中引用的每个术语、定义和定理都转换成Lean代码来实现形式化。他们与同事合作，于2025年6月推出了一个网站来记录他们的形式化项目。团队将Viazovska的原始工作分解成许多小的子任务，在线记录下来，并提供协作，以便更大的Lean社区可以认领并处理某个子任务。

与此同时，数学家Auguste Poiroux（某机构博士生）于2025年夏末帮助创立了某机构。“我们希望实现自动将论文或书籍的内容转换为Lean代码并立即检查，”Poiroux解释道。

该机构注意到了Hariharan及其同事的项目并取得了联系。“2025年秋季，该机构的人告诉我们，他们已经成功形式化了我们项目的较小部分，并与我们分享了一些结果，”现为某机构博士生的Hariharan回忆道。“但之后联系就中断了。我们不知道他们进展到哪一步了——甚至不知道他们是否还在做这个项目。”

“我们当时是个很小的团队，”Poiroux说。“我们意识到无法同时改进系统和处理Hariharan的项目。所以我们专注于AI。”在接下来的几周里，该机构的团队成员进一步开发了他们的基于智能体的语言模型，命名为Gauss。

最终，该软件似乎能够将数学著作转换为Lean代码，并在无需人工干预的情况下自动检查。“我们把Viazovska的八维证明作为测试，”Poiroux说。“突然，系统输出了完整的形式化证明。这完全出乎我们的意料。”

数学的未来

Poiroux和他的同事们非常兴奋。Hariharan的团队则不然。“至少可以说，我们非常惊讶，”Hariharan说。“那是我们的项目，我们投入了两年多的努力——然后某机构把它解决了。”

Hariharan和他的同事们曾计划将部分形式化工作作为一名本科生毕业论文的基础。“但我想事情就是这样。AI具有颠覆性，”Hariharan说。

“兴奋之余，我们没有充分考虑后果，”Poiroux说。“我理解，从外部看，可能显得我们故意隐瞒了进展。未来我们一定会更加谨慎。”

随后，该机构攻克了Viazovska的第二个证明，该证明涉及二十四维空间中的最优球体堆积。“这一次，我们只把论文给了Gauss，没有别的，”Poiroux说。“系统将其转换成了大约12万行Lean代码。”该代码随后已被验证。

该机构目前正与Hariharan及其他专家合作，进一步推进自动形式化，并覆盖更多数学领域。“对于许多领域，Lean中仍然缺少基础模块——我们目前还无法形式化那些领域的证明，”Poiroux说。

当数学的大部分领域都能够被形式化时，新的可能性将随之开启。该机构的系统不仅仅是翻译机器：它们能够检测并纠正论文中的小错误，这一能力暗示了一种潜在的前景——更高级的AI将监督整个数学领域，甚至在研究中超越人类。

“当我们的模型完整地理解数学时，它们可以以完全不同的方式思考数学，”Poiroux说，“并可能产生全新的成果。”

本文最初发表于《科学光谱》，经授权转载。FINISHED