人工智能與人協作攻克數學的分水嶺時刻 —— 21世紀菲爾茲獎成果首次完成形式化驗證

ISTOCK

來源：IEEE電氣電子工程師學會

2022年7月，烏克蘭數學家Maryna Viazovska榮獲素有“數學界諾貝爾獎”之稱的菲爾茲獎，這在當時成為重大新聞，她是該獎項設立86年來第二位獲此殊榮的女性。近四年后，Viazovska再度引發關注。如今，通過人類與AI的協作，她的數學證明已被形式化驗證，這標志著人工智能在輔助數學研究方面取得了飛速進展（https://www.math.inc/sphere-packing）。

并未參與此項工作的普林斯頓大學博士后、AI推理專家Liam Fowl表示：“這些新成果令人極為震撼，無疑標志著該領域正快速向前推進。”

在這項為她贏得菲爾茲獎的研究中，Viazovska解決了兩種版本的球體堆積問題 —— 該問題研究的是：相同的圓、球體等，在n維空間中能以多大密度進行堆積？在二維空間中，蜂窩結構是最優解；在三維空間中，金字塔式堆疊最為理想。但維度更高時，尋找最優解并嚴格證明其為最優就變得異常困難。

2016年，Viazovska解決了該問題的兩種情形。她借助被稱為（擬）模形式的強大數學工具，證明了名為E?的對稱結構是8維空間中的最優球體堆積方式；此后不久，她又與合作者共同證明，另一種被稱為Leech lattice的球體堆積結構是24維空間中的最優解。盡管這一成果看似抽象，卻有望幫助解決與高密度球體堆積相關的實際問題，包括智能手機與深空探測器所使用的糾錯編碼技術。

The sphere packing problem in dimension 8：

https://annals.math.princeton.edu/articles/keyword/sphere-packing

The sphere packing problem in dimension?24：

https://annals.math.princeton.edu/2017/185-3/p08

糾錯編碼技術：https://spectrum.ieee.org/novel-error-correction-code-opens-a-new-approach-to-universal-quantum-computing

這些證明已被數學界驗證并認定為正確，也因此為她贏得了菲爾茲獎。但形式化驗證 ——即讓計算機也能核驗證明的正確性 —— 則完全是另一回事。自2022年以來，AI輔助的形式化證明驗證已取得大量進展（https://cacm.acm.org/research/formal-reasoning-meets-llms-toward-ai-for-mathematics-and-verification/）。

一次機緣促成了這項形式化

工作幾年后，在瑞士洛桑，大三本科生Sidharth Hariharan與Viazovska的一次偶然相遇，重新點燃了她對球體堆積證明的興趣。盡管學術生涯尚處起步階段，哈里哈蘭已十分擅長證明的形式化工作。

“對證明的形式化驗證就像一枚官方橡皮圖章，”Fowl說，“它是一份權威認證，確保你的推理與結論準確無誤。”

Hariharan向Viazovska介紹了他是如何通過證明形式化這一過程來學習并真正理解數學概念的。維亞佐夫斯卡對此作出回應，表示主要出于好奇，她也有意將自己的證明進行形式化處理。由此，“在Lean中形式化球體堆積問題（https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/）”項目于2024年3月正式啟動。Lean是一款廣受歡迎的編程語言，同時也是一款證明輔助工具，數學家可以用它編寫證明，再由計算機對證明的絕對正確性進行核驗。

團隊由此展開合作，先撰寫一份人類可讀的“藍圖”，用它梳理出8維證明的各個組成部分，區分哪些已經被形式化和/或證明、哪些尚未完成，再在Lean中對缺失部分進行證明與形式化。

Hariharan如今是卡內基梅隆大學的一年級博士生，他回憶道：“我們為這個項目搭建代碼庫大約15個月后，于2025年6月向公眾開放了訪問權限。同年10月底，我們第一次收到了Math, Inc.公司的聯系。”

AI帶來的提速

Math, Inc.是一家初創公司（https://www.math.inc/），專門研發一款名為Gauss的人工智能，它是專為自動形式化證明而設計的系統。“這是一類特殊的語言模型，我們稱之為推理智能體，它可以把傳統的自然語言推理和完全形式化推理交織在一起。”Math, Inc.聯合創始人兼首席執行官Jesse Han解釋說，“它能夠進行文獻檢索、調用工具、用計算機編寫Lean代碼、記錄筆記、啟動驗證工具、運行Lean編譯器等等。”

去年夏天，Math, Inc.曾因宣布其開發的Gauss在三周內完成了強素數定理（PNT，https://mathstodon.xyz/@tao/111847680248482955）的Lean形式化驗證而登上新聞頭條，而這項工作此前由菲爾茲獎得主陶哲軒與Alex Kontorovich牽頭開展。與此類似，Math, Inc.聯系了Hariharan及其團隊，告知他們Gauss已經證明了與球體堆積項目相關的若干結論。

“他們告訴我們，Gauss完成了30個‘sorry’，這意味著它證明了我們原本希望證明的30個中間結論。”Hariharan解釋道。其中一部分結論被分享給項目團隊，并整合進他們自己的工作中。“其中一個結果還幫我們發現了項目里的一處筆誤，我們隨后進行了修正。”Hariharan補充說，“所以這是一次非常富有成果的合作。”

從8維到24維

但在那之后，雙方便陷入了沉寂，Math, Inc.似乎失去了興趣。不過，就在Hariharan及其團隊繼續投入這項熱愛的工作時，Math, Inc.正在打造全新升級版的Gauss。“我們在1月中旬取得了一項研究突破，推出了性能大幅增強的新版Gauss。”Han表示，“新版本僅用兩三天就復現了此前需要三周才能完成的素數定理形式化工作。”

幾天后，新版Gauss重新投入到球體堆積證明的形式化任務中。依托Hariharan團隊此前提供的寶貴基礎藍圖與已有成果，Gauss僅用五天時間，就不僅自動完成了8維情形的形式化驗證，還發現并修正了已發表論文中的一處筆誤。

Hariharan說：“1月底他們聯系我們，告訴我們已經完成了這項工作時，毫不夸張地說，我們極為震驚。但歸根結底，我們對這項技術感到非常興奮，因為它擁有創造卓越成果的能力，并能以非凡的方式為數學家提供助力。”

Sidharth Hariharan

2月23日宣布的8維球體堆積證明形式化，本身就已是自動形式化與人類–AI協作的分水嶺時刻。而如今，Math, Inc.又公布了一項更令人震撼的成果：Gauss已自動完成Viazovska 24維球體堆積證明的形式化 —— 整整超過20萬行代碼，僅用兩周時間。

8維與24維情形在基礎理論和證明整體架構上存在共通之處，這意味著8維的部分代碼可以重構后復用。然而，這次Gauss沒有現成的藍圖可以直接使用。“事實上，24維的難度遠高于8維，因為有大量缺失的背景內容需要補充，尤其是圍繞Leech lattice的諸多性質，特別是它的唯一性。”Han解釋道。

盡管24維的工作是自動完成的，Han與Hariharan都承認，這一成就離不開人類此前打下的大量基礎，他們將其視作一場人類與AI共同完成的協作成果。

但在Han看來，這一成果的意義更為深遠：它標志著數學領域一場革命性變革的開端 ——未來，超大規模的形式化驗證將成為常態。他總結道：“過去，程序員的工作是在卡片上打孔，后來編程行為與記錄程序的物理載體分離開來。我相信，這類技術最終會讓數學家解放出來，去做他們最擅長的事 —— 構想全新的數學世界。”

閱讀最新前沿科技趨勢報告，請訪問21世紀關鍵技術研究院的“未來知識庫”

未來知識庫是 “21世紀關鍵技術研究院”建 立的在線知識庫平臺，收藏的資料范圍包括人工智能、腦科學、互聯網、超級智能，數智大腦、能源、軍事、經濟、人類風險等等領域的前沿進展與未來趨勢。目前擁有超過8000篇重要資料。每周更新不少于100篇世界范圍最新研究資料。 歡迎掃描二維碼或訪問https://wx.zsxq.com/group/454854145828進入。

截止到2月28日 ”未來知識庫”精選的百部前沿科技趨勢報告

（加入未來知識庫，全部資料免費閱讀和下載）