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

機(jī)器之心編輯部

AI 在數(shù)學(xué)領(lǐng)域的研究取得新進(jìn)展！

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

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

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

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

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

去年，Gauss 只用了三周時(shí)間，就完成了陶哲軒和 Alex Kontorovich 提出的數(shù)學(xué)挑戰(zhàn)，即在 Lean 定理證明器中完成強(qiáng)素?cái)?shù)定理（Prime Number Theorem, PNT）的形式化工作。而該挑戰(zhàn)是在 2024 年 1 月提出，陶哲軒與 Alex Kontorovich 團(tuán)隊(duì)努力了 18 月，才在去年 7 月宣布取得階段性進(jìn)展，可 Gauss 僅用了三周時(shí)間。

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

接下來，我們就來詳細(xì)了解一下。

數(shù)學(xué)領(lǐng)域 AI 與人類協(xié)作的分水嶺時(shí)刻

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

近四年后的今天，Viazovska 再次引發(fā)了學(xué)術(shù)界的關(guān)注。如今，在人類與人工智能的協(xié)作下，她的數(shù)學(xué)證明已被形式化驗(yàn)證，這標(biāo)志著 AI 在輔助數(shù)學(xué)研究方面的能力取得了飛速進(jìn)展。

「這些新成果令人印象非常深刻，絕對標(biāo)志著該領(lǐng)域取得了快速進(jìn)展，」并未參與這項(xiàng)研究的普林斯頓大學(xué)博士后、AI 推理專家 Liam Fowl 評價(jià)道。

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

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

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

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

菲爾茲獎獲獎數(shù)學(xué)研究成果 —— 關(guān)于多維最優(yōu)球體堆積，如今已通過人機(jī)協(xié)作得到正式驗(yàn)證。

機(jī)緣巧合促成形式化項(xiàng)目

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

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

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

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

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

AI 帶來的加速

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

「因此，它能夠進(jìn)行文獻(xiàn)檢索、調(diào)用工具，并使用計(jì)算機(jī)編寫 Lean 代碼、做筆記、啟動驗(yàn)證工具、運(yùn)行 Lean 編譯器等等。」

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

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

從 8 維到 24 維

但是在此之后，對方杳無音訊。Math, Inc. 似乎失去了興趣。然而，就在 Sidharth Hariharan 和同事們繼續(xù)這項(xiàng)出于熱愛的研究時(shí)，Math, Inc. 正在構(gòu)建一個全新且改進(jìn)版的 Gauss。

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

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

Hariharan 說：「當(dāng)他們在 1 月下旬聯(lián)系我們，說他們已經(jīng)完成了這項(xiàng)工作時(shí)，毫不夸張地說，我們感到非常驚訝。但歸根結(jié)底，這是一項(xiàng)讓我們感到極其興奮的技術(shù)，因?yàn)樗心芰Τ删蛡ゴ蟮氖聵I(yè)，并以驚人的方式輔助數(shù)學(xué)家。」

Hariharan 正在進(jìn)行球體填充證明驗(yàn)證，夕陽西下，卡內(nèi)基梅隆大學(xué)哈默施拉格音樂廳后方。

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

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

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

但對 Jesse Han 來說，這代表著更多意義：它標(biāo)志著數(shù)學(xué)領(lǐng)域一場革命性變革的開始，超大規(guī)模的形式化將成為家常便飯。

他總結(jié)道：「過去，程序員就是那些在紙帶卡片上打孔的人，但后來，編程行為與其用來記錄程序的物質(zhì)載體分離開來。我認(rèn)為，這類技術(shù)的最終結(jié)果將是解放數(shù)學(xué)家，讓他們?nèi)プ鲎约鹤钌瞄L的事情 —— 也就是去自由構(gòu)想全新的數(shù)學(xué)世界。」

展望未來

可以說，在這一定理的證明過程中，Gauss 自主證明了大量關(guān)于模形式、離散幾何、圍道積分和傅里葉分析的重要結(jié)論，這一成果也以空前速度推進(jìn)了這一重大數(shù)學(xué)結(jié)果的驗(yàn)證，是自動形式化領(lǐng)域的歷史性成就。

Math, Inc. 認(rèn)為，數(shù)學(xué)形式化將通過使已知成果可搜索、可組合、可機(jī)器導(dǎo)航，加速科研進(jìn)程，而對 8 維與 24 維球體堆積這類結(jié)果的形式化，也深化了大家對數(shù)學(xué)知識統(tǒng)一性的理解 —— 它以嚴(yán)格方式揭示了看似無關(guān)領(lǐng)域之間的深層結(jié)構(gòu)聯(lián)系。

但一個可編譯、無報(bào)錯的形式化證明并非終點(diǎn)，更具挑戰(zhàn)性的工作在于如何在全球尺度上組織、整合與維護(hù)形式化知識。隨著越來越多的證明由 AI 系統(tǒng)產(chǎn)生，如何將其整合進(jìn)持續(xù)擴(kuò)展、相互兼容的知識體系，將成為規(guī)模化發(fā)展的基本要求。

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

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

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

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