啥？陶哲軒18個月沒搞定的數學挑戰，被這個“AI高斯”三周完成了

2025-09-15 09:00:00

人工智能新聞

這個名叫Gauss（高斯）的新AI Agent，有點殺瘋了的感覺。

不得了，這個名叫Gauss（高斯）的新AI Agent，有點殺瘋了的感覺。

因為它只用了三周的時間，就完成了陶哲軒和Alex Kontorovich提出的數學挑戰——

在Lean中形式化強素數定理（Prime Number Theorem，PNT）。

要知道，陶哲軒和Kontorovich在2024年1月提出這個挑戰后，足足花了18個月（今年7月）的時間，也才取得階段性的進展。

那么這個Gauss到底是什么來頭？

它的背后是一家叫做Math的AI公司，據介紹，Gauss是首個可以協助頂級數學家進行形式驗證的自動形式化（autoformalization）Agent：

這里的形式化（formalization），指的是把人類寫的數學內容轉換成一種機器可讀、可檢查、嚴密無歧義的形式語言，然后利用計算機幫助驗證其正確性。

而陶哲軒和Alex Kontorovich之所以目前僅取得階段性進展，問題就卡在了復分析（complex analysis）的核心難題上。

而這個Gauss作為硅基生命，它的特點就是可以不停的工作，極大地壓縮了以前只有頂尖形式化專家才能完成的工作量；與此同時，Gauss還形式化了上面提到的復分析中關鍵的缺失結果。

這就是為什么它能三周解決陶哲軒18個月都未能完成的數學挑戰的原因了。

Gauss是如何實現的？

目前Math公司官方并沒有發布具體的技術報告。

但從最終結果來看，Gauss生成了大約25000行Lean代碼，包含上千個定理和定義。

要知道，這種規模的形式化證明，以前往往需要多年才能完成。

歷史上最大的單個形式化項目（往往需要跨甚至10年的時間），也只是比這大一個數量級（最多50萬行代碼）。

相比之下，Lean的標準數學庫Mathlib有約200萬行代碼，包含35萬個定理，但卻由600多位貢獻者花了8年時間才建立起來。

為了支撐Gauss的運行，團隊還和Morph Labs合作開發了Trinity環境基礎設施。

因為要讓Gauss如此大規模運行，會涉及數千個并發Agent，且每個Agent都有自己的Lean運行環境，會消耗數TB的集群內存，是一個極其復雜的系統工程挑戰。

Math團隊還表示：

Gauss將大幅縮短完成大型數學項目所需的時間。
隨著算法不斷進步，我們計劃在未來12個月內，讓形式化代碼的總量提升100到1000倍。
這將成為新范式的訓練場——走向“可驗證的超級智能”和“通才型機器數學家”。

而就在剛剛，陶哲軒本人在Mastodon上對形式化相關的問題做了一番解釋（以下為陶哲軒的陳述）。

任何復雜的項目往往都有明確陳述的目標和隱含的未陳述目標。例如，一個Lean形式化項目的明確目標可能是獲得某個數學命題X的形式化證明；但通常還有一些未陳述的目標，例如以適合上游到 Mathlib 庫的方式形式化X的關鍵子命題和定義X₁, X₂, …；學習如何使用各種協作工具和分配任務；有機地發現X證明的更精細結構，這在以前的非形式化證明中可能沒有被強調；為新手形式化者提供實際培訓和經驗；以及更普遍地建立一個精通形式化藝術的人類社區。

過去，通常沒有必要闡明這些隱含目標，因為這些目標的實現與明確目標的實現之間存在很強的經驗相關性。在形式化項目的例子中，幾乎任何以人為中心的努力來實現明確目標，最終都會自然而然地實現上述大部分隱含目標。因此，明確目標有效地成為了更廣泛實際目標的可行替代。

然而，隨著功能強大的AI工具的出現，情況正在發生變化，這些工具采用與人類截然不同的方法。這些工具可以被指示去解決一個明確的目標，而不必實現如果由人類團隊執行任務時可能同時實現的所有隱含目標。事實上，AI優化算法的性質決定了它們甚至可能以犧牲所有隱含目標為代價，在明確目標上取得高績效。（參見古德哈特定律：“當一個衡量標準成為目標時，它就不再是一個好的衡量標準。”）

鑒于這些工具的日益部署，這向我表明，項目組織者現在需要付出更大的努力，明確闡述項目的所有目標，而不僅僅是名義上的目標。在某些情況下，這些目標甚至可能最初對組織者自己來說并不明顯，可能需要參與者之間進行一些討論。而有興趣用其AI工具測試此類項目的外部各方，則應提前與組織者協調，以防他們遺漏了一個或多個其工具不會優化的關鍵隱含目標。