機(jī)器之心編輯部

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

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

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

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

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

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

去年，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í)間。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

AI 帶來(lái)的加速

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

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

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

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

從 8 維到 24 維

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

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

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

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

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

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

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

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

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

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

展望未來(lái)

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

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

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

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

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

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

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