★置頂zzllrr小樂公眾號，追蹤《小樂數學科普》系列報道！

演講者：瑪麗娜·維亞佐夫斯卡（Maryna Viazovska，菲爾茲獎得主，洛桑聯邦理工學院EPFL）

標題：球體堆積問題的形式化

摘要：本次演講介紹8維和24維球體堆積（填充）問題形式化的路徑。報告將重點介紹迄今取得的主要里程碑、AI人工智能的作用以及大型形式化項目中出現的挑戰。

PPT：（中文翻譯僅供參考，請以原文英文為準）

作者：斯坦福大學數學未來研討會FMS（Future of Mathematics Symposium）

瑪麗娜·維亞佐夫斯卡（Maryna Viazovska，EPFL）2026-5-2

譯者：zzllrr小樂（數學科普公眾號）2026-5-26

求喜歡

主持人：

瑪麗娜·維亞佐夫斯卡接下來將要講解球體堆積問題的形式化工作。瑪麗娜是瑞士洛桑聯邦理工學院的教授兼數論方向學科帶頭人，她憑借八維空間球體堆積相關研究，以及和合作者共同完成的二十四維空間球體堆積研究，斬獲2022年菲爾茲獎（詳情參閱）。話不多說，有請瑪麗娜。

瑪麗娜·維亞佐夫斯卡（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）撰寫的評論文章，探討人工智能時代數學家的發展方向，詳情參閱：，文中提出多項現存問題，同時給出可行的解決思路，具備參考價值。

想要了解項目更多細節，歡迎查閱代碼倉庫 https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean ，也熱忱歡迎各界研究者參與協作。我的分享到此結束。

（掌聲）

Q&A問答環節

主持人：接下來現場開放提問環節。提問觀眾請等候工作人員遞送麥克風，正對話筒發言即可。

問：這套八維空間的形式化證明，能否簡便拓展應用到二十四維空間？

答：理論上可以拓展，高斯模型已經完成相關推導，我們暫時還未核對相關內容。

問：如果想要編寫規范、可復用的拓展代碼，難度如何？

答：我們先打磨完善八維空間對應的代碼體系，兩類問題的論文論證架構高度相似，八維的成熟代碼能夠為二十四維的開發提供參考支撐。

問：感謝精彩分享。彎曲空間中是否存在對應的球體堆積衍生問題？目前研究進展如何？人工智能能否助力這類拓展問題的求解？

答：球體堆積可以衍生出大量幾何優化子類問題，拓展定義并不復雜，難點在于推導求解。除歐幾里得空間外，球面、雙曲空間內均可設置同類問題。目前僅有少數場景可以運用線性規劃方法求出精準最優解。彎曲空間相關研究已經得出部分結論，但大多僅能確定密度上下界，完整求解的案例數量稀少。

八維與二十四維空間的相切球體問題早已徹底破解，該問題也屬于球體堆積的衍生類型，相關成果在上世紀七十年代末就已經問世。其余特殊空間的求解結論零散，尚未形成體系。

問：是否嘗試運用本次用到的研究方法，求解其他維度尚未破解的球體堆積問題？

答：暫時沒有開展相關嘗試。本次研究具備成熟的理論證明作為依托，和未知維度問題的探索難度不在同一層級，后續能否突破仍有待探究。

問：請教代碼編寫過程中，如何平衡人工可讀性代碼與機器生成代碼，編寫時的優先級如何設定？

答：項目初期先敲定整體證明架構，彼時無法預判后續發展走向。人工智能技術迭代速度遠超預期，兩三年前我們都難以實現如今的自動證明效果。整合代碼階段，我們會優先保留人工編寫的代碼，尊重研發人員的工作成果。

問：高斯生成的代碼和預期標準代碼存在哪些差異？機器證明過程中，是否跳過了泊松求和公式的推導？

答：并未跳過該公式的證明步驟。目前我們正在逐條核驗機器代碼，即便代碼邏輯無誤，也依舊會復盤梳理。現階段機器推導的內容，暫時不符合公共函數庫的收錄規范。

舉例說明相關問題，泊松求和公式的證明分散在五個文件夾內，關聯80多條定義聲明，部分內容冗余。

機器代碼中定義了半開半閉區間構成的單位立方體，先證明立方體屬于可測集合，后續又額外判定其為零可測集合。零可測是弱于可測的性質，該部分推導屬于多余步驟，可以直接刪減，相關關聯邏輯統一依托可測性質推導即可。

還有一處案例，人類研究者先期編寫了雅可比函數的性質推導文件，高斯模型補充完善了部分空缺內容，但額外添加了二加二等于四這類基礎引理，這類內容都需要剔除。

代碼中還存在大量無實際調用價值的冗余分支，這類內容可以借助人工智能工具批量清理。

整體代碼篇幅還有精簡壓縮的空間，多處推導邏輯也需要重新規范編寫。

主持人：再次感謝瑪麗娜的精彩分享。

參考資料

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

https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean

https://arxiv.org/abs/1603.06518

小樂數學科普本月文章

小樂數學科普歷年合集

版權聲明：本文首發于微信公眾號“zzllrr小樂”的專欄《小樂數學科普》。歡迎個人轉發。如需轉載，請在“zzllrr小樂”公眾號后臺回復“轉載”，還可通過公眾號菜單、發送郵件到zzllrr@gmail.com與我們取得聯系。相關圖文音視頻內容默認遵守CC BY-NC 4.0知識共享協議，未獲作者和譯者授權，禁止用于營銷宣傳和商業目的。

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊底部一起捐

助力騰訊公益

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！