获菲尔兹奖的高维最优球堆积问题相关数学研究成果，如今由人类与AI人工智能协作完成了形式化验证。
作者：Benjamin Skuse（本杰明·斯库斯）
& IEEE Spectrum
& Math.inc 2026-3-2
译者：zzllrr小乐（数学科普公众号）2026-3-14
图源：Quanta Magazine
2022年7月，乌克兰数学家 Maryna Viazovska（玛丽娜·维亚佐夫斯卡） 荣获菲尔兹奖（该奖项被广泛誉为 “数学界的诺贝尔奖”），这一消息曾轰动一时。她不仅是该奖项 86 年历史中第二位获奖的女性，更是在祖国乌克兰遭俄罗斯入侵仅数月后摘得这一殊荣。参阅：。时隔近四年，Viazovska 再次引发关注。如今，在人类与人工智能的协作下，她的证明完成了形式化验证，这标志着人工智能辅助数学研究的能力取得了飞速发展。https://cacm.acm.org/research/formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification/
“这些新成果令人叹为观止，无疑标志着该领域的发展迈出了跨越式的步伐。” 普林斯顿大学博士后、人工智能推理领域专家 Liam Fowl 如此评价，他并未参与此次研究工作。
在这项斩获菲尔兹奖的研究中，Viazovska 攻克了球堆积问题的两个难题。球堆积问题的核心是：在 n 维空间中，相同的圆形、球体等几何体的堆积密度能达到多少？在二维空间中，蜂窝状结构是最优解；在三维空间中，金字塔式的球体堆叠方式为最佳。但随着维度增加，寻找最优解并证明其最优性的难度会急剧攀升。
2016年，Viazovska解决了两个维度下的球堆积难题。她运用名为（拟）模形式的强大数学函数，证明了被称为 E₈的对称排列是 8 维空间中的最优球堆积方式，随后又与合作者一同证明，另一种名为利奇格（Leech lattice）的球堆积结构是 24 维空间的最优解。尽管这一成果看似抽象，却有望为解决现实生活中与密堆积相关的问题提供帮助，其中就包括智能手机和空间探测器所使用的纠错码技术。
该证明已通过数学界的验证并被认定为正确，这也为 Viazovska 赢得了菲尔兹奖的认可。但形式化验证 —— 即让计算机对证明进行验证的过程，则是另一项极具挑战性的工作。2022 年以来，人工智能辅助的形式化证明验证技术取得了诸多进展。
一次偶遇促成形式化验证项目落地
数年后，在瑞士洛桑，大三本科生 Sidharth Hariharan 与 Viazovska 的一次偶遇，重新点燃了她对球堆积问题证明进行形式化验证的兴趣。尽管职业生涯尚处于起步阶段，Hariharan 已在证明形式化领域展现出出色的能力。
“对证明进行形式化验证，就如同盖上一枚橡胶图章，是对推理逻辑正确性的正式认证。”Fowl 说。
Hariharan 向 Viazovska 分享了自己如何通过证明形式化的过程学习并深入理解数学概念。对此，Viazovska 出于好奇，表达了对自己的证明进行形式化验证的意愿。由此，2024年3月，“基于 Lean 的球堆积问题形式化验证项目” 正式启动 https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/ 。Lean 是一款广受认可的编程语言兼 “证明助手”，数学家可借助它撰写证明，再由计算机对证明的绝对正确性进行验证。
研究团队展开协作，撰写了一份便于人类阅读的 “蓝图”。这份蓝图用于梳理 8 维球堆积证明的各个组成部分，明确其中哪些部分已完成形式化验证或证明、哪些尚未完成，进而在 Lean 中对缺失的内容进行证明和形式化验证。
“我们为该项目搭建代码库耗时约15个月，直至2025年6月才开放公共访问权限。” 如今已是卡内基梅隆大学一年级博士生的 Hariharan 回忆道，“同年10月末，我们首次收到了Math, Inc. 公司的联系。”
人工智能助力研究提速
Math, Inc. 是一家初创企业，正研发一款名为 Gauss（高斯）的人工智能系统，其专门用于自动完成证明的形式化验证。“Gauss 是一种特殊的推理智能体语言模型，能将传统的自然语言推理与完全形式化的推理相结合。” 该公司首席执行官兼联合创始人 Jesse Han 解释道，“因此，它能完成文献检索、调用工具、用计算机编写 Lean 代码、做笔记、启动验证工具、运行 Lean 编译器等一系列操作。”
此前，Math, Inc. 就曾登上头条 —— 该公司宣布，Gauss 仅用三周时间就完成了素数定理强形式（PNT）的 Lean 形式化验证，而这一工作此前菲尔兹奖得主 Terence Tao（陶哲轩） 与 Alex Kontorovich（亚历克斯·康托罗维奇）也一直在推进。此次，该公司同样联系了 Hariharan 及其团队，表示 Gauss 已证明了与他们的球堆积项目相关的数个结论。
“他们告知我们，已经解决了 30 个待证问题（sorrys），也就是证明了我们想要验证的 30 个中间结论。”Hariharan 解释道。研究团队共享了其中一部分待证问题的验证结果，并将其与自身的研究成果整合。“其中一个验证结果还帮助我们发现了项目中的一处笔误，我们随后对其进行了修正。”Hariharan 补充道，“这次合作的成效十分显著。”
从8维到24维的突破
就在此次合作后，Math, Inc. 突然杳无音信，仿佛对该项目失去了兴趣。但当 Hariharan 及其团队仍在潜心研究时，这家公司正着手打造升级版的 Gauss 系统。“1 月中旬，我们取得了一项研究突破，研发出性能大幅提升的 Gauss 新版本。”Han 表示，“这个新版本仅用 2 至 3 天，就重现了此前耗时三周完成的素数定理强形式形式化验证成果。”
数日后，升级后的 Gauss 系统重新投入到球堆积问题的形式化验证工作中。依托 Hariharan 及其团队分享的珍贵前期蓝图和研究成果，Gauss 仅用 5 天时间，不仅自动完成了 8 维球堆积证明的形式化验证，还发现并修正了已发表论文中的一处笔误。
“1月末，当他们联系我们并告知研究完成时，毫不夸张地说，我们感到无比震惊。”Hariharan说，“但归根结底，这项技术让我们满怀期待，因为它拥有创造非凡成就、为数学家提供卓越助力的潜力。”
夕阳落在卡内基梅隆大学哈默施拉格大厅的身后，Sidharth Hariharan 正投身于球堆积证明的验证工作。（配图：Sidharth Hariharan）
2月23日，8维球堆积证明的形式化验证成果正式公布，这一成果本身就标志着自动形式化验证技术与人工智能 - 人类协作模式迎来了里程碑时刻。而如今，Math, Inc. 又公布了一项更令人瞩目的成就：Gauss 仅用两周时间，就完成了 Viazovska 提出的 24 维球堆积证明的自动形式化验证，相关代码量超 20 万行。
8维和24维球堆积证明在基础理论和整体论证架构上存在共性，这意味着 8 维证明中的部分代码可经过重构后复用。但此次验证 24 维问题时，Gauss 并无现成的蓝图可循。“而且这项工作的复杂程度远高于 8 维的情况，因为关于利奇格的诸多性质，尤其是其唯一性，有大量背景资料亟待补充完善。”Han 解释道。
尽管 24 维球堆积证明的形式化验证是由人工智能自主完成的，但 Han 和 Hariharan 均认可人类为这一成就奠定的诸多基础，认为这归根结底是人类与人工智能协作的成果。
而在 Han 看来，这一成果的意义远不止于此：它标志着数学领域革命性变革的开端，超大规模的形式化验证将成为常态。“过去，程序员需要在穿孔卡片上编写程序，而如今，编程行为早已与记录程序的物理载体相分离。” 他总结道，“我认为，这类技术的最终价值，是让数学家摆脱繁琐的机械性工作，全身心投入到他们最擅长的事情中 —— 构建全新的数学世界。”
Math.inc相关报道
完成高维球堆积问题的形式化证明
借助 Gauss 人工智能系统，我们助力完成了 8 维和 24 维球堆积问题的形式化验证，证实 E₈格与利奇格能在对应维度中实现无重叠球体的最密堆积。
上述成果最初由 Maryna Viazovska 与其合作者证明，也让 Viazovska 斩获了 2022 年国际数学家大会的菲尔兹奖。这是本世纪首个完成形式化验证的菲尔兹奖获奖成果。
问题背景
在 n 维空间中，相同球体的堆积密度能达到多少？一维空间中，该问题的解答显而易见；二维空间的初等证明也已问世数十年。三维空间的相关猜想由 Kepler 于 1611 年提出，直到 1998 年才由 Thomas Hales 完成证明 —— 这一证明高度依赖计算机辅助，后续又耗时十余年才完成形式化验证。
此后，该问题在其他维度一直悬而未决，直至 Viazovska 发现了其与模形式理论的惊人关联，率先攻克了 8 维空间的难题。短短数日内，Cohn、Kumar、Miller、Radchenko 与 Viazovska 携手，沿用相似方法解决了 24 维空间的球堆积问题。时至今日，该问题在其余维度仍未找到答案。
Peter Sarnak 曾这样评价 Viazovska 的精妙论证："大道至简，伟大的成果皆如此"。这一研究也为她赢得了被誉为 "数学界诺贝尔奖" 的菲尔兹奖。此后，Viazovska 进一步完善了自己提出的理论，证明了包括泛最优性在内的更多结论。8 维和 24 维球堆积问题的解法，融合了离散几何、调和分析与数论的深度交叉应用，是 21 世纪最具突破性的数学成果之一。
形式化验证过程
2024 年，Sidharth Hariharan 与 Maryna Viazovska 联合发起 8 维球堆积问题的形式化验证项目。他们与 Chris Birkbeck、Seewoo Lee、Gareth Ma、Bhavik Mehta 携手，撰写了详尽的研究蓝图，并开发了庞大的代码库 —— 其中包含了球堆积、格、（拟）模形式相关的全新定义与定理，而这些内容均未收录于 Mathlib 数学库中。
2025年11月，我们首次与球堆积项目维护团队展开合作。通过初代 Gauss 系统，我们成功证明了模形式、径向施瓦茨函数、基础球堆积理论的多个关键结论，随后便将目标锁定在更具挑战性的方向：完成该项目的剩余验证工作。
仅用 5 天时间，Gauss 就自动证明了 8 维球堆积验证所需的全部剩余结论。据球堆积项目团队估算，若使用现有工具完成 8 维空间的验证工作，还需额外投入 6 个月的时间。在此之后，Gauss 仅以原始论文为输入，在必要时自主开展文献检索，耗时两周就完成了 24 维球堆积问题的自动形式化验证。这也让球堆积问题形式化验证的代码总量从 7 万行增至约 20 万行。
验证过程中，Gauss 自主证明了模形式、离散几何、围道积分、傅里叶分析领域的诸多重要结论。它为该项目带来的贡献，以前所未有的速度推动了这一重大数学成果的验证进程，成为自动形式化验证领域的一座历史里程碑。
项目规模
3500行代码 —— 德布鲁因相关成果形式化验证（2025年6月）
25000行代码 —— 素数定理强形式形式化验证（2025年9月）
约20万行代码 —— 球堆积问题形式化验证（2026年2月）
人类团队开展的单一目标形式化验证项目，往往需要研究者投入整个职业生涯，耗时十余年甚至更久，其代码量也鲜有超过 50 万行的情况。Mathlib 数学库自 2017 年起由 600 余位贡献者共同搭建，目前代码量约为 200 万行。而借助 Gauss 系统，三周时间就能完成的工作，在不久前还需要耗费数年才能实现。
未来展望
数学的形式化验证，能让所有已知研究成果实现可检索、可组合、可机器解析，进而推动数学研究的提速。对 8 维、24 维球堆积这类成果开展形式化验证，能严谨证明看似独立的数学领域之间存在的深层结构关联，让我们对数学知识的整体性有更深刻的理解。
无错误编译的形式化证明并非研究的终点，更艰巨、更具深远意义的挑战还在后续：在全球范围内对形式化数学知识进行整理、整合与维护。未来数年，随着人工智能系统生成的证明成果不断增多，这将成为全世界共同面对的课题。将这些证明成果整合到持续拓展、兼容互通的知识库中，很快会成为规模化开展形式化验证的基本要求。我们将继续与球堆积项目维护团队及其他形式化数学库合作，确保 Gauss 生成的代码能长期为后人所用、便于维护。作为该方向的第一步，我们已借助 Gauss 对其生成的形式化验证代码进行自动重构、优化与风格改进，将代码量从峰值时的 50 万行精简至发布版本的约 20 万行。
致谢
本研究工作得到美国国防高级研究计划局（DARPA）指数性数学（expMath）项目的资助，在此致以诚挚的感谢。同时，感谢 Lean 社区的所有合作者，包括以 Chris Birkbeck、Sidharth Hariharan、Seewoo Lee、Bhavik Mehta、Maryna Viazovska 为核心的研究团队；也感谢 Jeremy Avigad、Kevin Buzzard、David Loeffler、Gareth Ma、Pietro Monticone、Mathlib 数学库维护团队以及数学计算机辅助推理研究所提供的宝贵支持。
参考资料
https://spectrum.ieee.org/ai-proof-verification
https://www.math.inc/sphere-packing
https://github.com/math-inc/Sphere-Packing-Lean
https://www.math.inc
https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/
https://cacm.acm.org/research/formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification/
热门跟贴