2026.5数学未来研讨会系列——球体堆积问题的形式化

演讲者：玛丽娜·维亚佐夫斯卡（Maryna Viazovska，菲尔兹奖得主，洛桑联邦理工学院EPFL）

标题：球体堆积问题的形式化

摘要：本次演讲介绍8维和24维球体堆积（填充）问题形式化的路径。报告将重点介绍迄今取得的主要里程碑、AI人工智能的作用以及大型形式化项目中出现的挑战。

PPT：（中文翻译仅供参考，请以原文英文为准）

作者：斯坦福大学数学未来研讨会FMS（Future of Mathematics Symposium）

玛丽娜·维亚佐夫斯卡（Maryna Viazovska，EPFL）2026-5-2

译者：zzllrr小乐（数学科普公众号）2026-5-26

求点赞

求分享

求喜欢

主持人：

玛丽娜·维亚佐夫斯卡接下来将要讲解球体堆积问题的形式化工作。玛丽娜是瑞士洛桑联邦理工学院的教授兼数论方向学科带头人，她凭借八维空间球体堆积相关研究，以及和合作者共同完成的二十四维空间球体堆积研究，斩获2022年菲尔兹奖（详情参阅小乐数学科普：菲尔兹奖历史上第2位女数学家得主——译自量子杂志Quanta Magazine）。话不多说，有请玛丽娜。

玛丽娜·维亚佐夫斯卡（Maryna Viazovska）：

谢谢大家。感谢贾里德的介绍。我十分荣幸能在此发言，本次演讲将围绕八维球体堆积问题的形式化研究项目展开。演讲前半部分讲解背后的数学原理，后半部分介绍形式化推进过程、途中遇到的问题以及我们收获的各类心得。

接下来列出参与本次项目的研究人员与人工智能工具。首先我们从数学本身开始讲起。

什么是球体堆积问题？

设想我们拥有数量无限、大小一致的球体，还有一个体积极大但有限的盒子。我们提出这样一个问题：坚硬的球体彼此可以相切，但不能相互穿插，这个盒子里最多能够容纳多少个这样的球体？当盒子各个维度的尺寸都远大于单个球体尺寸时，不难看出盒子的整体体积是核心影响因素。平均下来，单位体积内能够容纳的球体数量基本趋于稳定，球体堆积问题便由此产生。

这是一道十分自然、历史悠久且求解难度极高的优化问题，在诸多领域甚至应用领域中都会出现。早在十七世纪，开普勒就曾研究过船舱内最多能够摆放多少炮弹。彼时还有学者认为，该问题和凝聚态物质内部的原子排布规律存在关联。如今我们发现，炮弹与原子的共性，并没有十七世纪人们预想的那样多。后来研究者意识到，不必将研究范围局限在三维空间，该问题同样可以拓展到多维空间中求解，并且对应的求解结论能在诸多重要技术领域得到实际应用。

下面给出球体堆积问题更为规范严谨的定义。我们选定一个维数d，探究该维度下单位体积内可容纳球体的最大数量。我们引入球体堆积常数这一概念，统计的并非球体个数，而是球体体积在整体空间体积中所占的比例。每一个维度都对应一个数值，该数值是所有堆积方式所能达到占比的上确界，记作 Δd。

我们对Δd 已有不少研究成果。低维度空间的球体堆积常数已经明确。一维空间中，该数值固定为1，结果显而易见。二维空间的问题具备研究价值，但几何求解难度不算高，很早便得出答案。采用正三角形格排布方式，最多可以铺满平面约九成的区域。

三维空间对应的便是著名的开普勒猜想，该猜想于二十世纪末由托马斯・黑尔斯（Thomas Callister Hales）证明。这个问题本身也和形式化证明渊源颇深。当年这份证明文稿逻辑繁复，审稿人员多年都无法完成审核工作。于是托马斯・黑尔斯决定将证明过程做形式化处理，这项形式化工程又耗费了数年时间。由此可见，数学形式化与球体堆积问题之间有着深厚的历史关联。

超出人类直观感知的维度范围后，相关数据可以参考这张曲线图。

图中蓝色线条代表目前已知最优排布结构对应的堆积密度，绘制为连续实线。严格来说这样的画法并不严谨，我们仅能获取整数维度下的密度数值，维度间隔处的连线只是为了视觉展示效果。

蓝色线条代表密度下界，对应现实中可以实现的排布结构；红色线条则是球体堆积密度的一类上界，这条红线由科恩-埃尔基斯（Cohn-Elkies）上界公式计算得出，后续我会对此展开说明。

从图中能够看出，维度数值趋于无穷时，球体堆积密度会不断下降，且呈指数级衰减，这张图表采用对数坐标绘制。我们已经证实堆积常数会指数衰减，但至今未能确定对应的准确系数。同时图表还能反映出，一维、二维、三维这类低维度区间内，上下界数值基本重合。而绝大多数维度中，现有可实现排布结构对应的密度，和理论推导得出的密度上界之间都存在差值，并且维度越高，两者之间的差距就越大。

八维与二十四维空间呈现出特殊规律，图表里红蓝两条曲线在此处基本贴合。这两个维度的特殊之处体现在，空间内可以构建出性质独特的球体堆积结构。

八维空间中存在精妙的 E₈格（lattice），该数学构造在众多数学分支的各类问题里都会出现。E₈格是唯一秩数为8的幺模格。幺模（unimodular）的定义是经过归一化处理后，单位体积内平均包含一个格点。

偶格代表格内所有向量的模长平方均为偶数。该格中任意两点间的最小距离为√2，原因是模长平方必须取偶数，2是最小的非零偶数。我们选取半径为√2/2的球体，将球心依次设置在E₈格的各个点位上，便能构成格堆积结构，也可以计算出该堆积方式对应的密度。

证明过程

本次讲解的核心定理发表于2016年，定理证明八维欧几里得空间内，不存在堆积密度高于E₈格堆积的单位球体排布方式，E₈格堆积的密度大约为25%。

二十四维空间中也存在类似特殊构造，即里奇格（Leech lattice）。里奇格同样属于幺模偶格（或称偶幺模格）。二十四维空间内一共有24个具备（正定）偶幺模格性质的格，统称为尼迈尔格（Niemeier lattices）。这24个格里，仅有一个格最短向量的模长为2，其余格最短向量模长均为√2。这一特性让它成为求解球体堆积问题的优质构造模型。研究这类格堆积时，我们可以选用半径为1的球体，而非半径√2/2的球体。该格归一化后单位体积内仅有一个球心点位，球体半径取值为1，结构形式简洁规整。

2016年，我与亨利・科恩、史蒂文・米勒等学者共同证明，二十四维空间内最优的球体堆积方式就是里奇格堆积。结合此前的曲线图来看，代表理论上界的红线走势平稳规律，代表实际排布案例的蓝线起伏不定、变化不规则，八维与二十四维两处特殊构造，让密度数值出现了突破性变化。

接下来讲解密度上界的推导方式，上界主要依靠科恩线性规划方法计算得出，下面介绍该方法的原理。

该方法的核心思路是构造辅助函数，常被应用于几何优化类问题。在球体堆积问题的研究范畴中，亨利・科恩与达里尔・埃尔基斯率先运用该方法，德米特里・加尔巴诺夫（Gorbatchev）也同期独立开展相关研究。

该方法要求构造具备良好性质的施瓦茨函数，函数形态光滑且衰减速度极快，同时满足三项约束条件。设定固定维度 d，选取尽可能小的半径 r₀。

1、第一项约束条件：以坐标原点为球心、r₀为半径的球体范围之外，函数取值均小于等于零。

2、第二项约束条件：对该函数做傅里叶变换后，变换所得函数在全空间范围内取值均大于等于零。这两项约束条件相互制衡。

3、第三项约束条件：为平衡约束关系，我们对函数及其傅里叶变换做归一化处理，令二者在原点处的函数值均为1。

满足全部条件后，就能推算出球体堆积常数的理论密度上界。

2003年，亨利・科恩与达里尔・埃尔基斯运用这套方法，测算出一至三十六维空间对应的密度上界。多数维度算出的结果优于以往结论，但依旧无法达到最优临界值，仅有八维与二十四维两个特例。这两个维度下，计算得出的上界数值和实际最优堆积密度高度趋近。理论上界不可能超过现有可实现结构的堆积密度。

2003年的计算结果中，数值小数点后仅有三位零。后续研究者使用运算速度更快的计算机重复测算，八维空间数值小数点后可以出现六十位零，二十四维空间则能出现二十位零。

但这类数值模拟结果只能作为猜想佐证，无法等同于严谨的数学证明。我的研究贡献便是构造出完全契合最优约束条件的辅助函数，该施瓦茨函数针对最优半径 r₀，满足全部三项限定要求。

首篇相关论文发布一周后，我便联合亨利・科恩、史蒂文・米勒等学者，将这套方法拓展应用到二十四维空间，同样构造出符合最优条件的辅助函数。我们如今着手形式化证明的，正是这套核心定理。下图为证明E₈球体堆积最优性所用到的辅助函数，以及其对应的傅里叶变换图像。

魔法函数

史蒂文・米勒将这类函数称作魔法（magic，神奇）函数，依靠这类函数，便能轻松攻克难度极大的优化问题。原图中的原函数与傅里叶变换函数均为施瓦茨函数，衰减速度极快。单纯绘制原始图像，只能看到原点附近的凸起部分，其余区域无法观测。因此我们为函数乘以增速极快的系数，以此完整呈现函数形态。

从图像中能够观察出三处关键特征。原本八维空间对应的函数包含8个变量，我最终仅用单个变量就完成函数表达。原函数与傅里叶变换函数存在大量二重零点，零点位置恰好对应 E₈格最优堆积结构中，各个球体球心之间的间距数值。

这些特征都能够得到合理的数学解释。首先，开普勒问题具备围绕原点旋转不变的特性，据此可以判定辅助函数同样满足旋转不变性，仅依靠单一参数就能够描述函数全貌。其次，凸优化问题中的互补松弛原理，可以解释零点分布规律。最优函数需要满足对应的方程关系，结合问题本身性质，最终体现为函数在E₈格点间距对应数值处取值为零。泊松求和公式也能够佐证这一现象。

以上两点特征，也为定理证明提供了思路指引。结合两处推论线索，可以确定E₈空间辅助函数的构造形式。二重零点的特性，让我们在函数式中加入正弦平方项，以此生成对应的二重零点。同时傅里叶变换函数也需要满足零点条件，这一要求进一步限定了函数的构造形式。我们优先选取便于计算傅里叶变换的函数表达式，计算完成后，再验证零点相关性质。

按照该思路构造的函数，内部隐藏着模群对称特性。发掘出这项隐藏对称规律后，就能确定魔法函数的具体表达式。

其中涉及部分专业术语，在此不展开细说。核心工作便是推导出契合图像特征的函数积分表达式。最终结合前文三项函数性质，确定完整的函数定义。定理证明的最后一步，验证该函数完全符合科恩定理的各项约束条件。

确定函数g的表达式后，证明流程分为三步：第一步，计算函数的傅里叶变换；第二步，核验科恩 - 凯尔基斯定理中的两项不等式；第三步，算出函数及其傅里叶变换在原点处的取值。全部步骤核验完毕，即可完成E₈球体堆积问题的完整证明。

以上便是相关的数学原理部分，接下来介绍形式化证明的推进历程。

形式化证明的历程

2023年11月，凯文・巴扎德（Kevin Buzzard）到访洛桑联邦理工学院，开展专题系列讲座，该讲座是为纪念已故同事专门每年举办的学术活动。

凯文在讲座中分享了形式化证明的相关内容，讲述这项工作的趣味与研究价值。全新的研究方向打动了我，我决定牵头开展这项形式化项目。

彼时西德・哈拉里也以硕士生身份在洛桑联邦理工学院访学，我们二人开始一同探讨项目细节、推进相关工作。我们搭建了对应的代码仓库，项目初期近两年仅面向少数受邀人员内部开放。

后续陆续集结到一批感兴趣、愿意参与协作的研究者，我们制定出项目蓝图。多数形式化项目都采用这类模式：先撰写贴近正式学术论文的数学文稿，文稿内的每一条定义、每一段证明，都能够在Lean代码中精准对应查找。

下图是2025年6月的项目依赖关系图，图中标注出已完成的定义、证明与定理内容，大片空白区域代表尚未完成推导证明的部分。

2025年6月，我们认为项目条件成熟，正式对外公开，欢迎各界研究者参与共建。截至同年12月，项目取得大量全新进展。

众多研究者以及多款人工智能工具相继加入协作，其中包括“高斯”、“亚里士多德”，还有克劳德、通用对话模型等智能程序。

这是2026年2月的项目整体进度。二月期间项目迎来重大变故，学校在读博士生、同时任职于数学智能公司的奥古斯特・波尔找到我，告知我一份迟来的新年成果。团队开展相关运算实验后，成功得出无漏洞的完整形式化证明。面对这份成果，我们需要做出抉择。

正如陶哲轩在相关演讲中提到，单纯获取一份机器生成的完备证明，并没有完全达成我们最初的研究目标。我们期望得到逻辑清晰、便于理解核验、可信度高的证明内容，同时希望拆解证明中的可用模块，将通用内容上传至数学函数库，提升代码复用性。

目前高斯模型已经生成完整的形式化代码，这份成果已经留存数月。但项目并未就此收尾，我们仍需要将这套完整代码整合并入初始开发分支。

介绍整合工作面临的挑战之前，先梳理高斯模型生成代码前，项目原本的推进进度、代码仓库的文件构成，以及后续代码复用的规划方向。此前展示过项目早期的蓝图架构，整体结构繁杂交错。下面梳理形式化定理需要完成的各项工作。

首先补齐基础理论内容，录入球体堆积、格堆积、周期球体堆积的规范定义，以及各类基础推论，目前这部分基础内容已经编写完成。项目用到科恩线性规划方法，因此需要补充傅里叶分析相关定理。数学函数库中已经收录部分相关内容，但仍存在关键内容缺失，多维形式的泊松求和公式尚未完善，这也是我们后续需要补充编写的模块。

基础理论与傅里叶相关内容补齐后，便可着手证明科恩定理。构造魔法函数还需要用到围道积分相关知识，目前函数库内相关内容储备不足，现有资料也无法直接适配使用需求，该方向目前也在持续完善优化。

构造魔法函数还需要模形式基础理论，函数库中模形式相关体系已经相对完备，仅缺少少量细分结论。我们计划将项目中新推导得出的通用结论，同步上传补充至公共函数库。全部基础内容准备就绪后，便可构造魔法函数，进而完成不等式证明。不等式最初的证明方式偏向数值运算，将证明过程转化为区间算术的大规模计算。

后续又诞生两份全新证明思路，唐・罗姆尼克（Dan Romik）与奇维分别推导出更贴合人类思考逻辑、可读性更强的证明过程。依托各类证明方法，最终即可完成核心定理的全部推导。下图罗列了球体堆积基础理论需要补充完善的内容条目。

我们需要明确球体堆积有限密度与无限密度的定义。有一项经典实用的推论：求解球体堆积密度上确界时，统计全部排布结构，或是仅统计周期性排布结构，最终得出的上确界数值完全一致。该结论推导难度不高，不仅适用于本项目，后续其他相关研究也可以复用。

使用Lean编写代码时会发现，很多主观上显而易见的结论，都需要花费时间规范定义、逐条核验，才能通过程序校验。

本次项目希望完善更高维度通用版本的泊松求和公式，优化证明逻辑，最终将这份内容收录进公共函数库。周期性堆积相关结论，既是独立的基础知识点，也是科恩线性规划方法的必备前置条件。该计算方法以周期性球体堆积为研究基础，一般情况的堆积问题，均可等效转化为周期性堆积问题求解。

下图展示需要核验证明的不等式内容，图像中两处蓝色曲线分别对应两类函数，需要证实其中一个函数取值恒负，另一个函数取值恒正。

图像呈现的结果直观易懂，但程序无法直接采信视觉判断，依旧需要严谨的推导论证。

目前已有两篇文献给出差异化证明思路，高斯模型也依托原始数值计算方法，得出有效的核验凭证。

这便是现阶段代码仓库的整体状态。正如陶哲轩所言，我们虽然拿到了完备的形式化证明，也掌握基础原理，但部分内容依旧无法达到预期标准。近期刊登的相关报道，也反映出同类研究普遍面临这类问题，诸多团队都在攻克相关难题，也让我们更有信心探寻优化方案。

待办与复盘

现阶段剩余工作主要分为几方面：

梳理精简代码结构，删减冗余推导步骤，修正不规范的证明写法，替换掉稳定性差、不利于后期维护的程序指令，筛选出具备通用价值、适用范围超出本项目的推导结论，整理后提交至公共函数库，同时复盘本次形式化项目的全过程，总结经验教训。

这项研究也引发了数学界与形式化证明领域的广泛讨论，社交平台涌现大量相关观点。

在此引用两篇专业论文，探讨大规模形式化研究的合理开展模式。第一篇论文从数理哲学角度，探讨数学证明的对应性问题。

形式化证明一方面可以作为判定结论真伪的凭证，另一方面，研究者也希望读懂证明的每一处逻辑细节。人工推导的非形式化证明与机器形式化证明之间，如何建立清晰的对应关联，是亟待解决的问题。项目蓝图规划模式，可以有效缓解这一难题。

先拟定完整的形式化框架，再对照框架编写代码，能够顺畅衔接理论设计与程序代码。人工智能自动生成的代码，往往很难和初始规划框架形成清晰对应关系。这也是我们坚持优化代码、打通人工逻辑与程序代码关联的重要原因。

第二篇由杰里米・阿维加德（Jeremy Avigad）撰写的评论文章，探讨人工智能时代数学家的发展方向，详情参阅：AI人工智能时代的数学家们——杰里米·阿维加德（Jeremy Avigad），文中提出多项现存问题，同时给出可行的解决思路，具备参考价值。

想要了解项目更多细节，欢迎查阅代码仓库 https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean ，也热忱欢迎各界研究者参与协作。我的分享到此结束。

（掌声）

Q&A问答环节

主持人：接下来现场开放提问环节。提问观众请等候工作人员递送麦克风，正对话筒发言即可。

问：这套八维空间的形式化证明，能否简便拓展应用到二十四维空间？

答：理论上可以拓展，高斯模型已经完成相关推导，我们暂时还未核对相关内容。

问：如果想要编写规范、可复用的拓展代码，难度如何？

答：我们先打磨完善八维空间对应的代码体系，两类问题的论文论证架构高度相似，八维的成熟代码能够为二十四维的开发提供参考支撑。

问：感谢精彩分享。弯曲空间中是否存在对应的球体堆积衍生问题？目前研究进展如何？人工智能能否助力这类拓展问题的求解？

答：球体堆积可以衍生出大量几何优化子类问题，拓展定义并不复杂，难点在于推导求解。除欧几里得空间外，球面、双曲空间内均可设置同类问题。目前仅有少数场景可以运用线性规划方法求出精准最优解。弯曲空间相关研究已经得出部分结论，但大多仅能确定密度上下界，完整求解的案例数量稀少。

八维与二十四维空间的相切球体问题早已彻底破解，该问题也属于球体堆积的衍生类型，相关成果在上世纪七十年代末就已经问世。其余特殊空间的求解结论零散，尚未形成体系。

问：是否尝试运用本次用到的研究方法，求解其他维度尚未破解的球体堆积问题？

答：暂时没有开展相关尝试。本次研究具备成熟的理论证明作为依托，和未知维度问题的探索难度不在同一层级，后续能否突破仍有待探究。

问：请教代码编写过程中，如何平衡人工可读性代码与机器生成代码，编写时的优先级如何设定？

答：项目初期先敲定整体证明架构，彼时无法预判后续发展走向。人工智能技术迭代速度远超预期，两三年前我们都难以实现如今的自动证明效果。整合代码阶段，我们会优先保留人工编写的代码，尊重研发人员的工作成果。

问：高斯生成的代码和预期标准代码存在哪些差异？机器证明过程中，是否跳过了泊松求和公式的推导？

答：并未跳过该公式的证明步骤。目前我们正在逐条核验机器代码，即便代码逻辑无误，也依旧会复盘梳理。现阶段机器推导的内容，暂时不符合公共函数库的收录规范。

举例说明相关问题，泊松求和公式的证明分散在五个文件夹内，关联80多条定义声明，部分内容冗余。

机器代码中定义了半开半闭区间构成的单位立方体，先证明立方体属于可测集合，后续又额外判定其为零可测集合。零可测是弱于可测的性质，该部分推导属于多余步骤，可以直接删减，相关关联逻辑统一依托可测性质推导即可。

还有一处案例，人类研究者先期编写了雅可比函数的性质推导文件，高斯模型补充完善了部分空缺内容，但额外添加了二加二等于四这类基础引理，这类内容都需要剔除。

代码中还存在大量无实际调用价值的冗余分支，这类内容可以借助人工智能工具批量清理。

整体代码篇幅还有精简压缩的空间，多处推导逻辑也需要重新规范编写。

主持人：再次感谢玛丽娜的精彩分享。

参考资料

https://www.youtube.com/watch?v=lcgPj7hge-E