ISTOCK
来源：IEEE电气电子工程师学会
2022年7月，乌克兰数学家Maryna Viazovska荣获素有“数学界诺贝尔奖”之称的菲尔兹奖，这在当时成为重大新闻，她是该奖项设立86年来第二位获此殊荣的女性。近四年后，Viazovska再度引发关注。如今，通过人类与AI的协作，她的数学证明已被形式化验证，这标志着人工智能在辅助数学研究方面取得了飞速进展（https://www.math.inc/sphere-packing）。
并未参与此项工作的普林斯顿大学博士后、AI推理专家Liam Fowl表示：“这些新成果令人极为震撼，无疑标志着该领域正快速向前推进。”
在这项为她赢得菲尔兹奖的研究中，Viazovska解决了两种版本的球体堆积问题 —— 该问题研究的是：相同的圆、球体等，在n维空间中能以多大密度进行堆积？在二维空间中，蜂窝结构是最优解；在三维空间中，金字塔式堆叠最为理想。但维度更高时，寻找最优解并严格证明其为最优就变得异常困难。
2016年，Viazovska解决了该问题的两种情形。她借助被称为（拟）模形式的强大数学工具，证明了名为E₈的对称结构是8维空间中的最优球体堆积方式；此后不久，她又与合作者共同证明，另一种被称为Leech lattice的球体堆积结构是24维空间中的最优解。尽管这一成果看似抽象，却有望帮助解决与高密度球体堆积相关的实际问题，包括智能手机与深空探测器所使用的纠错编码技术。
The sphere packing problem in dimension 8：
https://annals.math.princeton.edu/articles/keyword/sphere-packing
The sphere packing problem in dimension 24：
https://annals.math.princeton.edu/2017/185-3/p08
纠错编码技术：https://spectrum.ieee.org/novel-error-correction-code-opens-a-new-approach-to-universal-quantum-computing
这些证明已被数学界验证并认定为正确，也因此为她赢得了菲尔兹奖。但形式化验证 ——即让计算机也能核验证明的正确性 —— 则完全是另一回事。自2022年以来，AI辅助的形式化证明验证已取得大量进展（https://cacm.acm.org/research/formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification/）。
一次机缘促成了这项形式化
工作几年后，在瑞士洛桑，大三本科生Sidharth Hariharan与Viazovska的一次偶然相遇，重新点燃了她对球体堆积证明的兴趣。尽管学术生涯尚处起步阶段，哈里哈兰已十分擅长证明的形式化工作。
“对证明的形式化验证就像一枚官方橡皮图章，”Fowl说，“它是一份权威认证，确保你的推理与结论准确无误。”
Hariharan向Viazovska介绍了他是如何通过证明形式化这一过程来学习并真正理解数学概念的。维亚佐夫斯卡对此作出回应，表示主要出于好奇，她也有意将自己的证明进行形式化处理。由此，“在Lean中形式化球体堆积问题（https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/）”项目于2024年3月正式启动。Lean是一款广受欢迎的编程语言，同时也是一款证明辅助工具，数学家可以用它编写证明，再由计算机对证明的绝对正确性进行核验。
团队由此展开合作，先撰写一份人类可读的“蓝图”，用它梳理出8维证明的各个组成部分，区分哪些已经被形式化和/或证明、哪些尚未完成，再在Lean中对缺失部分进行证明与形式化。
Hariharan如今是卡内基梅隆大学的一年级博士生，他回忆道：“我们为这个项目搭建代码库大约15个月后，于2025年6月向公众开放了访问权限。同年10月底，我们第一次收到了Math, Inc.公司的联系。”
AI带来的提速
Math, Inc.是一家初创公司（https://www.math.inc/），专门研发一款名为Gauss的人工智能，它是专为自动形式化证明而设计的系统。“这是一类特殊的语言模型，我们称之为推理智能体，它可以把传统的自然语言推理和完全形式化推理交织在一起。”Math, Inc.联合创始人兼首席执行官Jesse Han解释说，“它能够进行文献检索、调用工具、用计算机编写Lean代码、记录笔记、启动验证工具、运行Lean编译器等等。”
去年夏天，Math, Inc.曾因宣布其开发的Gauss在三周内完成了强素数定理（PNT，https://mathstodon.xyz/@tao/111847680248482955）的Lean形式化验证而登上新闻头条，而这项工作此前由菲尔兹奖得主陶哲轩与Alex Kontorovich牵头开展。与此类似，Math, Inc.联系了Hariharan及其团队，告知他们Gauss已经证明了与球体堆积项目相关的若干结论。
“他们告诉我们，Gauss完成了30个‘sorry’，这意味着它证明了我们原本希望证明的30个中间结论。”Hariharan解释道。其中一部分结论被分享给项目团队，并整合进他们自己的工作中。“其中一个结果还帮我们发现了项目里的一处笔误，我们随后进行了修正。”Hariharan补充说，“所以这是一次非常富有成果的合作。”
从8维到24维
但在那之后，双方便陷入了沉寂，Math, Inc.似乎失去了兴趣。不过，就在Hariharan及其团队继续投入这项热爱的工作时，Math, Inc.正在打造全新升级版的Gauss。“我们在1月中旬取得了一项研究突破，推出了性能大幅增强的新版Gauss。”Han表示，“新版本仅用两三天就复现了此前需要三周才能完成的素数定理形式化工作。”
几天后，新版Gauss重新投入到球体堆积证明的形式化任务中。依托Hariharan团队此前提供的宝贵基础蓝图与已有成果，Gauss仅用五天时间，就不仅自动完成了8维情形的形式化验证，还发现并修正了已发表论文中的一处笔误。
Hariharan说：“1月底他们联系我们，告诉我们已经完成了这项工作时，毫不夸张地说，我们极为震惊。但归根结底，我们对这项技术感到非常兴奋，因为它拥有创造卓越成果的能力，并能以非凡的方式为数学家提供助力。”
Sidharth Hariharan
2月23日宣布的8维球体堆积证明形式化，本身就已是自动形式化与人类–AI协作的分水岭时刻。而如今，Math, Inc.又公布了一项更令人震撼的成果：Gauss已自动完成Viazovska 24维球体堆积证明的形式化 —— 整整超过20万行代码，仅用两周时间。
8维与24维情形在基础理论和证明整体架构上存在共通之处，这意味着8维的部分代码可以重构后复用。然而，这次Gauss没有现成的蓝图可以直接使用。“事实上，24维的难度远高于8维，因为有大量缺失的背景内容需要补充，尤其是围绕Leech lattice的诸多性质，特别是它的唯一性。”Han解释道。
尽管24维的工作是自动完成的，Han与Hariharan都承认，这一成就离不开人类此前打下的大量基础，他们将其视作一场人类与AI共同完成的协作成果。
但在Han看来，这一成果的意义更为深远：它标志着数学领域一场革命性变革的开端 ——未来，超大规模的形式化验证将成为常态。他总结道：“过去，程序员的工作是在卡片上打孔，后来编程行为与记录程序的物理载体分离开来。我相信，这类技术最终会让数学家解放出来，去做他们最擅长的事 —— 构想全新的数学世界。”
阅读最新前沿科技趋势报告，请访问21世纪关键技术研究院的“未来知识库”
未来知识库是 “21世纪关键技术研究院”建 立的在线知识库平台，收藏的资料范围包括人工智能、脑科学、互联网、超级智能，数智大脑、能源、军事、经济、人类风险等等领域的前沿进展与未来趋势。目前拥有超过8000篇重要资料。每周更新不少于100篇世界范围最新研究资料。 欢迎扫描二维码或访问https://wx.zsxq.com/group/454854145828进入。
截止到2月28日 ”未来知识库”精选的百部前沿科技趋势报告
（加入未来知识库，全部资料免费阅读和下载）
热门跟贴