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

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

& IEEE Spectrum

& Math.inc 2026-3-2

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

圖源：Quanta Magazine

2022年7月，烏克蘭數(shù)學(xué)家 Maryna Viazovska（瑪麗娜·維亞佐夫斯卡） 榮獲菲爾茲獎（該獎項被廣泛譽為 “數(shù)學(xué)界的諾貝爾獎”），這一消息曾轟動一時。她不僅是該獎項 86 年歷史中第二位獲獎的女性，更是在祖國烏克蘭遭俄羅斯入侵僅數(shù)月后摘得這一殊榮。參閱：。時隔近四年，Viazovska 再次引發(fā)關(guān)注。如今，在人類與人工智能的協(xié)作下，她的證明完成了形式化驗證，這標(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 如此評價，他并未參與此次研究工作。

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

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

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

一次偶遇促成形式化驗證項目落地

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

“對證明進行形式化驗證，就如同蓋上一枚橡膠圖章，是對推理邏輯正確性的正式認證?！盕owl 說。

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

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

“我們?yōu)樵擁椖看罱ùa庫耗時約15個月，直至2025年6月才開放公共訪問權(quán)限。” 如今已是卡內(nèi)基梅隆大學(xué)一年級博士生的 Hariharan 回憶道，“同年10月末，我們首次收到了Math, Inc. 公司的聯(lián)系。”

人工智能助力研究提速

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

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

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

從8維到24維的突破

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

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

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

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

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

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

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

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

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

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

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

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

問題背景

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

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

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

形式化驗證過程

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

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

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

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

項目規(guī)模

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

25000行代碼 —— 素數(shù)定理強形式形式化驗證（2025年9月）

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

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

未來展望

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

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

致謝

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

參考資料

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/