獲菲爾茲獎(jiǎng)的高維最優(yōu)球堆積問題相關(guān)數(shù)學(xué)研究成果，如今由人類與AI人工智能協(xié)作完成了形式化驗(yàn)證。

作者：Benjamin Skuse（本杰明·斯庫斯）

& IEEE Spectrum

& Math.inc 2026-3-2

譯者：zzllrr小樂（數(shù)學(xué)科普公眾號(hào)）2026-3-14

圖源：Quanta Magazine

2022年7月，烏克蘭數(shù)學(xué)家 Maryna Viazovska（瑪麗娜·維亞佐夫斯卡） 榮獲菲爾茲獎(jiǎng)（該獎(jiǎng)項(xiàng)被廣泛譽(yù)為 “數(shù)學(xué)界的諾貝爾獎(jiǎng)”），這一消息曾轟動(dòng)一時(shí)。她不僅是該獎(jiǎng)項(xiàng) 86 年歷史中第二位獲獎(jiǎng)的女性，更是在祖國烏克蘭遭俄羅斯入侵僅數(shù)月后摘得這一殊榮。參閱：。時(shí)隔近四年，Viazovska 再次引發(fā)關(guān)注。如今，在人類與人工智能的協(xié)作下，她的證明完成了形式化驗(yàn)證，這標(biāo)志著人工智能輔助數(shù)學(xué)研究的能力取得了飛速發(fā)展。https://cacm.acm.org/research/formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification/

“這些新成果令人嘆為觀止，無疑標(biāo)志著該領(lǐng)域的發(fā)展邁出了跨越式的步伐?！?普林斯頓大學(xué)博士后、人工智能推理領(lǐng)域?qū)＜?Liam Fowl 如此評(píng)價(jià)，他并未參與此次研究工作。

在這項(xiàng)斬獲菲爾茲獎(jiǎng)的研究中，Viazovska 攻克了球堆積問題的兩個(gè)難題。球堆積問題的核心是：在 n 維空間中，相同的圓形、球體等幾何體的堆積密度能達(dá)到多少？在二維空間中，蜂窩狀結(jié)構(gòu)是最優(yōu)解；在三維空間中，金字塔式的球體堆疊方式為最佳。但隨著維度增加，尋找最優(yōu)解并證明其最優(yōu)性的難度會(huì)急劇攀升。

2016年，Viazovska解決了兩個(gè)維度下的球堆積難題。她運(yùn)用名為（擬）模形式的強(qiáng)大數(shù)學(xué)函數(shù)，證明了被稱為 E?的對(duì)稱排列是 8 維空間中的最優(yōu)球堆積方式，隨后又與合作者一同證明，另一種名為利奇格（Leech lattice）的球堆積結(jié)構(gòu)是 24 維空間的最優(yōu)解。盡管這一成果看似抽象，卻有望為解決現(xiàn)實(shí)生活中與密堆積相關(guān)的問題提供幫助，其中就包括智能手機(jī)和空間探測(cè)器所使用的糾錯(cuò)碼技術(shù)。

該證明已通過數(shù)學(xué)界的驗(yàn)證并被認(rèn)定為正確，這也為 Viazovska 贏得了菲爾茲獎(jiǎng)的認(rèn)可。但形式化驗(yàn)證 —— 即讓計(jì)算機(jī)對(duì)證明進(jìn)行驗(yàn)證的過程，則是另一項(xiàng)極具挑戰(zhàn)性的工作。2022 年以來，人工智能輔助的形式化證明驗(yàn)證技術(shù)取得了諸多進(jìn)展。

一次偶遇促成形式化驗(yàn)證項(xiàng)目落地

數(shù)年后，在瑞士洛桑，大三本科生 Sidharth Hariharan 與 Viazovska 的一次偶遇，重新點(diǎn)燃了她對(duì)球堆積問題證明進(jìn)行形式化驗(yàn)證的興趣。盡管職業(yè)生涯尚處于起步階段，Hariharan 已在證明形式化領(lǐng)域展現(xiàn)出出色的能力。

“對(duì)證明進(jìn)行形式化驗(yàn)證，就如同蓋上一枚橡膠圖章，是對(duì)推理邏輯正確性的正式認(rèn)證?！盕owl 說。

Hariharan 向 Viazovska 分享了自己如何通過證明形式化的過程學(xué)習(xí)并深入理解數(shù)學(xué)概念。對(duì)此，Viazovska 出于好奇，表達(dá)了對(duì)自己的證明進(jìn)行形式化驗(yàn)證的意愿。由此，2024年3月，“基于 Lean 的球堆積問題形式化驗(yàn)證項(xiàng)目” 正式啟動(dòng) https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/ 。Lean 是一款廣受認(rèn)可的編程語言兼 “證明助手”，數(shù)學(xué)家可借助它撰寫證明，再由計(jì)算機(jī)對(duì)證明的絕對(duì)正確性進(jìn)行驗(yàn)證。

研究團(tuán)隊(duì)展開協(xié)作，撰寫了一份便于人類閱讀的 “藍(lán)圖”。這份藍(lán)圖用于梳理 8 維球堆積證明的各個(gè)組成部分，明確其中哪些部分已完成形式化驗(yàn)證或證明、哪些尚未完成，進(jìn)而在 Lean 中對(duì)缺失的內(nèi)容進(jìn)行證明和形式化驗(yàn)證。

“我們?yōu)樵擁?xiàng)目搭建代碼庫耗時(shí)約15個(gè)月，直至2025年6月才開放公共訪問權(quán)限?！?如今已是卡內(nèi)基梅隆大學(xué)一年級(jí)博士生的 Hariharan 回憶道，“同年10月末，我們首次收到了Math, Inc. 公司的聯(lián)系?！?/p>

人工智能助力研究提速

Math, Inc. 是一家初創(chuàng)企業(yè)，正研發(fā)一款名為 Gauss（高斯）的人工智能系統(tǒng)，其專門用于自動(dòng)完成證明的形式化驗(yàn)證?！癎auss 是一種特殊的推理智能體語言模型，能將傳統(tǒng)的自然語言推理與完全形式化的推理相結(jié)合。” 該公司首席執(zhí)行官兼聯(lián)合創(chuàng)始人 Jesse Han 解釋道，“因此，它能完成文獻(xiàn)檢索、調(diào)用工具、用計(jì)算機(jī)編寫 Lean 代碼、做筆記、啟動(dòng)驗(yàn)證工具、運(yùn)行 Lean 編譯器等一系列操作?！?/p>

此前，Math, Inc. 就曾登上頭條 —— 該公司宣布，Gauss 僅用三周時(shí)間就完成了素?cái)?shù)定理強(qiáng)形式（PNT）的 Lean 形式化驗(yàn)證，而這一工作此前菲爾茲獎(jiǎng)得主 Terence Tao（陶哲軒） 與 Alex Kontorovich（亞歷克斯·康托羅維奇）也一直在推進(jìn)。此次，該公司同樣聯(lián)系了 Hariharan 及其團(tuán)隊(duì)，表示 Gauss 已證明了與他們的球堆積項(xiàng)目相關(guān)的數(shù)個(gè)結(jié)論。

“他們告知我們，已經(jīng)解決了 30 個(gè)待證問題（sorrys），也就是證明了我們想要驗(yàn)證的 30 個(gè)中間結(jié)論。”Hariharan 解釋道。研究團(tuán)隊(duì)共享了其中一部分待證問題的驗(yàn)證結(jié)果，并將其與自身的研究成果整合。“其中一個(gè)驗(yàn)證結(jié)果還幫助我們發(fā)現(xiàn)了項(xiàng)目中的一處筆誤，我們隨后對(duì)其進(jìn)行了修正?！盚ariharan 補(bǔ)充道，“這次合作的成效十分顯著?！?/p>

從8維到24維的突破

就在此次合作后，Math, Inc. 突然杳無音信，仿佛對(duì)該項(xiàng)目失去了興趣。但當(dāng) Hariharan 及其團(tuán)隊(duì)仍在潛心研究時(shí)，這家公司正著手打造升級(jí)版的 Gauss 系統(tǒng)。“1 月中旬，我們?nèi)〉昧艘豁?xiàng)研究突破，研發(fā)出性能大幅提升的 Gauss 新版本?！盚an 表示，“這個(gè)新版本僅用 2 至 3 天，就重現(xiàn)了此前耗時(shí)三周完成的素?cái)?shù)定理強(qiáng)形式形式化驗(yàn)證成果?！?/p>

數(shù)日后，升級(jí)后的 Gauss 系統(tǒng)重新投入到球堆積問題的形式化驗(yàn)證工作中。依托 Hariharan 及其團(tuán)隊(duì)分享的珍貴前期藍(lán)圖和研究成果，Gauss 僅用 5 天時(shí)間，不僅自動(dòng)完成了 8 維球堆積證明的形式化驗(yàn)證，還發(fā)現(xiàn)并修正了已發(fā)表論文中的一處筆誤。

“1月末，當(dāng)他們聯(lián)系我們并告知研究完成時(shí)，毫不夸張地說，我們感到無比震驚。”Hariharan說，“但歸根結(jié)底，這項(xiàng)技術(shù)讓我們滿懷期待，因?yàn)樗鼡碛袆?chuàng)造非凡成就、為數(shù)學(xué)家提供卓越助力的潛力。”

夕陽落在卡內(nèi)基梅隆大學(xué)哈默施拉格大廳的身后，Sidharth Hariharan 正投身于球堆積證明的驗(yàn)證工作。（配圖：Sidharth Hariharan）

2月23日，8維球堆積證明的形式化驗(yàn)證成果正式公布，這一成果本身就標(biāo)志著自動(dòng)形式化驗(yàn)證技術(shù)與人工智能 - 人類協(xié)作模式迎來了里程碑時(shí)刻。而如今，Math, Inc. 又公布了一項(xiàng)更令人矚目的成就：Gauss 僅用兩周時(shí)間，就完成了 Viazovska 提出的 24 維球堆積證明的自動(dòng)形式化驗(yàn)證，相關(guān)代碼量超 20 萬行。

8維和24維球堆積證明在基礎(chǔ)理論和整體論證架構(gòu)上存在共性，這意味著 8 維證明中的部分代碼可經(jīng)過重構(gòu)后復(fù)用。但此次驗(yàn)證 24 維問題時(shí)，Gauss 并無現(xiàn)成的藍(lán)圖可循?！岸疫@項(xiàng)工作的復(fù)雜程度遠(yuǎn)高于 8 維的情況，因?yàn)殛P(guān)于利奇格的諸多性質(zhì)，尤其是其唯一性，有大量背景資料亟待補(bǔ)充完善?！盚an 解釋道。

盡管 24 維球堆積證明的形式化驗(yàn)證是由人工智能自主完成的，但 Han 和 Hariharan 均認(rèn)可人類為這一成就奠定的諸多基礎(chǔ)，認(rèn)為這歸根結(jié)底是人類與人工智能協(xié)作的成果。

而在 Han 看來，這一成果的意義遠(yuǎn)不止于此：它標(biāo)志著數(shù)學(xué)領(lǐng)域革命性變革的開端，超大規(guī)模的形式化驗(yàn)證將成為常態(tài)。“過去，程序員需要在穿孔卡片上編寫程序，而如今，編程行為早已與記錄程序的物理載體相分離。” 他總結(jié)道，“我認(rèn)為，這類技術(shù)的最終價(jià)值，是讓數(shù)學(xué)家擺脫繁瑣的機(jī)械性工作，全身心投入到他們最擅長(zhǎng)的事情中 —— 構(gòu)建全新的數(shù)學(xué)世界?！?/p>

Math.inc相關(guān)報(bào)道

完成高維球堆積問題的形式化證明

借助 Gauss 人工智能系統(tǒng)，我們助力完成了 8 維和 24 維球堆積問題的形式化驗(yàn)證，證實(shí) E?格與利奇格能在對(duì)應(yīng)維度中實(shí)現(xiàn)無重疊球體的最密堆積。

上述成果最初由 Maryna Viazovska 與其合作者證明，也讓 Viazovska 斬獲了 2022 年國際數(shù)學(xué)家大會(huì)的菲爾茲獎(jiǎng)。這是本世紀(jì)首個(gè)完成形式化驗(yàn)證的菲爾茲獎(jiǎng)獲獎(jiǎng)成果。

問題背景

在 n 維空間中，相同球體的堆積密度能達(dá)到多少？一維空間中，該問題的解答顯而易見；二維空間的初等證明也已問世數(shù)十年。三維空間的相關(guān)猜想由 Kepler 于 1611 年提出，直到 1998 年才由 Thomas Hales 完成證明 —— 這一證明高度依賴計(jì)算機(jī)輔助，后續(xù)又耗時(shí)十余年才完成形式化驗(yàn)證。

此后，該問題在其他維度一直懸而未決，直至 Viazovska 發(fā)現(xiàn)了其與模形式理論的驚人關(guān)聯(lián)，率先攻克了 8 維空間的難題。短短數(shù)日內(nèi)，Cohn、Kumar、Miller、Radchenko 與 Viazovska 攜手，沿用相似方法解決了 24 維空間的球堆積問題。時(shí)至今日，該問題在其余維度仍未找到答案。

Peter Sarnak 曾這樣評(píng)價(jià) Viazovska 的精妙論證："大道至簡(jiǎn)，偉大的成果皆如此"。這一研究也為她贏得了被譽(yù)為 "數(shù)學(xué)界諾貝爾獎(jiǎng)" 的菲爾茲獎(jiǎng)。此后，Viazovska 進(jìn)一步完善了自己提出的理論，證明了包括泛最優(yōu)性在內(nèi)的更多結(jié)論。8 維和 24 維球堆積問題的解法，融合了離散幾何、調(diào)和分析與數(shù)論的深度交叉應(yīng)用，是 21 世紀(jì)最具突破性的數(shù)學(xué)成果之一。

形式化驗(yàn)證過程

2024 年，Sidharth Hariharan 與 Maryna Viazovska 聯(lián)合發(fā)起 8 維球堆積問題的形式化驗(yàn)證項(xiàng)目。他們與 Chris Birkbeck、Seewoo Lee、Gareth Ma、Bhavik Mehta 攜手，撰寫了詳盡的研究藍(lán)圖，并開發(fā)了龐大的代碼庫 —— 其中包含了球堆積、格、（擬）模形式相關(guān)的全新定義與定理，而這些內(nèi)容均未收錄于 Mathlib 數(shù)學(xué)庫中。

2025年11月，我們首次與球堆積項(xiàng)目維護(hù)團(tuán)隊(duì)展開合作。通過初代 Gauss 系統(tǒng)，我們成功證明了模形式、徑向施瓦茨函數(shù)、基礎(chǔ)球堆積理論的多個(gè)關(guān)鍵結(jié)論，隨后便將目標(biāo)鎖定在更具挑戰(zhàn)性的方向：完成該項(xiàng)目的剩余驗(yàn)證工作。

僅用 5 天時(shí)間，Gauss 就自動(dòng)證明了 8 維球堆積驗(yàn)證所需的全部剩余結(jié)論。據(jù)球堆積項(xiàng)目團(tuán)隊(duì)估算，若使用現(xiàn)有工具完成 8 維空間的驗(yàn)證工作，還需額外投入 6 個(gè)月的時(shí)間。在此之后，Gauss 僅以原始論文為輸入，在必要時(shí)自主開展文獻(xiàn)檢索，耗時(shí)兩周就完成了 24 維球堆積問題的自動(dòng)形式化驗(yàn)證。這也讓球堆積問題形式化驗(yàn)證的代碼總量從 7 萬行增至約 20 萬行。

驗(yàn)證過程中，Gauss 自主證明了模形式、離散幾何、圍道積分、傅里葉分析領(lǐng)域的諸多重要結(jié)論。它為該項(xiàng)目帶來的貢獻(xiàn)，以前所未有的速度推動(dòng)了這一重大數(shù)學(xué)成果的驗(yàn)證進(jìn)程，成為自動(dòng)形式化驗(yàn)證領(lǐng)域的一座歷史里程碑。

項(xiàng)目規(guī)模

3500行代碼 —— 德布魯因相關(guān)成果形式化驗(yàn)證（2025年6月）

25000行代碼 —— 素?cái)?shù)定理強(qiáng)形式形式化驗(yàn)證（2025年9月）

約20萬行代碼 —— 球堆積問題形式化驗(yàn)證（2026年2月）

人類團(tuán)隊(duì)開展的單一目標(biāo)形式化驗(yàn)證項(xiàng)目，往往需要研究者投入整個(gè)職業(yè)生涯，耗時(shí)十余年甚至更久，其代碼量也鮮有超過 50 萬行的情況。Mathlib 數(shù)學(xué)庫自 2017 年起由 600 余位貢獻(xiàn)者共同搭建，目前代碼量約為 200 萬行。而借助 Gauss 系統(tǒng)，三周時(shí)間就能完成的工作，在不久前還需要耗費(fèi)數(shù)年才能實(shí)現(xiàn)。

未來展望

數(shù)學(xué)的形式化驗(yàn)證，能讓所有已知研究成果實(shí)現(xiàn)可檢索、可組合、可機(jī)器解析，進(jìn)而推動(dòng)數(shù)學(xué)研究的提速。對(duì) 8 維、24 維球堆積這類成果開展形式化驗(yàn)證，能嚴(yán)謹(jǐn)證明看似獨(dú)立的數(shù)學(xué)領(lǐng)域之間存在的深層結(jié)構(gòu)關(guān)聯(lián)，讓我們對(duì)數(shù)學(xué)知識(shí)的整體性有更深刻的理解。

無錯(cuò)誤編譯的形式化證明并非研究的終點(diǎn)，更艱巨、更具深遠(yuǎn)意義的挑戰(zhàn)還在后續(xù)：在全球范圍內(nèi)對(duì)形式化數(shù)學(xué)知識(shí)進(jìn)行整理、整合與維護(hù)。未來數(shù)年，隨著人工智能系統(tǒng)生成的證明成果不斷增多，這將成為全世界共同面對(duì)的課題。將這些證明成果整合到持續(xù)拓展、兼容互通的知識(shí)庫中，很快會(huì)成為規(guī)模化開展形式化驗(yàn)證的基本要求。我們將繼續(xù)與球堆積項(xiàng)目維護(hù)團(tuán)隊(duì)及其他形式化數(shù)學(xué)庫合作，確保 Gauss 生成的代碼能長(zhǎng)期為后人所用、便于維護(hù)。作為該方向的第一步，我們已借助 Gauss 對(duì)其生成的形式化驗(yàn)證代碼進(jìn)行自動(dòng)重構(gòu)、優(yōu)化與風(fēng)格改進(jìn)，將代碼量從峰值時(shí)的 50 萬行精簡(jiǎn)至發(fā)布版本的約 20 萬行。

致謝

本研究工作得到美國國防高級(jí)研究計(jì)劃局（DARPA）指數(shù)性數(shù)學(xué)（expMath）項(xiàng)目的資助，在此致以誠摯的感謝。同時(shí)，感謝 Lean 社區(qū)的所有合作者，包括以 Chris Birkbeck、Sidharth Hariharan、Seewoo Lee、Bhavik Mehta、Maryna Viazovska 為核心的研究團(tuán)隊(duì)；也感謝 Jeremy Avigad、Kevin Buzzard、David Loeffler、Gareth Ma、Pietro Monticone、Mathlib 數(shù)學(xué)庫維護(hù)團(tuán)隊(duì)以及數(shù)學(xué)計(jì)算機(jī)輔助推理研究所提供的寶貴支持。

參考資料

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/