陶哲軒最新演講：AI時代，數(shù)學(xué)研究將進(jìn)入前所未有的規(guī)模

西風(fēng) 發(fā)自 凹非寺

量子位 | 公眾號 QbitAI

陶哲軒最新演講公開，AI含量爆表。

在IMO 2024現(xiàn)場，“陶神”帶來了洋洋灑灑1個小時的精彩分享，主題就叫：AI與數(shù)學(xué)。

他怎么看AI和數(shù)學(xué)的關(guān)系？怎么理解機器學(xué)習(xí)、大模型等在數(shù)學(xué)領(lǐng)域的應(yīng)用與發(fā)展？

所有觀察和觀點都毫無保留分享：

借助AI，可以想象未來可以取一類1000個問題同時處理，你真的可以開始以一種前所未有的規(guī)模進(jìn)行數(shù)學(xué)研究。

除此之外，“陶神”還由古至今講述了機器輔助計算的傳統(tǒng)與演變。

AI等一系列機器在數(shù)學(xué)研究中的妙用并非空口無憑：

• 畢達(dá)哥拉斯三元數(shù)組的問題只能使用計算機解決
• 開普勒猜想最終也是借由計算機輔助證明
• 機器學(xué)習(xí)在紐結(jié)理論中的應(yīng)用：已經(jīng)能夠幫助猜測兩種不同統(tǒng)計數(shù)據(jù)之間的聯(lián)系

他本人還透露，自己用GPT-4找解題靈感；用GitHub Copilot輔助證明，大概有20%概率，它能寫出接近正確的下一步證明。

不光是在演講中講AI，陶哲軒最近發(fā)布的幾個帖子也都和AI息息相關(guān)。

網(wǎng)友紛紛安利：

他沒有支持或反對AI炒作，而只是理性開放地評估了這些工具及其能力，還有未來可能發(fā)生的事。

量子位在不改變原意的基礎(chǔ)上，對“陶神”這次最新的演講內(nèi)容進(jìn)行了編譯整理。

“陶神”從機器輔助計算的傳統(tǒng)開始講起，又接著講了大致以下幾個板塊的內(nèi)容：

• 計算機起初最基本的用途
• 機器在科學(xué)計算中的應(yīng)用
• 現(xiàn)代用機器進(jìn)行數(shù)學(xué)研究的創(chuàng)造性方法：證明助手、機器學(xué)習(xí)、大語言模型

長期以來就有機器輔助計算的傳統(tǒng)

你們都聽說過AI以及它如何改變一切。早些時候有一個DeepMind發(fā)布了一個AlphaGeometry，現(xiàn)在可以回答一些IMO幾何問題。

我將更多地討論這些工具是如何開始改變數(shù)學(xué)研究的。

這與數(shù)學(xué)競賽不同，不是設(shè)定三個小時什么的來解決一個問題，而是需要幾個月甚至更長時間，有時解決不了問題，那就必須改變問題。這絕對不同于數(shù)學(xué)競賽，盡管在技能上有些重疊。

這一切都非常令人興奮，它正在開始具有變革性。但另一方面，也有一種連續(xù)性的感覺，我們實際上已經(jīng)使用計算機和機器來做數(shù)學(xué)運算很長時間了，而我們進(jìn)行這些運算的方式的本質(zhì)正在發(fā)生變化。

但實際上，這是遵循了長期以來機器輔助的傳統(tǒng)。

那么，問題來了。我們使用機器來做數(shù)學(xué)已經(jīng)有多久了？答案是數(shù)千年。

這是羅馬人曾經(jīng)用來做數(shù)學(xué)的機器，算盤是早期的機器，甚至還有一些更早的。聽起來可能有點無聊，這些并不是非常智能的機器。

計算機呢？我們使用計算機做數(shù)學(xué)多久了？大約是三四百年。這有點奇怪，因為你知道，我們的電子計算機直到20世紀(jì)三四十年代才出現(xiàn)。

但在電子計算機之前，計算機曾經(jīng)是機械式的，計算機也曾指進(jìn)行計算的人，是一種職業(yè)。

曾經(jīng)有人力“計算機集群”，人使用加法機計算彈道學(xué)等問題，計算能力的基本單位不靠CPU，而是kilgirl，即1000名女性1小時可以完成多少計算任務(wù)，當(dāng)時男人們都在打仗。

計算機最基本的用途是制作表格

人們很早就在使用計算機，正如我之前所說，實際上早在17世紀(jì)甚至更早之前就開始使用了。

那時計算機最基本的用途是制作表格（table），你可能聽說過納皮爾的對數(shù)表。

如果你想計算正弦、余弦等，你會使用計算機生成這些表格。我高中上課時仍會學(xué)習(xí)如何使用這些表格，它們剛剛被淘汰。

當(dāng)然，現(xiàn)在我們有計算器和現(xiàn)代計算機。

我的意思是，在數(shù)學(xué)研究中，我們依賴于表格，現(xiàn)在我們稱它們?yōu)?strong>數(shù)據(jù)庫，但它們本質(zhì)上還是一樣的東西。

在數(shù)學(xué)中有許多重要的成果最初是通過表格發(fā)現(xiàn)的。

例如，數(shù)論中最基本的成果之一——素數(shù)定理。它大致告訴你在一個大數(shù)x之前有多少個素數(shù)，這一發(fā)現(xiàn)歸功于勒讓德和高斯等人。

當(dāng)時他們雖未能證明它，但由于高斯和其他人使用了早期的計算設(shè)備，他們推測這一理論是正確的。實際上，高斯自己就像一個計算機一樣，計算表格并嘗試找出規(guī)律。

之后還出現(xiàn)了另一個重要猜想——Birch and Swinnerton-Dyer猜想，這里不詳述。這個猜想也是人類通過查看大量關(guān)于曲線的數(shù)據(jù)表格然后首次發(fā)現(xiàn)的。

如今，包括我在內(nèi)的許多數(shù)學(xué)家使用的一個表格，是所謂的Online Encyclopedia of Integer Sequences（OEIS），它收集了大量數(shù)學(xué)序列數(shù)據(jù)。

也許你遇到過它，像“1, 1, 2, 3, 5, 8,13”，你知道這是斐波那契數(shù)列，OEIS是一個數(shù)據(jù)庫，有成千上萬這樣的序列。

在數(shù)學(xué)研究中，數(shù)學(xué)家經(jīng)常會遇到一些自然出現(xiàn)的數(shù)字序列，這些序列可能依賴于變量n，如空間的維數(shù)、集合的基數(shù)等。

你可以計算這些序列的前五個、六個或十個數(shù)字，然后將其輸入到OEIS中進(jìn)行比較。如果幸運的話，這個序列可能已經(jīng)被別人放在那里了，可能來源于對某個完全不同的數(shù)學(xué)問題的研究。

這樣的發(fā)現(xiàn)可以大大提示兩個問題之間可能存在的聯(lián)系，許多研究就是這樣開始的。

機器在科學(xué)計算中的應(yīng)用

機器在數(shù)學(xué)領(lǐng)域的另一個重要應(yīng)用是科學(xué)計算（scientific computation）。

當(dāng)你需要執(zhí)行大規(guī)模計算時，你會將大量的算術(shù)運算任務(wù)丟給計算機。自1920年代以來，這一做法已廣泛被采用。

也許第一個真正進(jìn)行科學(xué)計算的人是亨德里克·洛倫茲。

我記得是荷蘭人想要建一個巨大的堤壩，委托他想弄清楚水流會怎樣變化。所以他們必須建立模型和一些流體方程，洛倫茲實際上使用了一群人類“計算機”來解決這個問題，采用了浮點運算。

他意識到，如果你想讓很多人很快地完成大量計算，你應(yīng)該用浮點數(shù)來表示各種不同大小的數(shù)字。當(dāng)然，我們現(xiàn)在使用計算機來模擬各種事物。

如果你在解決許多線性方程或者不同的方程，你可能想進(jìn)行一些組合計算，也可以解決代數(shù)問題。你在IMO中看到的許多幾何問題原則上都可以通過科學(xué)計算來解決。

有一些代數(shù)軟件包，你可以將任何幾何問題，比如涉及10個點和一些線和圓的問題，轉(zhuǎn)化為一個包含20個實數(shù)和20個未知數(shù)的方程系統(tǒng)，然后輸入到如Sage或Maple等軟件中。

不過，隨著問題規(guī)模的擴大，解決問題的計算復(fù)雜性可能會呈指數(shù)級或雙指數(shù)級增長，會超出傳統(tǒng)計算機代數(shù)軟件包的處理能力。

因此直到最近，還不可能僅用標(biāo)準(zhǔn)的計算機代數(shù)軟件包來暴力解決這些問題。但現(xiàn)在有了AI的輔助，情況可能有希望改變。

另一種強大的科學(xué)計算類型是所謂的SAT求解器，可以用來解決某種邏輯謎題。

例如，你有1000個或真或假的陳述，而且你知道如果第三個陳述是真的，第六個陳述也是真的，那么第七個陳述必然是假的。如果你給出了一系列這樣的約束條件，SAT求解器就會嘗試?yán)盟羞@些信息，來得出例如能否證明這些陳述中的某些是對還是錯等結(jié)論。

還有一個更高級的版本稱為SMT求解器。如果你有一些變量x、y、z，并且假設(shè)一些定律等等，你可以將這些定律和一些其它事實輸入進(jìn)去，嘗試簡單暴力地在有限的假設(shè)中得出結(jié)論。

這些非常強大，但也不能很好地擴展。再次強調(diào)，問題的復(fù)雜度可能使運算時間呈指數(shù)增長，因此一旦超過大約1000個命題，對這些求解器來說，再運行就變得非常非常困難。

不過，計算機實際上可以解決一些問題。

例如，一個成功案例是在組合數(shù)學(xué)中的應(yīng)用，我認(rèn)為人類在沒有幫助的情況下解決這個問題是不可能的，也許只能通過計算機解決。

問題關(guān)于畢達(dá)哥拉斯三元組（勾股數(shù)組）：

將自然數(shù)涂成紅色或藍(lán)色兩種顏色，無論怎樣涂色，是否總有一種顏色包含畢達(dá)哥拉斯三元組abc？

此問題以前并未得到驗證，直到一臺大型計算機進(jìn)行計算之后才被解決。

現(xiàn)在我們知道，你無需檢查所有自然數(shù)。

對于自然數(shù)1到7824，可以將其分為兩種顏色，其中任何一種顏色中都不包含畢達(dá)哥拉斯三元組。但對于自然數(shù)1到7825，是一定會包含的。

我認(rèn)為這是當(dāng)時世界上最長的證明，現(xiàn)在是第二長的證明了。這個證明需要4個CPU年的計算時間，并且最終生成了一個包含200TB數(shù)據(jù)的證明文件，該文件后來被壓縮至86GB。

所以這是使用計算機的一種相當(dāng)明顯的方式。

現(xiàn)在使用計算機研究的三種創(chuàng)意方式

最近幾年，我們開始用更具創(chuàng)造性的方式使用計算機，特別是將它們與彼此以及更傳統(tǒng)的數(shù)據(jù)庫、表格、科學(xué)計算相結(jié)合。

我們使用機器學(xué)習(xí)神經(jīng)網(wǎng)絡(luò)以不同于人的方式來發(fā)現(xiàn)新的聯(lián)系，找出不同類型的數(shù)學(xué)之間的相關(guān)方式。

最引人注目的是大語言模型，它可以進(jìn)行自然語言對話，像ChatGPT、Claude等，有時它們可以產(chǎn)生解決問題的有效方法。

還有另一種技術(shù)被數(shù)學(xué)家們使用——形式證明助手（formal proof assistants）。

這些工具本質(zhì)上是編程語言，就像你使用計算機語言編寫可執(zhí)行代碼一樣，形式證明助手是用來檢驗事物的語言，它們幫助你驗證某個論證是否真實，并從數(shù)據(jù)中得出結(jié)論。

最近這些工具的使用變得相對易用，且正在助力許多有趣的數(shù)學(xué)項目，這些項目在沒有形式證明助手的幫助下是不可能實現(xiàn)的。

未來，它們將與我提到的其它工具很好地結(jié)合起來。

所以我想談?wù)勈褂矛F(xiàn)代計算機和機器進(jìn)行數(shù)學(xué)研究的方法，從證明助手開始。

證明助手

第一個真正的計算機輔助證明也許是四色定理的證明。

這個定理在1976年得到了證明：任何一張地圖只用四種顏色進(jìn)行著色，就能使相鄰區(qū)域的顏色不相同。

△圖源維基百科

他們證明四色定理的方式基本上是對國家數(shù)量進(jìn)行歸納。你需要展示如果你有一張龐大的地圖，那么就會存在一些國家的子圖，他們列出了大約1000到2000個特殊的子圖，每一個龐大的國家圖在某種意義上都必須包含這些子圖中的至少一個，這是他們必須檢查的一件事。

然后他們必須檢查每當(dāng)你有一個子圖時，你可以用更簡單的東西替換這個子圖，如果你能用四種顏色來著色這個更簡單的東西，你就能給主圖著色。

還有可簡化性，對于這些子圖中的每一個都要進(jìn)行檢查。

這些任務(wù)中的一些可以由計算機完成，還有一些任務(wù)是人工花費數(shù)小時手動檢查的。

我認(rèn)為，這是一個需要重新審視的過程，它非常乏味，并且過程并不完美，存在許多小錯誤。按照現(xiàn)代的計算機證明標(biāo)準(zhǔn)，這并不是一個可以被計算機驗證的證明。

這種情況直到90年代才有所改變，那時出現(xiàn)了一個使用大約700個子圖的更簡單的證明。

2005年，使用Coq證明輔助工具，實現(xiàn)了完全形式化的計算機可驗證證明。

我們可以看到，從首次證明出現(xiàn)到我們實際上能夠完全通過計算機驗證之間有一個巨大的差距。

另一個著名的例子是關(guān)于球體最密堆積的幾何問題——開普勒猜想。

開普勒猜想稱，在三維空間中，最密的球體排列方式是面心立方堆積（FCC）和六方最密堆積（HCP）。這兩種排列方式的球體占據(jù)的體積比約為74.048%，這是所有可能的排列方式中最大的。

△圖源維基百科

怎么確定這種堆積方式是否是最好的？這成為一個特別難的問題，并沒有一個完全對人類可讀的猜想證明。

問題在于，對于無窮多的球體，密度是一個漸進(jìn)的事情，所以它不是一個先驗的有限問題，你不能僅僅把它扔給計算機來解決。

但是你可以試著把它簡化為有限的問題。

每次進(jìn)行堆積時，它會將空間細(xì)分為被稱為Voronoi區(qū)域的多面體。球的Voronoi多面體就是所有距離該球中心最近的點所組成的區(qū)域，這些多面體都有特定的體積，你還可以計算它們的面數(shù)和表面積等，并因此獲得這些統(tǒng)計數(shù)據(jù)。

Toth在20世紀(jì)50年代提出了一種策略。他觀察到某些加權(quán)不等式基于有限多個Voronoi多面體的體積能得到球堆積密度的上界。

你可以嘗試建立這些多面體之間的關(guān)系，比如，如果一個多面體非常大，可能會迫使附近的多面體變得非常小，因此你可以嘗試找到一些連接一個多面體的體積與另一個多面體的體積的不等式。

許多研究者嘗試過這種方法，有些甚至聲稱成功，但沒有一個得到認(rèn)可能作為確切的證明。

最終，這個問題由Thomas Hales及其合作者解決。他采用了基本相同的策略，但加入了許多技術(shù)性調(diào)整。

他們把Voronoi單元改進(jìn)得更精細(xì)，并不只是簡單測量體積，而是創(chuàng)造了一個綜合得分，將體積和多個小的臨時調(diào)整結(jié)合起來。他的目標(biāo)是在這些不同得分之間建立線性不等式，從而最終得到密度的上限，并希望精確地達(dá)到最優(yōu)密度。

這種方法極具靈活性，但也因為可嘗試的方案過多而顯得過于復(fù)雜。

Thomas Hales和其學(xué)生Samuel Ferguson意識到，每次他們在解決最小化問題時遇到困難，都能調(diào)整評分函數(shù)來回避這些困難。函數(shù)變得更加復(fù)雜，每次更改都可能花費很長時間。

更糟糕的是，這個函數(shù)與之前論文中的內(nèi)容略有不兼容，就需要回頭去修改之前的論文。

最初，他們并沒有計劃依賴計算機，但隨著項目變得越來越復(fù)雜，必須越來越多地依賴計算機處理。

到1998年，他們最終宣布該項目成功，從一個精心選擇的包含150個變量的優(yōu)化問題中，通過線性規(guī)劃計算得出了開普勒猜想的證明。

證明包括了250頁的筆記和3GB的計算機程序、數(shù)據(jù)和結(jié)果。

這個證明在審核過程中遇到了重大困難。它被提交給了一些頂尖的數(shù)學(xué)期刊，評審過程耗時四年，由一個專家小組負(fù)責(zé)。

在評審結(jié)束時，他們表示對證明的正確性有99%的把握，但他們無法確認(rèn)計算機計算的正確性。他們采取了一種非常不尋常的做法，即在發(fā)表論文時添加了一個注釋來說明這一點。后來，他們撤銷了這個注釋。

當(dāng)時，是否接受計算機輔助證明作為正式證明存在很大爭議?，F(xiàn)在，我們對此更加自信，但即便在論文發(fā)表后，關(guān)于其是否真正構(gòu)成證明仍有疑問。

因此，這可能是第一個真正需要將問題完全按照基本原則形式化的高知名度案例。為此，Hales開發(fā)了一種語言，稱之為Flyspeck項目。

他最初估計需要20年來形式化他們的證明，但實際上，在21位合作者的幫助下，他僅用了12年時間就完成了。最終，這一成果在2014年公布。

因此，我們現(xiàn)在對這一結(jié)果充滿信心。

我們已經(jīng)開始探索更好的工作流程來進(jìn)行形式化，雖然這一過程仍然很繁瑣，但正在逐步改進(jìn)。

Peter Scholze是一位非常杰出的年輕數(shù)學(xué)家，他因許多成就而聞名，尤其是創(chuàng)建了一個被稱為“濃縮數(shù)學(xué)”的數(shù)學(xué)領(lǐng)域。

這個領(lǐng)域利用代數(shù)、范疇論及其它代數(shù)工具，來解決傳統(tǒng)上抵抗代數(shù)方法的泛函分析和函數(shù)空間理論等問題。

Scholze建立了包括所謂的濃縮abelian群和向量空間的一整套范疇。他的主要觀點是，我們在研究生課程中學(xué)習(xí)的所有關(guān)于函數(shù)空間的分類都是不準(zhǔn)確的，或者它們不是最自然的，而他提出的分類具有更好的屬性。

然而，有一個非常重要的消失定理他需要證明。這個定理的證明涉及到某個范疇理論群的非常技術(shù)性的計算。因此，這成為了他理論的基礎(chǔ)。

他在一篇博客文章中討論了這一結(jié)果，提到他花了一整年時間沉迷于這個定理的證明，幾乎陷入瘋狂。最終，他們設(shè)法將論證印刷在紙上，但沒有人敢深入探查這些細(xì)節(jié)，所以他仍然有持續(xù)的疑慮。

有了這個定理，這種濃縮公式在泛函分析中的應(yīng)用才站得住腳。這極為基礎(chǔ)且重要，因此，99.9%的確定性還不夠。

世界各地有許多關(guān)于濃縮數(shù)學(xué)的研究小組，但他們都未能完成這個定理的證明。這個證明過程并不有趣，所以他說這可能是他最重要的成就，但必須確保其正確性。

后來，使用了一種更現(xiàn)代的、稱為Lean的程序語言。

Lean是近些年發(fā)展起來的一種語言，它是一個眾包項目，旨在開發(fā)龐大的數(shù)學(xué)庫。與其從數(shù)學(xué)的基本公理推導(dǎo)一切，這個庫已經(jīng)證明了許多中間結(jié)果，如本科數(shù)學(xué)課程中可能會看到的基礎(chǔ)群論、拓?fù)鋵W(xué)等主題，這些已經(jīng)被形式化了。

但為了形式化這個理論，他們不得不添加許多額外內(nèi)容，盡管數(shù)學(xué)庫還不完整，仍有很多領(lǐng)域，如同調(diào)代數(shù)、層理論等需要添加到庫中，但在短短18個月內(nèi)，他們形式化了這個定理。

證明基本正確，盡管存在一些小的技術(shù)問題，但沒有發(fā)現(xiàn)重大錯誤，他們找到了一些簡化的技巧，有些技術(shù)步驟過于復(fù)雜而難以形式化，因此他們被迫尋找了一些捷徑。

實際上，這個項目的價值更多的是間接的。

首先，他們大大豐富了Lean數(shù)學(xué)庫?，F(xiàn)在，這個數(shù)學(xué)庫可以處理大量的抽象代數(shù)，遠(yuǎn)遠(yuǎn)超過了以前的能力。此外，還有其它支持軟件被建立起來，例如blueprint（藍(lán)圖）。

直接形式化一個龐大的證明，比如50頁的證明，真的很痛苦，你必須把整個證明記在腦海中。

正確的工作流程是，你拿一個大的證明，首先編寫一個blueprint，它將這個證明分解成數(shù)百個小步驟。每一步都可以單獨形式化，然后再將它們?nèi)拷M合起來。你的團(tuán)隊中不同的人可以在不同的步驟中形式化論證不同部分。

這個項目的另一個成果是，現(xiàn)在我們有了一個由數(shù)萬行代碼組成的形式化證明。目前正在努力將這個證明轉(zhuǎn)換為人類可讀的格式。此外，還開發(fā)了一些工具，可以將用Lean這種語言編寫的證明轉(zhuǎn)換回人類可讀的形式。

例如，這里有一個拓?fù)鋯栴}的證明，它已被成功轉(zhuǎn)換為人類可以理解的格式。

因此，這些文本都是從形式化證明中計算機生成的。它看起來像是人類編寫的證明，使用了相同類型的數(shù)學(xué)語言，但更具交互性。

你可以點擊任何位置，系統(tǒng)會告訴你當(dāng)前的假設(shè)、你正在嘗試證明什么、變量是什么。如果某個步驟太簡短，你可以展開它以了解其來源，并且可以深入到你想要的公理。

我認(rèn)為這是非常好的創(chuàng)新，我相信未來我們編寫的教科書將采用這種互動式風(fēng)格，首先進(jìn)行形式化，然后你將擁有比現(xiàn)有教科書更具互動性的版本。

受此啟發(fā)，我自己也開始了一個形式化的項目。

去年，我與包括Tim Gowers在內(nèi)的幾個人一起解決了一個組合學(xué)問題。它涉及到一個具有“小倍增”性質(zhì)的二進(jìn)制Hamming立方體的子集，這個子集的大小有一定的限制。

我們在相對較短的時間內(nèi)將其形式化，證明大約有33頁長。

實際上，這可能仍是迄今為止最快完成形式化的實際研究論文，在三周內(nèi)由大約20人的團(tuán)隊完成，利用了Scholze項目中開發(fā)的所有這些blueprint。

因此，它使得證明任務(wù)變得更加開放，協(xié)作性更強，你還可以獲得精美的可視化效果。

正如我所說，你要做的第一件事是把你的大定理分解成許多小塊。我們得到的定理稱為PFR，對應(yīng)于這里圖表底部的一個小圈。

然后我們引入了所有這些其它證明，PFR證明必須依賴于幾個先前的證明。

因此，存在一個依賴圖，它們的顏色取決于你是否已經(jīng)形式化它們。綠色圈是一個已經(jīng)用形式化證明的，藍(lán)色圈是尚未被形式化證明，但已準(zhǔn)備好被形式化，比如所有定義都已到位。白色圈，即使證明還沒有被形式化，必須有人編寫。

因此，你得到了這個任務(wù)樹，而這個項目的美妙之處在于你可以讓所有這些人獨立地在這張圖的不同部分上協(xié)作。

參與者中有些人甚至不是數(shù)學(xué)家，他們是計算機程序員，但他們非常擅長做這些小型拼圖式的事情。每個人都選擇了他們認(rèn)為能做的一個圈，并最終在三周內(nèi)完成了整個項目，這是一個非常激動人心的項目。

你知道，在數(shù)學(xué)領(lǐng)域，我們通常不會與這么多人合作，我見過的最多是5個人。這是因為當(dāng)你在一個大項目上合作時，你必須信任每個人的數(shù)學(xué)都是正確的，超過一定規(guī)模，這就變得不可行。

但有了這樣一個項目，Lean編譯器會自動檢查，你不能上傳任何無法編譯的內(nèi)容，所以你可以與你從未見過的人合作。

這是一個例子，我認(rèn)為這將成為未來進(jìn)行數(shù)學(xué)研究的一種越來越普遍的方式。

雖然工具正在改進(jìn)且變得更加用戶友好，但仍然很痛苦，且需要具備一定的編程專業(yè)知識。

另一方面，如果你需要修改你的證明，比如，這個定理中原來有一個12，后來要把12改進(jìn)成11，從而得到了一個稍強一些的定理。

通常情況下，如果你這么做，你必須重寫整個證明，或者嘗試將12替換為11但接下來還必須檢查在此過程中是否有其它錯誤。

但實際上，當(dāng)我們對這個過程進(jìn)行形式化后，只用了幾天時間就把12改為11，我們只是在某個地方將12改為11，然后Lean在大約五個地方報錯。

目前實際上有不少大型證明形式化項目正在進(jìn)行中，也許最大的是Kevin Buzzard的項目，他剛剛獲得了一筆巨額資金用于將費馬大定理在Lean中形式化。

他說這個項目最重要的部分將需要五年時間來完成，但他沒有聲稱五年內(nèi)能完成全部，很有趣。

所以這是形式化證明助手的一個應(yīng)用。

機器學(xué)習(xí)

接下來我將談?wù)剻C器學(xué)習(xí)。

機器學(xué)習(xí)使用神經(jīng)網(wǎng)絡(luò)來預(yù)測各種問題的答案，這些答案可以在許多領(lǐng)域中使用。不過，我將跳過我最初討論的使用神經(jīng)網(wǎng)絡(luò)猜測偏微分方程解的方法。

我想談?wù)剻C器學(xué)習(xí)在結(jié)理論中的應(yīng)用。

結(jié)理論是數(shù)學(xué)中一個相當(dāng)有趣的領(lǐng)域，它匯集了許多不同的數(shù)學(xué)分支。

結(jié)就是空間中閉合的一圈繩索或曲線。如果有辦法可以連續(xù)地將一個結(jié)變形為另一個結(jié)，并且在這個過程中繩索不允許自我交叉，那么這兩個結(jié)就被認(rèn)為是等價的。

△圖源維基百科

因此，結(jié)理論中的基本問題是：兩個結(jié)何時是等價的？兩個結(jié)，是否有辦法將一個轉(zhuǎn)變?yōu)榱硪粋€？

通常解決這個問題的方法是開發(fā)所謂的結(jié)不變量。

這些可以是各種數(shù)值，有時也包括多項式，你可以將這些數(shù)值或多項式附加到一個結(jié)上，無論你如何連續(xù)變形結(jié)，這些數(shù)值都不會改變。因此，如果兩個結(jié)具有不同的不變量，它們就不能被認(rèn)為是等價的。

存在許多類型的結(jié)不變量。有一種稱為簽名的不變量，你可以平展結(jié)并計算交叉點無論交叉是向上還是向下，并據(jù)此創(chuàng)建一個特定的矩陣等。

有一些著名的多項式，如瓊斯多項式、亞歷山大多項式，這些與許多數(shù)學(xué)領(lǐng)域有關(guān)。

還有一種是所謂的雙曲不變量，來自幾何學(xué)。

你可以取結(jié)的補空間，這通常被稱為雙曲空間，它具有一定的幾何結(jié)構(gòu)，有距離概念，你可以保留它的體積和其它一些不變量。因此，這些不變量是實數(shù)或復(fù)數(shù)，每個結(jié)都帶有一些組合不變量，如簽名、雙曲幾何不變量等。

這里有一系列帶有各種雙曲變量的結(jié)，有些被稱為雙曲體積等。

盡管已知存在兩種不同的方法來生成關(guān)于結(jié)的統(tǒng)計數(shù)據(jù)，但之前沒有人能發(fā)現(xiàn)這兩種方法之間有任何聯(lián)系或共同點。

直到最近，人們開始使用機器學(xué)習(xí)來解決這個問題。

他們創(chuàng)建了包含數(shù)百萬個結(jié)的數(shù)據(jù)庫，然后在這個數(shù)據(jù)庫上訓(xùn)練了一個神經(jīng)網(wǎng)絡(luò)。結(jié)果發(fā)現(xiàn)，訓(xùn)練后的神經(jīng)網(wǎng)絡(luò)能夠利用所有的雙曲幾何不變量，并且在大約90%的情況下能正確預(yù)測簽名。

因此，他們創(chuàng)建了這個黑盒子，它能告訴你簽名以某種方式隱藏在這些幾何變量中，但它并不告訴你這是如何做到的。這仍然很有用，因為一旦你有了這個黑盒子，你就可以隨意操作它。

接下來他們進(jìn)行的實際上是一種非常簡單顯著性分析。這個黑盒子接收大約20種不同的輸入，其中一種是你的變量類型，并輸出一個結(jié)果，即簽名。

在他們發(fā)現(xiàn)20個輸入中，只有三個實際上在輸出中起了重要作用，包括縱向平移以及子午線平移的實部和復(fù)部。

一旦他們確定了哪些變量最重要，他們可以直接將簽名與這三個特定輸入進(jìn)行比較，然后人類判斷來確定。

通過觀察這些圖表，他們提出了一個猜想，結(jié)果是錯誤的，他們實際上又使用神經(jīng)網(wǎng)絡(luò)來證明它是錯誤的。

通過失敗，他們又提出了一個修正版本，是一個解釋了這一現(xiàn)象的正確命題。因此，他們擁有了一個理論解釋，闡述了為什么簽名與這些特定的統(tǒng)計數(shù)據(jù)如此密切相關(guān)。

我認(rèn)為這體現(xiàn)了機器學(xué)習(xí)在數(shù)學(xué)領(lǐng)域應(yīng)用的增長趨勢。它雖然不能直接解決問題，但能提供許多有價值的線索，指明數(shù)據(jù)間潛在的聯(lián)系以及研究的方向，建立這些聯(lián)系的工作仍需人類來完成。

大語言模型

最后，我們有大語言模型，這些是最引人注目的，可能也是最有新聞價值的。你知道，神經(jīng)網(wǎng)絡(luò)已經(jīng)存在了20年，語言模型大概存在了5年左右，但它們只是最近才達(dá)到了與人類相似的輸出水平。

你們可能都聽說過GPT-4。GPT-4發(fā)布時，有一篇非常著名的論文描述了它的能力，并且它確實匹配這些能力。

這是一個來自2022年IMO的稍微簡化版本的問題，對于這個特定的問題，系統(tǒng)給出了一個完整且正確的解決方案。

但這是一個精選的例子，他們測試了數(shù)百個IMO級別的問題，成功率大約是1%。所以他們能夠解決特定的問題，且必須以正確的方式格式化問題才行。盡管如此，這仍然非常了不起。

另一方面，這些工具的有趣之處在于，人類覺得困難的事情，AI有時可以很容易地做到，但人類覺得容易的事情，AI經(jīng)常會表現(xiàn)很糟糕，這是一種非常正交的解決問題的方式。

在另一篇論文中，他們要求模型做一個基本的算術(shù)計算“7×4+8×8”，模型的答案是120，但當(dāng)它逐步解釋時，又得出了答案是92。這說明，雖然AI在某些情況下能找到正確答案，但處理過程并不總是準(zhǔn)確無誤。

因此，人們正在嘗試各種方法，將這些模型與更可靠的軟件連接，不需要自己做計算，可將計算任務(wù)交給Python。

你還可以強制模型只產(chǎn)生正確的答案，只在一種證明助手語言中輸出，如果它無法編譯，你就將其退回給AI，AI必須重新嘗試?；蛘吣憧梢灾苯咏趟鯥MO題的技巧，比如嘗試簡單的例子，矛盾證明等。

所以人們正在嘗試各種方法，雖然還沒有能力解決大多數(shù)數(shù)學(xué)問題，更不用說數(shù)學(xué)研究問題，但目前正在取得進(jìn)展。

除了直接解決問題外，它們還可以作為靈感來源，我自己也使用過這些模型，嘗試過各種問題。

有一個問題，GPT-4給我推薦了10種方法，其中5種我已經(jīng)嘗試過明顯無效，但有一種之前我沒注意到的技術(shù)是生成特定問題的函數(shù)，我意識到這是正確的方法。所以，它在某種程度上是有用的，現(xiàn)在還不完美，但也不是完全無用。

還有另一種AI輔助實際上對證明助手非常有用。

正如我所說，編寫形式化證明是一項非常繁瑣的任務(wù)。這就像計算機語言一樣，你必須準(zhǔn)確無誤地編寫語法，如果漏掉一個步驟，它就無法編譯。

我使用了一個叫做GitHub Copilot的工具，你可以寫下一半的證明，它會嘗試猜測下一行是什么。大約20%的猜測是接近正確的，然后你可以接受它并繼續(xù)。

在這個例子中，我試圖證明這里的命題，灰色行是Copilot建議的內(nèi)容。結(jié)果顯示第一行是無用的，但第二行有用。因此，你不能僅僅接受輸入，因為它不一定能編譯通過。

但是，如果你已經(jīng)大致了解代碼的工作原理，這將為你節(jié)省大量時間。

現(xiàn)在還有實驗在嘗試讓AI提出一個證明方案，然后你將其反饋給編譯器，如果編譯錯誤，你就將錯誤信息反饋回去。

我們已經(jīng)開始嘗試證明那些四五行長的內(nèi)容，可以通過這種方法進(jìn)行約束。當(dāng)然，像數(shù)千行的大型證明還遠(yuǎn)遠(yuǎn)不能立即形式化，但它已經(jīng)是一個有用的工具了。

目前機器發(fā)展處于哪一階段？

那么，我們現(xiàn)在處于什么階段呢？

有人希望在未來幾年內(nèi)我們可以使用計算機直接解決數(shù)學(xué)問題，我認(rèn)為我們距離這一目標(biāo)還很遠(yuǎn)。

對于非常狹窄的問題，你可以設(shè)置專門的AI來處理一小部分問題。但即便如此，它們也不是完全可靠的。它們可能有用，但仍然有限。

至少在未來幾年里，它們主要還是用于輔助，不只是我們熟悉的蠻力計算輔助，人們正在嘗試各種創(chuàng)新方法，希望AI能夠非常擅長生成有見地的猜測。

我認(rèn)為這是一個特別令人興奮的方向。

我們已經(jīng)看到了關(guān)于結(jié)的一個小例子，AI已經(jīng)能夠猜測兩種不同統(tǒng)計數(shù)據(jù)之間的聯(lián)系。因此，你只需創(chuàng)建這些龐大的數(shù)據(jù)集并將它們輸入到AI中，它們就會自動生成不同數(shù)學(xué)對象之間的許多有價值的聯(lián)系。

我們還沒有真正知道如何做到這一點，部分是因為我們沒有這些大型數(shù)據(jù)集，但我認(rèn)為這最終是可能做到的。

證明定理是一個痛苦且費時的過程，我們通常一次只能證明一個定理，或者如果效率高的話，可能是兩個或三個。但是借助AI，你可以想象將來不僅僅是試圖解決一個問題，而是取一類1000個問題，然后對AI說：“好的，我要求你用這種技術(shù)來解決這1000個問題?！?/p>

使用這種技術(shù)，我能解決多少問題？如果我結(jié)合它們，我能做到什么？你可以開始探索問題的空間，而不是單獨解決每個問題。

這是一個需要幾十年時間，通過成百上千篇論文慢慢摸索各種技術(shù)能做什么、不能做什么的過程。

但有了這些工具，你真的可以開始以一種前所未有的規(guī)模進(jìn)行數(shù)學(xué)研究。

因此，未來將非常令人興奮。我的意思是，我們?nèi)詫⒁詡鹘y(tǒng)方式證明定理。事實上，我們必須這樣做，因為如果我們自己不知道如何操作，我們將無法指導(dǎo)這些AI。但我們將能夠做很多我們現(xiàn)在無法做到的事情。

參考鏈接：
[1]https://www.youtube.com/watch?v=e049IoFBnLA
[2]https://www.reddit.com/r/singularity/comments/1f0o9vo/terence_tao_says_ai_could_solve_mathematical/