机器之心编辑部

AI 在数学领域的研究取得新进展！

近日，一家名为 Math, Inc. 的公司宣称利用 Gauss 智能体，已经完成了一个关乎 8 维和 24 维空间中的最优球体堆积定理的形式化证明，代码量约为 20 万行（LOC）。

这一定理最初由数学家玛丽娜・维亚佐夫斯卡（Maryna Viazovska）及其合作者证明，Maryna Viazovska 也凭此荣获 2022 年国际数学家大会菲尔兹奖。

据悉，这是本世纪唯一一个被完全形式化证明的菲尔兹奖成果，也是历史上规模最大的单一用途 Lean 形式化项目。

而背后的这家名为 Math, Inc. 的公司，也不是第一次完成数学问题的形式化证明了。

资料显示，Math, Inc. 是由 xAI 前联合创始人、Morph Labs 首席科学家 Christian Szegedy 创立，致力于通过自动形式化技术打造可验证超级智能，Gauss 则是首款专为协助数学专家开展形式化验证工作打造的自动形式化智能体。

去年，Gauss 只用了三周时间，就完成了陶哲轩和 Alex Kontorovich 提出的数学挑战，即在 Lean 定理证明器中完成强素数定理（Prime Number Theorem, PNT）的形式化工作。而该挑战是在 2024 年 1 月提出，陶哲轩与 Alex Kontorovich 团队努力了 18 月，才在去年 7 月宣布取得阶段性进展，可 Gauss 仅用了三周时间。

而这一次，在高维球体堆积问题的形式化证明过程中，Gauss 的速度仍然惊人……

接下来，我们就来详细了解一下。

数学领域 AI 与人类协作的分水岭时刻

2022 年 7 月，乌克兰数学家 Maryna Viazovska 荣获被广泛誉为「数学界诺贝尔奖」的菲尔兹奖，这在当时引起了巨大轰动，她是该奖项 86 年历史上第二位获此殊荣的女性。

近四年后的今天，Viazovska 再次引发了学术界的关注。如今，在人类与人工智能的协作下，她的数学证明已被形式化验证，这标志着 AI 在辅助数学研究方面的能力取得了飞速进展。

「这些新成果令人印象非常深刻，绝对标志着该领域取得了快速进展，」并未参与这项研究的普林斯顿大学博士后、AI 推理专家 Liam Fowl 评价道。

在她获得菲尔兹奖的研究中，Viazovska 攻克了两个版本的球体填充问题。该问题探讨的是：在 n 维空间中，相同的圆、球体等能以多大的密度进行排列？

在二维空间中，蜂窝结构是最佳方案。在三维空间中，将球体堆叠成金字塔状则是最优解。但在此之后，要想找到最佳解并证明它确实是最优的，就变得极其困难。

2016 年，Viazovska 解决了其中两种维度下的问题。通过使用被称为（准）模形式的强大数学函数，她证明了一种名为 E (8) 的对称排列是 8 维空间中的最佳填充方式；不久之后，她又与合作者共同证明了另一种被称为水蛭晶格（Leech lattice）的球体填充方式是 24 维空间中的最优解。尽管这看起来非常抽象，但该成果有望帮助解决日常生活中与高密度球体填充相关的实际问题，包括智能手机和太空探测器所使用的纠错码。

这些证明经过了数学界的验证并被确认为正确，这也为她赢得了菲尔兹奖。但是，形式化验证（即证明能够被计算机绝对验证的能力）完全是另一回事。自 2022 年以来，AI 辅助的形式化证明验证已经取得了长足的进步。

菲尔兹奖获奖数学研究成果 —— 关于多维最优球体堆积，如今已通过人机协作得到正式验证。

机缘巧合促成形式化项目

几年后，在瑞士洛桑，读大三的本科生 Sidharth Hariharan 与 Viazovska 的偶然相遇，重新点燃了她对球体填充证明的兴趣。尽管 Hariharan 处于学术生涯的极早期，但他已经熟练掌握了形式化证明。

「对证明进行形式化验证就像盖上了一枚橡皮图章，」 Fowl 说道，「这是一种真正的权威认证，能证明你的推理陈述是绝对正确的。」

Hariharan 告诉 Viazovska，他一直通过形式化证明的过程来学习和真正理解数学概念。对此，Viazovska 主要出于好奇，表达了对将自己的证明进行形式化的兴趣。由此，在 2024 年 3 月，「在 Lean 中形式化球体填充」（Formalising Sphere Packing in Lean）项目应运而生。Lean 是一种流行的编程语言和「证明助手」，它允许数学家编写证明，然后由计算机验证其绝对的正确性。

这个协作项目汇集了伦敦帝国理工学院的 Bhavik Mehta、英国东安格利亚大学的 Christopher Birkbeck、加州大学伯克利分校的 Seewoo Lee 等专家。该项目的核心工作是编写一份人类可读的「蓝图」，用来梳理 8 维证明的各个组成部分，明确哪些已经或尚未被形式化和 / 或证明，随后在 Lean 环境中证明并形式化那些缺失的元素。

「在 2025 年 6 月开放公众访问之前，我们已经为这个项目的代码库构建了大约 15 个月，」现已是卡内基梅隆大学博士一年级学生的 Sidharth Hariharan 回忆道，「随后，在 10 月下旬，我们首次收到了 Math, Inc. 公司的消息。」

AI 带来的加速

Math, Inc. 是一家初创公司，正在开发一款名为 Gauss 的人工智能，专门用于自动形式化证明。「这是一种被称为推理智能体的特殊语言模型，旨在将传统的自然语言推理与完全形式化的推理交织在一起，」Math, Inc. 首席执行官兼联合创始人 Jesse Han 解释说。

「因此，它能够进行文献检索、调用工具，并使用计算机编写 Lean 代码、做笔记、启动验证工具、运行 Lean 编译器等等。」

Math, Inc. 首次登上头条新闻是在去年夏天，当时该公司宣布 Gauss 用了三周时间完成了强素数定理（PNT）在 Lean 中的形式化，而这项任务原本是菲尔兹奖得主陶哲轩和 Alex Kontorovich 一直在努力攻克的。同样地，Math, Inc. 联系了 Hariharan 及其同事，告知他们 Gauss 已经证明了与他们的球体填充项目相关的几个事实。

Hariharan 解释道：「他们告诉我们，他们完成了 30 个 sorry（注：Lean 语言中表示待证明环节的占位符），这意味着他们证明了 30 个我们需要验证的中间事实。」其中一部分证明被分享给了项目团队，并与他们自己的工作成果进行了合并。「其中一个证明甚至帮我们发现了项目中的一个排版错误，随后我们进行了修正，」 Hariharan 补充说，「所以这是一次非常富有成效的合作。」

从 8 维到 24 维

但是在此之后，对方杳无音讯。Math, Inc. 似乎失去了兴趣。然而，就在 Sidharth Hariharan 和同事们继续这项出于热爱的研究时，Math, Inc. 正在构建一个全新且改进版的 Gauss。

「我们在 1 月中旬取得了研究上的突破，打造出了一个功能更强大的 Gauss 版本，」 Jesse Han 说道，「这个新版本只用两三天的时间，就重现了我们之前花了三周才完成的 PNT 成果。」

几天后，新版 Gauss 被重新引向了球体填充的形式化任务。基于 Hariharan 和合作者分享的宝贵蓝图和已有工作，Gauss 不仅自动形式化了 8 维的情况，还在短短五天内发现并修复了已发表论文中的一个排版错误。

Hariharan 说：「当他们在 1 月下旬联系我们，说他们已经完成了这项工作时，毫不夸张地说，我们感到非常惊讶。但归根结底，这是一项让我们感到极其兴奋的技术，因为它有能力成就伟大的事业，并以惊人的方式辅助数学家。」

Hariharan 正在进行球体填充证明验证，夕阳西下，卡内基梅隆大学哈默施拉格音乐厅后方。

仅仅是 2 月 23 日宣布的 8 维球体填充证明形式化，就已经代表了自动形式化和人机协作的分水岭时刻。但在今天，Math, Inc. 揭晓了一项更加令人瞩目的成就：Gauss 在短短两周内，自动形式化了 Viazovska 24 维球体填充的证明 —— 包含了超过 20 万行的全部代码。

8 维和 24 维的情况在基础理论和证明的整体架构上存在共通之处，这意味着 8 维案例中的部分代码可以被重构和复用。然而，这一次 Gauss 并没有现成的蓝图可供参考。「它实际上比 8 维的情况复杂得多，因为围绕水蛭晶格的许多属性（尤其是它的唯一性），有大量缺失的背景材料需要被整合，」 Jesse Han 解释道。

尽管 24 维的证明过程是一项自动化的工作，但 Jesse Han 和 Hariharan 都承认，正是人类的众多贡献为这一成就奠定了基础。总体而言，他们将此视为人类与 AI 通力协作的结晶。

但对 Jesse Han 来说，这代表着更多意义：它标志着数学领域一场革命性变革的开始，超大规模的形式化将成为家常便饭。

他总结道：「过去，程序员就是那些在纸带卡片上打孔的人，但后来，编程行为与其用来记录程序的物质载体分离开来。我认为，这类技术的最终结果将是解放数学家，让他们去做自己最擅长的事情 —— 也就是去自由构想全新的数学世界。」

展望未来

可以说，在这一定理的证明过程中，Gauss 自主证明了大量关于模形式、离散几何、围道积分和傅里叶分析的重要结论，这一成果也以空前速度推进了这一重大数学结果的验证，是自动形式化领域的历史性成就。

Math, Inc. 认为，数学形式化将通过使已知成果可搜索、可组合、可机器导航，加速科研进程，而对 8 维与 24 维球体堆积这类结果的形式化，也深化了大家对数学知识统一性的理解 —— 它以严格方式揭示了看似无关领域之间的深层结构联系。

但一个可编译、无报错的形式化证明并非终点，更具挑战性的工作在于如何在全球尺度上组织、整合与维护形式化知识。随着越来越多的证明由 AI 系统产生，如何将其整合进持续扩展、相互兼容的知识体系，将成为规模化发展的基本要求。

未来，Math, Inc. 将继续与球体堆积项目及其他形式化数学库的维护者合作，确保 Gauss 生成的代码在未来仍具可用性与可维护性。

https://x.com/mathematics_inc/status/2028542388717986135

https://spectrum.ieee.org/ai-proof-verification

https://www.math.inc/sphere-packing