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. 公司的聯系。”

人工智能助力研究提速

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

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

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

從8維到24維的突破

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

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

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

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

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

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

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