菲爾茲獎成果首次被AI完整形式化，Gauss20萬行代碼改寫數學史？

機器之心編輯部

AI 在數學領域的研究取得新進展！

近日，一家名為 Math, Inc. 的公司宣稱利用 Gauss 智能體，已經完成了一個關乎 8 維和 24 維空間中的最優球體堆積定理的形式化證明，代碼量約為 20 萬行（LOC）。

這一定理最初由數學家瑪麗娜?維亞佐夫斯卡（Maryna Viazovska）及其合作者證明，Maryna Viazovska 也憑此榮獲 2022 年國際數學家大會菲爾茲獎。

據悉，這是本世紀唯一一個被完全形式化證明的菲爾茲獎成果，也是歷史上規模最大的單一用途 Lean 形式化項目。

而背后的這家名為 Math, Inc. 的公司，也不是第一次完成數學問題的形式化證明了。

資料顯示，Math, Inc. 是由 xAI 前聯合創始人、Morph Labs 首席科學家 Christian Szegedy 創立，致力于通過自動形式化技術打造可驗證超級智能，Gauss 則是首款專為協助數學專家開展形式化驗證工作打造的自動形式化智能體。

去年，Gauss 只用了三周時間，就完成了陶哲軒和 Alex Kontorovich 提出的數學挑戰，即在 Lean 定理證明器中完成強素數定理（Prime Number Theorem, PNT）的形式化工作。而該挑戰是在 2024 年 1 月提出，陶哲軒與 Alex Kontorovich 團隊努力了 18 月，才在去年 7 月宣布取得階段性進展，可 Gauss 僅用了三周時間。

而這一次，在高維球體堆積問題的形式化證明過程中，Gauss 的速度仍然驚人……

接下來，我們就來詳細了解一下。

數學領域 AI 與人類協作的分水嶺時刻

2022 年 7 月，烏克蘭數學家 Maryna Viazovska 榮獲被廣泛譽為「數學界諾貝爾獎」的菲爾茲獎，這在當時引起了巨大轟動，她是該獎項 86 年歷史上第二位獲此殊榮的女性。

近四年后的今天，Viazovska 再次引發了學術界的關注。如今，在人類與人工智能的協作下，她的數學證明已被形式化驗證，這標志著 AI 在輔助數學研究方面的能力取得了飛速進展。

「這些新成果令人印象非常深刻，絕對標志著該領域取得了快速進展，」并未參與這項研究的普林斯頓大學博士后、AI 推理專家 Liam Fowl 評價道。

在她獲得菲爾茲獎的研究中，Viazovska 攻克了兩個版本的球體填充問題。該問題探討的是：在 n 維空間中，相同的圓、球體等能以多大的密度進行排列？

在二維空間中，蜂窩結構是最佳方案。在三維空間中，將球體堆疊成金字塔狀則是最優解。但在此之后，要想找到最佳解并證明它確實是最優的，就變得極其困難。

2016 年，Viazovska 解決了其中兩種維度下的問題。通過使用被稱為（準）模形式的強大數學函數，她證明了一種名為 E (8) 的對稱排列是 8 維空間中的最佳填充方式；不久之后，她又與合作者共同證明了另一種被稱為水蛭晶格（Leech lattice）的球體填充方式是 24 維空間中的最優解。盡管這看起來非常抽象，但該成果有望幫助解決日常生活中與高密度球體填充相關的實際問題，包括智能手機和太空探測器所使用的糾錯碼。

這些證明經過了數學界的驗證并被確認為正確，這也為她贏得了菲爾茲獎。但是，形式化驗證（即證明能夠被計算機絕對驗證的能力）完全是另一回事。自 2022 年以來，AI 輔助的形式化證明驗證已經取得了長足的進步。

菲爾茲獎獲獎數學研究成果 —— 關于多維最優球體堆積，如今已通過人機協作得到正式驗證。

機緣巧合促成形式化項目

幾年后，在瑞士洛桑，讀大三的本科生 Sidharth Hariharan 與 Viazovska 的偶然相遇，重新點燃了她對球體填充證明的興趣。盡管 Hariharan 處于學術生涯的極早期，但他已經熟練掌握了形式化證明。

「對證明進行形式化驗證就像蓋上了一枚橡皮圖章，」 Fowl 說道，「這是一種真正的權威認證，能證明你的推理陳述是絕對正確的。」

Hariharan 告訴 Viazovska，他一直通過形式化證明的過程來學習和真正理解數學概念。對此，Viazovska 主要出于好奇，表達了對將自己的證明進行形式化的興趣。由此，在 2024 年 3 月，「在 Lean 中形式化球體填充」（Formalising Sphere Packing in Lean）項目應運而生。Lean 是一種流行的編程語言和「證明助手」，它允許數學家編寫證明，然后由計算機驗證其絕對的正確性。

這個協作項目匯集了倫敦帝國理工學院的 Bhavik Mehta、英國東安格利亞大學的 Christopher Birkbeck、加州大學伯克利分校的 Seewoo Lee 等專家。該項目的核心工作是編寫一份人類可讀的「藍圖」，用來梳理 8 維證明的各個組成部分，明確哪些已經或尚未被形式化和 / 或證明，隨后在 Lean 環境中證明并形式化那些缺失的元素。

「在 2025 年 6 月開放公眾訪問之前，我們已經為這個項目的代碼庫構建了大約 15 個月，」現已是卡內基梅隆大學博士一年級學生的 Sidharth Hariharan 回憶道，「隨后，在 10 月下旬，我們首次收到了 Math, Inc. 公司的消息。」

AI 帶來的加速

Math, Inc. 是一家初創公司，正在開發一款名為 Gauss 的人工智能，專門用于自動形式化證明。「這是一種被稱為推理智能體的特殊語言模型，旨在將傳統的自然語言推理與完全形式化的推理交織在一起，」Math, Inc. 首席執行官兼聯合創始人 Jesse Han 解釋說。

「因此，它能夠進行文獻檢索、調用工具，并使用計算機編寫 Lean 代碼、做筆記、啟動驗證工具、運行 Lean 編譯器等等。」

Math, Inc. 首次登上頭條新聞是在去年夏天，當時該公司宣布 Gauss 用了三周時間完成了強素數定理（PNT）在 Lean 中的形式化，而這項任務原本是菲爾茲獎得主陶哲軒和 Alex Kontorovich 一直在努力攻克的。同樣地，Math, Inc. 聯系了 Hariharan 及其同事，告知他們 Gauss 已經證明了與他們的球體填充項目相關的幾個事實。

Hariharan 解釋道：「他們告訴我們，他們完成了 30 個 sorry（注：Lean 語言中表示待證明環節的占位符），這意味著他們證明了 30 個我們需要驗證的中間事實。」其中一部分證明被分享給了項目團隊，并與他們自己的工作成果進行了合并。「其中一個證明甚至幫我們發現了項目中的一個排版錯誤，隨后我們進行了修正，」 Hariharan 補充說，「所以這是一次非常富有成效的合作。」

從 8 維到 24 維

但是在此之后，對方杳無音訊。Math, Inc. 似乎失去了興趣。然而，就在 Sidharth Hariharan 和同事們繼續這項出于熱愛的研究時，Math, Inc. 正在構建一個全新且改進版的 Gauss。

「我們在 1 月中旬取得了研究上的突破，打造出了一個功能更強大的 Gauss 版本，」 Jesse Han 說道，「這個新版本只用兩三天的時間，就重現了我們之前花了三周才完成的 PNT 成果。」

幾天后，新版 Gauss 被重新引向了球體填充的形式化任務。基于 Hariharan 和合作者分享的寶貴藍圖和已有工作，Gauss 不僅自動形式化了 8 維的情況，還在短短五天內發現并修復了已發表論文中的一個排版錯誤。

Hariharan 說：「當他們在 1 月下旬聯系我們，說他們已經完成了這項工作時，毫不夸張地說，我們感到非常驚訝。但歸根結底，這是一項讓我們感到極其興奮的技術，因為它有能力成就偉大的事業，并以驚人的方式輔助數學家。」

Hariharan 正在進行球體填充證明驗證，夕陽西下，卡內基梅隆大學哈默施拉格音樂廳后方。

僅僅是 2 月 23 日宣布的 8 維球體填充證明形式化，就已經代表了自動形式化和人機協作的分水嶺時刻。但在今天，Math, Inc. 揭曉了一項更加令人矚目的成就：Gauss 在短短兩周內，自動形式化了 Viazovska 24 維球體填充的證明 —— 包含了超過 20 萬行的全部代碼。

8 維和 24 維的情況在基礎理論和證明的整體架構上存在共通之處，這意味著 8 維案例中的部分代碼可以被重構和復用。然而，這一次 Gauss 并沒有現成的藍圖可供參考。「它實際上比 8 維的情況復雜得多，因為圍繞水蛭晶格的許多屬性（尤其是它的唯一性），有大量缺失的背景材料需要被整合，」 Jesse Han 解釋道。

盡管 24 維的證明過程是一項自動化的工作，但 Jesse Han 和 Hariharan 都承認，正是人類的眾多貢獻為這一成就奠定了基礎。總體而言，他們將此視為人類與 AI 通力協作的結晶。

但對 Jesse Han 來說，這代表著更多意義：它標志著數學領域一場革命性變革的開始，超大規模的形式化將成為家常便飯。

他總結道：「過去，程序員就是那些在紙帶卡片上打孔的人，但后來，編程行為與其用來記錄程序的物質載體分離開來。我認為，這類技術的最終結果將是解放數學家，讓他們去做自己最擅長的事情 —— 也就是去自由構想全新的數學世界。」

展望未來

可以說，在這一定理的證明過程中，Gauss 自主證明了大量關于模形式、離散幾何、圍道積分和傅里葉分析的重要結論，這一成果也以空前速度推進了這一重大數學結果的驗證，是自動形式化領域的歷史性成就。

Math, Inc. 認為，數學形式化將通過使已知成果可搜索、可組合、可機器導航，加速科研進程，而對 8 維與 24 維球體堆積這類結果的形式化，也深化了大家對數學知識統一性的理解 —— 它以嚴格方式揭示了看似無關領域之間的深層結構聯系。

但一個可編譯、無報錯的形式化證明并非終點，更具挑戰性的工作在于如何在全球尺度上組織、整合與維護形式化知識。隨著越來越多的證明由 AI 系統產生，如何將其整合進持續擴展、相互兼容的知識體系，將成為規模化發展的基本要求。

未來，Math, Inc. 將繼續與球體堆積項目及其他形式化數學庫的維護者合作，確保 Gauss 生成的代碼在未來仍具可用性與可維護性。

https://x.com/mathematics_inc/status/2028542388717986135

https://spectrum.ieee.org/ai-proof-verification

https://www.math.inc/sphere-packing