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

因為它只用了三周的時間，就完成了陶哲軒和Alex Kontorovich提出的數(shù)學(xué)挑戰(zhàn)——

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

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

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

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

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

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

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

這就是為什么它能三周解決陶哲軒18個月都未能完成的數(shù)學(xué)挑戰(zhàn)的原因了。

Gauss是如何實現(xiàn)的？

目前Math公司官方并沒有發(fā)布具體的技術(shù)報告。

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

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

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

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

為了支撐Gauss的運行，團隊還和Morph Labs合作開發(fā)了Trinity環(huán)境基礎(chǔ)設(shè)施。

因為要讓Gauss如此大規(guī)模運行，會涉及數(shù)千個并發(fā)Agent，且每個Agent都有自己的Lean運行環(huán)境，會消耗數(shù)TB的集群內(nèi)存，是一個極其復(fù)雜的系統(tǒng)工程挑戰(zhàn)。

Math團隊還表示：

Gauss將大幅縮短完成大型數(shù)學(xué)項目所需的時間。

隨著算法不斷進步，我們計劃在未來12個月內(nèi)，讓形式化代碼的總量提升100到1000倍。

這將成為新范式的訓(xùn)練場——走向“可驗證的超級智能”和“通才型機器數(shù)學(xué)家”。

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

任何復(fù)雜的項目往往都有明確陳述的目標(biāo)和隱含的未陳述目標(biāo)。例如，一個Lean形式化項目的明確目標(biāo)可能是獲得某個數(shù)學(xué)命題X的形式化證明；但通常還有一些未陳述的目標(biāo)，例如以適合上游到 Mathlib 庫的方式形式化X的關(guān)鍵子命題和定義X1, X2, …；學(xué)習(xí)如何使用各種協(xié)作工具和分配任務(wù)；有機地發(fā)現(xiàn)X證明的更精細結(jié)構(gòu)，這在以前的非形式化證明中可能沒有被強調(diào)；為新手形式化者提供實際培訓(xùn)和經(jīng)驗；以及更普遍地建立一個精通形式化藝術(shù)的人類社區(qū)。

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

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

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

創(chuàng)始人是ICML’25時間檢驗獎作者

值得一提的是，Math這家公司的老板也是有點實力在身上的。

因為他正是拿下今年AI定會ICML時間檢驗獎?wù)撐牡淖髡咧唬?strong>Christian Szegedy。

這篇論文是他和另一位作者Sergey Loffe在2015年提出的Batch Normalization（批次歸一化，簡稱BatchNorm）。

如今，這篇論文的引用量超過6萬次，是深度學(xué)習(xí)發(fā)展史上一個里程碑式的突破，極大地推動了深層神經(jīng)網(wǎng)絡(luò)的訓(xùn)練和應(yīng)用。

可以說它是讓深度學(xué)習(xí)從小規(guī)模實驗，走向大規(guī)模實用化和可靠性的關(guān)鍵技術(shù)之一。

當(dāng)然，網(wǎng)友們看罷Gauss之后雖然驚呼Amazing，但同時也在喊官方趕緊把論文公開嘍。

至于更細節(jié)的技術(shù)內(nèi)容，我們可以蹲一波了~