AI與人類協作在數學領域迎來里程碑時刻 ——21世紀菲爾茲獎獲獎證明首次完成形式化驗證——IEEE Spectrum

獲菲爾茲獎的高維最優球堆積問題相關數學研究成果，如今由人類與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. 公司的聯系?！?/p>

人工智能助力研究提速

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

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

“他們告知我們，已經解決了 30 個待證問題（sorrys），也就是證明了我們想要驗證的 30 個中間結論?！盚ariharan 解釋道。研究團隊共享了其中一部分待證問題的驗證結果，并將其與自身的研究成果整合。“其中一個驗證結果還幫助我們發現了項目中的一處筆誤，我們隨后對其進行了修正?！盚ariharan 補充道，“這次合作的成效十分顯著?！?/p>

從8維到24維的突破

就在此次合作后，Math, Inc. 突然杳無音信，仿佛對該項目失去了興趣。但當 Hariharan 及其團隊仍在潛心研究時，這家公司正著手打造升級版的 Gauss 系統。“1 月中旬，我們取得了一項研究突破，研發出性能大幅提升的 Gauss 新版本。”Han 表示，“這個新版本僅用 2 至 3 天，就重現了此前耗時三周完成的素數定理強形式形式化驗證成果?！?/p>

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

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

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

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

8維和24維球堆積證明在基礎理論和整體論證架構上存在共性，這意味著 8 維證明中的部分代碼可經過重構后復用。但此次驗證 24 維問題時，Gauss 并無現成的藍圖可循。“而且這項工作的復雜程度遠高于 8 維的情況，因為關于利奇格的諸多性質，尤其是其唯一性，有大量背景資料亟待補充完善?！盚an 解釋道。

盡管 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/