在探索「數(shù)學(xué)之美」的路上，人工智能到底走到哪一步了？說(shuō)到這個(gè)話題，可能沒(méi)人比數(shù)學(xué)家陶哲軒更懂。他幾乎是最常用 AI 輔助證明的數(shù)學(xué)家之一，還在今年的 AI 數(shù)學(xué)奧林匹克競(jìng)賽（AIMO 進(jìn)步獎(jiǎng)）擔(dān)任了顧問(wèn)委員。

最近，在 IMO 2024 的一場(chǎng)演講中，陶哲軒全面回顧和展望了計(jì)算機(jī)與人工智能在數(shù)學(xué)研究中應(yīng)用范式的演變。

視頻鏈接：https://www.youtube.com/watch?v=e049IoFBnLA

為期一個(gè)小時(shí)的演講中，他從早期計(jì)算工具討論到現(xiàn)代機(jī)器學(xué)習(xí)和形式化證明助手的演變過(guò)程，還著重介紹了最近取得的突破和面臨的挑戰(zhàn)。陶哲軒強(qiáng)調(diào)，雖然人工智能在數(shù)學(xué)領(lǐng)域的作用越來(lái)越大，但人類的洞察力和創(chuàng)造力對(duì)于在該領(lǐng)域取得有意義的進(jìn)展仍然至關(guān)重要。

以下是陶哲軒演講全文：

謝謝！回到 IMO 我很開(kāi)心，在 IMO 的那段時(shí)間是我一生中最快樂(lè)的時(shí)光之一?，F(xiàn)在回想起來(lái)，仍然覺(jué)得很美好。我希望大家都能玩得開(kāi)心，無(wú)論你是否取得了好成績(jī)，不僅僅是在比賽中，在社交活動(dòng)中也是如此。

我的演講主題是人工智能，更廣泛地說(shuō)，是如何用計(jì)算機(jī)輔助數(shù)學(xué)。你們都聽(tīng)說(shuō)過(guò)人工智能以及它如何改變一切。今年早些時(shí)候，DeepMind 發(fā)布了一款新產(chǎn)品 AlphaGeometry。因此，這場(chǎng)演講我將更多地討論這些工具如何開(kāi)始改變數(shù)學(xué)研究。

數(shù)學(xué)研究不同于數(shù)學(xué)競(jìng)賽，解決一個(gè)問(wèn)題不止需要 3 個(gè)小時(shí)，而是需要幾個(gè)月。有時(shí)，你解決不了問(wèn)題，就必須改變問(wèn)題。雖然在技巧上有一些重疊，但這與數(shù)學(xué)競(jìng)賽絕對(duì)不同。因此，AI 的加入太令人興奮了，而且具備變革性。

但另一方面，這也是一種連續(xù)性。我們使用計(jì)算機(jī)和機(jī)器進(jìn)行數(shù)學(xué)運(yùn)算已經(jīng)有很長(zhǎng)一段時(shí)間了。即使做數(shù)學(xué)的方式和性質(zhì)正在發(fā)生變化，但我們實(shí)際上是沿襲了機(jī)器輔助的悠久傳統(tǒng)。

那么，有個(gè)問(wèn)題：我們使用機(jī)器進(jìn)行數(shù)學(xué)運(yùn)算有多久了？

答案是數(shù)千年。這是羅馬人用來(lái)做數(shù)學(xué)運(yùn)算的機(jī)器，它不是很靈巧。

計(jì)算機(jī)呢？我們用計(jì)算機(jī)做數(shù)學(xué)題有多久了？大約有 300 到 400 年。有點(diǎn)奇怪吧，因?yàn)楝F(xiàn)代計(jì)算機(jī)直到 20 世紀(jì) 30 年代和 40 年代才出現(xiàn)。在此之前，計(jì)算機(jī)并不是電子的，而是機(jī)械的，再之前，它們是「人類」?！赣?jì)算機(jī)」實(shí)際上是一種職業(yè)，是「計(jì)算的人」。

這是世界大戰(zhàn)期間的「計(jì)算機(jī)集群」，用來(lái)計(jì)算彈道等等。這些計(jì)算機(jī)通常都是女孩，因?yàn)槟腥藗兊墓ぷ魇谴蛘獭＿€有一些程序員，他們負(fù)責(zé)告訴女孩們?cè)撟鍪裁?。那時(shí)計(jì)算能力的基本單位和 CPU 無(wú)關(guān)。

所以，一千個(gè)女孩這樣工作一小時(shí)，能完成多少計(jì)算量？

正如我所說(shuō)，我們使用計(jì)算機(jī)的歷史可以追溯到 18 世紀(jì)甚至更早。在那個(gè)時(shí)代，計(jì)算機(jī)最基本的用途就是建立表格。我上高中時(shí)還在課程中學(xué)習(xí)如何使用這些已被淘汰的表格。

當(dāng)然，現(xiàn)在我們有了計(jì)算器和電腦?，F(xiàn)在我們?nèi)匀皇褂帽砀?。在?shù)學(xué)研究中，我們依賴表格，即使現(xiàn)在叫它們數(shù)據(jù)庫(kù)，但本質(zhì)上是一個(gè)東西。

數(shù)學(xué)領(lǐng)域的許多重要成果都是通過(guò)數(shù)論中的表格首次發(fā)現(xiàn)的。數(shù)論中最基本的成果之一叫做素?cái)?shù)理論。Legendre 和 Gauss 發(fā)現(xiàn)了它，雖然無(wú)法證明這一點(diǎn)，但他們推測(cè)這是真的。

在數(shù)論中有一個(gè)非常核心的問(wèn)題，叫做伯金 - 斯旺頓模猜想（（Birch and Swinnerton-Dyer），我想在這里談?wù)劇?/span>

這個(gè)猜想也是通過(guò)大量的表格發(fā)現(xiàn)的?，F(xiàn)在，包括我在內(nèi)的很多數(shù)學(xué)家都在使用一個(gè)表格，叫做「整數(shù)序列在線百科全書(shū)」（Online Encyclopedia of Integar Sequences，OEIS）。也許你也會(huì)遇到它，你可能會(huì)認(rèn)出很多整數(shù)序列。

比如我告訴你 1,1,2,3,5,8,13 這個(gè)序列，OEIS 就是一個(gè)包含數(shù)十萬(wàn)個(gè)類似序列的數(shù)據(jù)庫(kù)。

很多時(shí)候，數(shù)學(xué)家在研究一個(gè)問(wèn)題時(shí)，都會(huì)涉及到一些數(shù)字的自然序列。例如，也許有一個(gè)取決于 n 的空間序列，你可以計(jì)算出這些數(shù)字中的前五六個(gè)或前十個(gè)，然后將其放入 OEIS 中進(jìn)行比較。

如果你運(yùn)氣好的話，這個(gè)序列已經(jīng)被別人放在那里了。它可能來(lái)自于一個(gè)完全不同的來(lái)源，比如是對(duì)其他數(shù)學(xué)問(wèn)題的研究。這就給了你一個(gè)很大的線索 —— 兩個(gè)問(wèn)題之間存在著聯(lián)系，許多研究都是這樣產(chǎn)生的。

表格就是我們最早使用計(jì)算機(jī)的方法之一。當(dāng)你想到用計(jì)算機(jī)來(lái)做數(shù)學(xué)題時(shí)，你會(huì)想到數(shù)值運(yùn)算，它是可持續(xù)計(jì)算的正式名稱。你想要做一個(gè)非常龐大的計(jì)算，就需要做很多很多的算術(shù)運(yùn)算。

把它輸出給計(jì)算機(jī)，我們從上世紀(jì) 20 年代就開(kāi)始做了。也許第一個(gè)真正進(jìn)行科學(xué)計(jì)算的人是 Hendrick Lorentz。他的任務(wù)是建一個(gè)巨大的像辦公室一樣的東西，他們想知道水流的內(nèi)部是怎么回事，所以他們必須建立一些流體方程模型。

他用了一大堆人類計(jì)算機(jī)來(lái)解決這個(gè)問(wèn)題，且不得不發(fā)明了浮點(diǎn)運(yùn)算來(lái)完成這項(xiàng)工作。他意識(shí)到，想讓很多人快速完成大量計(jì)算，應(yīng)該用浮點(diǎn)來(lái)表示大量不同大小的數(shù)字。

當(dāng)然，我們現(xiàn)在用計(jì)算機(jī)來(lái)建模各種事物，比如解決大量線性方程或偏微分方程，做一些商業(yè)計(jì)算。它還可以解決代數(shù)問(wèn)題，許多幾何題原則上也都可以通過(guò)科學(xué)計(jì)算來(lái)解決。

不幸的是，一旦它的計(jì)算規(guī)模增加，其復(fù)雜性就會(huì)變成指數(shù)級(jí)。因此，直到最近，用計(jì)算機(jī)代數(shù)軟件蠻力解決這些問(wèn)題還不太可行。但現(xiàn)在有了人工智能系統(tǒng)，這件事也許就更有希望了。

另一種已變得相當(dāng)強(qiáng)大的科學(xué)計(jì)算是所謂的 SAT 求解器。它們基本上可以解決邏輯難題。比如，如果你有 10 個(gè)陳述或者 1000 個(gè)陳述都是真的或假的，而你知道，如果第 3 個(gè)陳述是真的，第 6 個(gè)陳述是真的，那么第 7 個(gè)陳述一定是假的。如果給你一大堆這樣的限制條件，SAT 求解器就會(huì)嘗試接受所有這些信息，然后總結(jié)：你能證明這些句子的某種組合嗎？

SAT 求解器還有一個(gè)更花哨的版本，叫做 SMT 求解器。在這里，你還會(huì)有一些變量 x、y 和 z，你還會(huì)假設(shè)一些法則。但不幸的是，它們的規(guī)模也非常大，根本無(wú)法很好地?cái)U(kuò)展。同樣，解決這些問(wèn)題的時(shí)間和復(fù)雜度也會(huì)呈指數(shù)級(jí)增長(zhǎng)。一旦超過(guò) 1000 個(gè)左右的命題，就很難在任何合理的時(shí)間內(nèi)運(yùn)行這些。

但它們實(shí)際上可以解決一些問(wèn)題。比如最近的一個(gè)成功案例，如圖所示，可能只有計(jì)算機(jī)才能解決，我認(rèn)為只憑一個(gè)人根本解出不來(lái)。

這就是所謂的畢達(dá)哥拉斯三元組問(wèn)題，在大型計(jì)算機(jī)服務(wù)器計(jì)算之前，這個(gè)問(wèn)題一直沒(méi)有解決。

問(wèn)題是，你把自然數(shù)染成兩種顏色：紅色或藍(lán)色，但無(wú)論你如何給這兩個(gè)自然數(shù)著色，其中一種顏色都必須包含一個(gè)畢達(dá)哥拉斯三元組 A、B、C 三個(gè)數(shù)。

現(xiàn)在我們知道了，事實(shí)上并不需要窮舉，只需要查到 7824。

這個(gè)證明需要 7 個(gè) CPU-year 計(jì)算。他們生成了 200 兆字節(jié)，后來(lái)被壓縮到 68 千兆字節(jié)。這就是我們利用計(jì)算機(jī)進(jìn)行大量案例分析的一種方式。

但近年來(lái)，我們開(kāi)始用更有創(chuàng)意的方式使用計(jì)算機(jī)。因此，有三種方式可以利用計(jì)算機(jī)進(jìn)行數(shù)學(xué)運(yùn)算。我覺(jué)得我真的很興奮，尤其是當(dāng)它們相互結(jié)合，并與更經(jīng)典的數(shù)據(jù)庫(kù) —— 表格和符號(hào)計(jì)算，這種科學(xué)計(jì)算結(jié)合在一起的時(shí)候。

首先，我們利用機(jī)器學(xué)習(xí)和較新的網(wǎng)絡(luò)來(lái)發(fā)現(xiàn)新的聯(lián)系，并找出不同類型數(shù)學(xué)之間的關(guān)聯(lián)方式，而這些方式是人類無(wú)法看到或不太可能看到的。

尤其是大型語(yǔ)言模型，某種意義上說(shuō)，它是機(jī)器學(xué)習(xí)的大型版本，是一種可以使用自然語(yǔ)言的算法，比如 ChatGPT 等。它們可以生成可能的證明、解決問(wèn)題的方法，這些方法有時(shí)有效，有時(shí)無(wú)效。在我之后的演講中，你會(huì)看到更多這樣的例子。

不過(guò)，還有另一種技術(shù)剛剛被日常數(shù)學(xué)家所使用，這就是所謂的形式化證明輔助。計(jì)算機(jī)語(yǔ)言是用來(lái)編寫(xiě)可執(zhí)行代碼的，而形式化輔助證明則是用來(lái)檢查事物的語(yǔ)言，用來(lái)檢查某個(gè)論證是否真實(shí)，是否能從數(shù)據(jù)中得出結(jié)論。

這些語(yǔ)言使用起來(lái)相當(dāng)煩人，而現(xiàn)在它們變得越來(lái)越容易上手了。它們促進(jìn)了許多有趣的數(shù)學(xué)項(xiàng)目，如果沒(méi)有這些證明輔助工具，這些項(xiàng)目是不可能完成的，而且它們將來(lái)會(huì)與我在這里介紹的其他工具結(jié)合得非常好。

所以，我想談?wù)勈褂脵C(jī)器和計(jì)算機(jī)輔助數(shù)學(xué)研究的新成果。從證明輔助開(kāi)始吧。是的，歷史上第一個(gè)真正意義上的計(jì)算機(jī)輔助證明可能是四色定理的證明，即「任何一張地圖，只用四種顏色，就能讓相鄰的國(guó)家染上不同的顏色」。

1976 年那時(shí)，還沒(méi)有輔助證明。實(shí)際上，當(dāng)時(shí)做的尚不能稱之為計(jì)算機(jī)證明。如今，這是一個(gè)需要大量計(jì)算的證明，其中一半由計(jì)算機(jī)完成，一半由人類完成。

他們證明四色定理的方法是：你基本上可以歸納出國(guó)家的數(shù)量，并證明如果你有一個(gè)龐大的地圖，其中有一些國(guó)家的子圖，那么就會(huì)產(chǎn)生一個(gè)大約有 1000 到 2000 個(gè)特殊子圖的列表。

其中有一些工作他們可以通過(guò)計(jì)算機(jī)完成，但也不得不手工將每張圖表輸入程序并進(jìn)行檢查。這項(xiàng)任務(wù)實(shí)際上是由人工計(jì)算機(jī)完成的，其中一位作者的女兒不得不花上幾個(gè)小時(shí)手動(dòng)檢查。工作非常繁瑣，而且過(guò)程并不完美。有很多小錯(cuò)誤，他們不得不更新表格。因此，這并不是現(xiàn)代計(jì)算機(jī)證明的標(biāo)準(zhǔn)，計(jì)算機(jī)可驗(yàn)證的證明是在九十年代才出現(xiàn)的，當(dāng)時(shí)只用了 700 多個(gè)圖就得到了一個(gè)更簡(jiǎn)單的證明。

但現(xiàn)在，所有需要檢查的東西，都可以通過(guò)一種非常精確的方式找到屬性列表。你可以用你喜歡的計(jì)算機(jī)語(yǔ)言（C 或 Python 或其他語(yǔ)言）編寫(xiě)代碼，用幾頁(yè)紙和幾百行代碼就能檢查出來(lái)，幾分鐘就能搞定。然后再實(shí)際檢查它是否完全正確，并提供一個(gè)一直到數(shù)學(xué)公理的證明。

從證明首次出現(xiàn)，到我們可以用計(jì)算機(jī)完全驗(yàn)證，這中間有一個(gè)巨大的鴻溝。

另一個(gè)有名的例子是開(kāi)普勒猜想。說(shuō)起來(lái)非常簡(jiǎn)單。即如何在三維空間中最有效地堆疊球體，以最大限度地填充空間。如下展示了一種「三角形」的堆積方式，它看起來(lái)就像水果店里堆著的橘子一樣。還有一種對(duì)偶的立方堆積方式。兩種堆積方式的密度是相同的，都約為 74%。

問(wèn)題是，開(kāi)普勒猜想，這個(gè)難題困擾了數(shù)學(xué)家?guī)讉€(gè)世紀(jì)。二維空間的最佳堆積并不難證明。但拓展到 24 維度，我們直到最近才得出答案，烏克蘭女?dāng)?shù)學(xué)家 Viazovska 最近解決了這個(gè)問(wèn)題。

有一種證明開(kāi)普勒猜想的策略，雖然堆疊的球的數(shù)量是無(wú)限的，但我們可以先試著把它簡(jiǎn)化成一個(gè)有限的問(wèn)題，用電腦來(lái)處理。

匈牙利數(shù)學(xué)家 Tóth 在 50 年代提出了一個(gè)重要的想法，即將開(kāi)普勒猜想的證明轉(zhuǎn)化為一個(gè)有限的組合問(wèn)題。每次堆積時(shí)，空間會(huì)被細(xì)分成一些稱為「沃羅諾伊區(qū)域」的多面體。這些區(qū)域是通過(guò)找出哪些點(diǎn)更接近某個(gè)球體而不是其他球體來(lái)確定的。

可以通過(guò)計(jì)算「沃羅諾伊區(qū)域」的體積等屬性，進(jìn)一步得知球體在空間中的排列密度。因此，如果你能算出這些多面體的體積在平均上如何變化，那么就可以估算堆積密度的最大值。你還可以嘗試找出這些多面體之間的關(guān)系，比如，如果一個(gè)多面體非常大，可能會(huì)導(dǎo)致附近的多面體非常小。

因此，你可以試著找到一些不等式，基于這些不等式，進(jìn)行線性規(guī)劃等數(shù)學(xué)運(yùn)算，最后得出了一個(gè)正確的值。然而，盡管許多人嘗試了這種方法，有些甚至聲稱成功了，但沒(méi)有一個(gè)被公認(rèn)為是正式的證明。

這個(gè)問(wèn)題最終首先由 Thomas Hales 和他的合作伙伴 Ferguson 解決了。他基本上采用了與前人相同的策略，但在技術(shù)層面做了很多調(diào)整，比如他沒(méi)有直接計(jì)算多面體體積，而是發(fā)明了一種評(píng)分系統(tǒng)，通過(guò)對(duì)每個(gè)單元進(jìn)行科學(xué)評(píng)分來(lái)優(yōu)化計(jì)算。

這些評(píng)分基于體積并進(jìn)行了微調(diào)，目標(biāo)是通過(guò)線性不等式約束不同單元的得分，最終計(jì)算出密度的最大值，從而得出開(kāi)普勒猜想在三維中的答案。

這種方法非常靈活，但也因?yàn)檫^(guò)于靈活，導(dǎo)致有太多變量，比如設(shè)置評(píng)分的方法等。這也把問(wèn)題搞得更復(fù)雜了。

Hales 和 Ferguson 意識(shí)到，一旦計(jì)算函數(shù)的最小值時(shí)出了問(wèn)題，就得改變得分函數(shù)，從頭再來(lái)。但這樣一來(lái)，所有已經(jīng)檢查過(guò)的工作都得重做。于是，評(píng)分系統(tǒng)變得越來(lái)越復(fù)雜。他們?cè)谶@方面的工作持續(xù)了將近十年，每改一次都需要花費(fèi)數(shù)月來(lái)調(diào)整。

Hales 在一篇文章中曾寫(xiě)道：「這種不斷調(diào)整的做法并不受同行們歡迎。每當(dāng)我在學(xué)術(shù)會(huì)議上展示自己的新成果，我總是在展示不同函數(shù)的最小值。而且更糟糕的是，新函數(shù)與我之前的論文不完全兼容，因此我不得不回去修改和補(bǔ)充早期的工作?！巩?dāng)然盡管如此，他們最終還是證明出來(lái)了開(kāi)普勒猜想在三維中的答案。

起初，他們并不打算用計(jì)算機(jī)輔助證明，但隨著項(xiàng)目越來(lái)越復(fù)雜，他們不可避免地越來(lái)越多用到計(jì)算機(jī)。按照當(dāng)時(shí)的標(biāo)準(zhǔn)，這個(gè)證明的規(guī)模極為龐大。到 1998 年，整個(gè)證明包括了 250 頁(yè)的筆記以及 3GB 的計(jì)算機(jī)程序和數(shù)據(jù)。

同時(shí)，使用計(jì)算機(jī)導(dǎo)致 Thomas Hales 的論文難以通過(guò)審查。Hales 把論文提交給了數(shù)學(xué)頂級(jí)期刊之一《數(shù)學(xué)年刊》（Annals of Mathematics），整個(gè)審稿過(guò)程持續(xù)了四年，審稿委員會(huì)包括 12 名審稿人。最終，他們表示 99% 地確定證明是正確的，但無(wú)法完全確認(rèn)其中的所有計(jì)算。出于這種不確定性，編輯們采取了非常罕見(jiàn)的做法，發(fā)表了論文，并附上了一個(gè)來(lái)自編輯的保留說(shuō)明，提醒讀者有未完全驗(yàn)證的部分。不過(guò)后來(lái)，這個(gè)保留說(shuō)明被移除了。

當(dāng)時(shí)，關(guān)于計(jì)算機(jī)輔助證明是否可以被視為真正的數(shù)學(xué)證明存在相當(dāng)大的爭(zhēng)議。即使在論文發(fā)表后，仍有一些數(shù)學(xué)家質(zhì)疑這是否真正構(gòu)成一個(gè)完整的證明。

這可能是第一個(gè)用計(jì)算機(jī)輔助數(shù)學(xué)證明的大事件。這促使數(shù)學(xué)家們開(kāi)始推動(dòng)如何將證明過(guò)程完全形式化。Thomas Hales 因此創(chuàng)建了一個(gè)項(xiàng)目 ——「Flyspeck」，基于已有的計(jì)算機(jī)語(yǔ)言，他帶領(lǐng)團(tuán)隊(duì)構(gòu)建了一種適用于數(shù)學(xué)證明的語(yǔ)言，來(lái)形式化他的開(kāi)普勒猜想證明。

起初，他估計(jì)這一過(guò)程需要 20 年，但在 21 位合作者的幫助下，他在 12 年內(nèi)完成了，并在 2014 年正式發(fā)表。如今，我們對(duì)「Flyspeck」充滿信心。即便整個(gè)過(guò)程非常艱難，在過(guò)去的幾年中，我們?nèi)栽谥饾u摸索出一種更好的工作流程來(lái)形式化證明。

彼得?朔爾策（Peter Scholze）是一位非常杰出的年輕數(shù)學(xué)家，曾獲得菲爾茲獎(jiǎng)，他因許多成就而聞名，其中之一就是他創(chuàng)造了一個(gè)極具潛力的數(shù)學(xué)領(lǐng)域，稱為「凝聚態(tài)數(shù)學(xué)（Condensed Mathematics）」。這個(gè)領(lǐng)域結(jié)合了代數(shù)、范疇論等工具，應(yīng)用于泛函分析的理論，如度量空間等。在泛函分析中，傳統(tǒng)上比較抗拒代數(shù)方法的應(yīng)用，但凝聚數(shù)學(xué)原則上可以用代數(shù)方法解決一些關(guān)于函數(shù)空間的某些問(wèn)題。

朔爾策建立了「凝聚群」和「凝聚向量空間」這一整套理論。他的主要觀點(diǎn)是，我們?cè)谘芯可n程中學(xué)習(xí)的函數(shù)空間的范疇是不正確的，或者說(shuō)并非具備最佳性質(zhì)的自然范疇。然而，這套理論中有一個(gè)非常重要的消失定理需要證明，盡管朔爾策沒(méi)有詳細(xì)解釋其中的符號(hào)和術(shù)語(yǔ)。

朔爾策的凝聚數(shù)學(xué)理論中有一個(gè)非常難的消滅定理（vanishing theorem），涉及某個(gè)范疇論群的計(jì)算。這個(gè)消失定理是他理論的基礎(chǔ)，如果無(wú)法證明該定理，那么凝聚數(shù)學(xué)的框架就無(wú)法發(fā)揮其應(yīng)有的潛力。

他在博客中寫(xiě)道：自己花了一整年時(shí)間，深陷于證明這個(gè)定理的過(guò)程中，幾乎因此而瘋狂。最終，他把推理寫(xiě)在了紙上，但沒(méi)有人敢詳細(xì)查看其中的細(xì)節(jié)。因此，他仍然對(duì)這個(gè)定理存有疑慮。他指出，如果這個(gè)凝聚數(shù)學(xué)的表述能有效應(yīng)用于泛函分析領(lǐng)域，那么它的意義將極為重要。然而，他也表示，99.9% 的確定性仍然不夠，因?yàn)檫@一工作的主題具有極其基礎(chǔ)性的作用。

他說(shuō)：「他很高興看到世界各地有許多學(xué)習(xí)小組在討論相關(guān)競(jìng)賽事件，但他們都沒(méi)有深入到這個(gè)定理的證明部分?！顾硎?，這趟數(shù)學(xué)旅程并不是很有趣。他還強(qiáng)調(diào)，這可能是他最重要的一項(xiàng)工作，因此必須確保其正確性。

他很希望將這個(gè)定理用更現(xiàn)代的語(yǔ)言進(jìn)行形式化。他使用一種叫做 Lean 的 Preface 語(yǔ)言。Lean 是近年來(lái)得到廣泛開(kāi)發(fā)的語(yǔ)言，背后有一個(gè)眾包的數(shù)學(xué)庫(kù)開(kāi)發(fā)團(tuán)隊(duì)。越深入和高級(jí)的數(shù)學(xué)領(lǐng)域證明就越顯得繁瑣，尤其是像這種高深的數(shù)學(xué)領(lǐng)域，使用 Lean 可以幫助更加簡(jiǎn)潔地形式化復(fù)雜的證明過(guò)程。

數(shù)學(xué)庫(kù)已經(jīng)發(fā)展成為一個(gè)核心資源，它已經(jīng)證明了許多中間結(jié)果。你在本科數(shù)學(xué)課程中可能會(huì)看到的一些基礎(chǔ)內(nèi)容，比如基礎(chǔ)微積分、群論或拓?fù)鋵W(xué)的基本概念等，都已經(jīng)被形式化。因此，Lean 提供了一個(gè)堅(jiān)實(shí)的基礎(chǔ)，讓你不必從數(shù)學(xué)公理重新開(kāi)始，而是從大致相當(dāng)于本科數(shù)學(xué)教育的水平出發(fā)。盡管與更高級(jí)的數(shù)學(xué)研究還有很大差距，但這一基礎(chǔ)已經(jīng)能大大幫助復(fù)雜數(shù)學(xué)問(wèn)題的形式化過(guò)程。

為了形式化這個(gè)定理，他們不得不添加許多額外的內(nèi)容，因?yàn)?Lean 的數(shù)學(xué)庫(kù)目前仍不完整。在數(shù)學(xué)的許多領(lǐng)域里，比如同調(diào)代數(shù)理論和層理論，還需要被加入到這個(gè)庫(kù)中。這些高級(jí)數(shù)學(xué)工具對(duì)于更復(fù)雜的數(shù)學(xué)證明是必要的，但 Lean 目前的庫(kù)還沒(méi)有完全覆蓋這些內(nèi)容，因此需要繼續(xù)擴(kuò)展以支持更廣泛的數(shù)學(xué)領(lǐng)域。

在 EMEA 項(xiàng)目中，僅用了 18 個(gè)月，他們就能夠能用 Lean 自動(dòng)化地證明這一定理，Lean 的證明基本上是正確的。他們還找到了一些簡(jiǎn)化方法。有些步驟用代碼實(shí)現(xiàn)起來(lái)太難，因此他們被迫尋找一些捷徑。這個(gè)項(xiàng)目帶來(lái)的是長(zhǎng)遠(yuǎn)的價(jià)值。首先，他們極大地豐富了 Lean 的數(shù)學(xué)庫(kù)，能夠處理大量的抽象代數(shù)了。那些為支持該項(xiàng)目而構(gòu)建的軟件，后續(xù)的項(xiàng)目也在用。

例如，EMEA 項(xiàng)目中衍生出了一種名為「藍(lán)圖」的工具。想象一下，要直接形式化一個(gè)長(zhǎng)達(dá) 50 頁(yè)的證明，確實(shí)很痛苦。你需要在腦海中保持整個(gè)證明的連貫性。

「藍(lán)圖」的界面

為此，我們找到了正確的工作流程：首先為這個(gè)大型證明編寫(xiě)一個(gè)「藍(lán)圖」，它將證明分解成了數(shù)百個(gè)小步驟。每個(gè)步驟都可以單獨(dú)形式化，然后將它們組合起來(lái)。你首先編寫(xiě)這個(gè)「藍(lán)圖」，你的團(tuán)隊(duì)成員可以分別處理不同部分。這種拆分還讓我們得到了一點(diǎn)啟示：如果想以人類的方式閱讀數(shù)學(xué)證明，「藍(lán)圖」是最佳選擇。

目前，人們正在致力于將這份長(zhǎng)達(dá)數(shù)萬(wàn)行的形式化證明轉(zhuǎn)換回人類可讀的形式。為此，已經(jīng)開(kāi)發(fā)了一些新工具。例如，你可以將 Lean 的格式轉(zhuǎn)換成人類可讀的形式。這里有一個(gè)拓?fù)鋯?wèn)題的例子。這里的所有文本都是計(jì)算機(jī)根據(jù)形式化證明自動(dòng)生成的，看起來(lái)和一個(gè)人類寫(xiě)出來(lái)的沒(méi)什么差別。

它同樣使用數(shù)學(xué)語(yǔ)言，但它的互動(dòng)性更強(qiáng)。你可以點(diǎn)擊任何位置，它會(huì)告訴你你當(dāng)前處于哪個(gè)位置，假設(shè)是什么，你要證明什么，變量是什么。如果某個(gè)步驟太簡(jiǎn)略，你可以展開(kāi)，它會(huì)解釋每個(gè)詞的來(lái)源。如果你愿意，還可以一直深入探索每一個(gè)細(xì)節(jié)。

我覺(jué)得這是一個(gè)很棒的想法。我相信未來(lái)的教材會(huì)以這種互動(dòng)的形式編寫(xiě)。你先對(duì)它們進(jìn)行形式化，然后就可以制作出更加互動(dòng)的教材，內(nèi)部?jī)?nèi)容也會(huì)更加靈活多樣。

受此啟發(fā)，我自己也開(kāi)始了一個(gè)形式化的項(xiàng)目。去年，我與其他幾個(gè)人一起解決了一個(gè)關(guān)于組合產(chǎn)物的問(wèn)題。

這個(gè)證明大約有 33 頁(yè)，我們?cè)谙鄬?duì)較短的時(shí)間內(nèi)完成了它的形式化，可能依然是最快形式化的研究論文。用了三周時(shí)間，團(tuán)隊(duì)有 20 人左右，利用了所有已經(jīng)開(kāi)發(fā)出來(lái)的藍(lán)圖工具完成了這一切。總的來(lái)說(shuō)，這種方法讓證明過(guò)程更加開(kāi)放和協(xié)作化。而且你還能獲得很多漂亮的可視化圖表。正如我之前提到的，第一步是把你的大定理拆解成許多小部分。我們有一個(gè)定理，稱為 PFR，接下來(lái)我們會(huì)解釋為什么。在這張圖的底部，有一個(gè)表示「宇宙」的小氣泡。

然后我們引入了所有這些其他陳述，比如說(shuō)某個(gè)證明必須依賴于之前的幾個(gè)陳述，而這些陳述又依賴于更早的陳述。因此，形成了一個(gè)依賴圖，圖中的不同顏色表示這些陳述是否已形式化。綠色的氣泡表示這個(gè)陳述已經(jīng)在你的形式化語(yǔ)言中得到了正式證明 ；藍(lán)色的氣泡表示這個(gè)陳述還沒(méi)有形式化，但已經(jīng)準(zhǔn)備好進(jìn)行形式化，因?yàn)樗卸x都已經(jīng)就位。

而白色氣泡表示，連陳述都還沒(méi)有被形式化，需要有人把陳述寫(xiě)出來(lái)。因此，這就形成了一棵任務(wù)樹(shù)。這個(gè)項(xiàng)目的妙處在于，你可以讓所有人獨(dú)立合作，處理任務(wù)圖中的不同部分。每個(gè)小氣泡對(duì)應(yīng)一個(gè)陳述，而你不需要理解整個(gè)證明，只需處理你負(fù)責(zé)的那一部分就可以了。

比如，這個(gè)問(wèn)題是一個(gè)常見(jiàn)選擇題，但參與的人中有概率論領(lǐng)域的專家，也有一些根本不是數(shù)學(xué)家的人。他們是計(jì)算機(jī)程序員，但非常擅長(zhǎng)解決這類小型謎題。所以每個(gè)人都挑選了一個(gè)他們覺(jué)得自己能處理的小氣泡，并完成了它。最后，我們?cè)谌軆?nèi)完成了整個(gè)項(xiàng)目，這真的是一個(gè)非常令人興奮的項(xiàng)目。

在數(shù)學(xué)領(lǐng)域，我們通常不會(huì)與這么多人合作，通常一個(gè)團(tuán)隊(duì)最多也就五個(gè)人左右。這是由于合作大型項(xiàng)目時(shí)，團(tuán)隊(duì)中每個(gè)人的數(shù)學(xué)水平都要值得信任。需要確保他們的工作都是正確的，并且達(dá)到一定的質(zhì)量標(biāo)準(zhǔn)。但這一般不太可能。

但用 Lean 編譯器做這種項(xiàng)目，它可以自動(dòng)檢查。上傳無(wú)法編譯的內(nèi)容會(huì)被編譯器拒絕。因此，你可以與從未見(jiàn)過(guò)面的人通過(guò) Lean 合作。我在這個(gè)過(guò)程中遇到了很多人，也為在 Lean 社區(qū)遇到的伙伴寫(xiě)了不少推薦信。

Lean 的格式讓數(shù)學(xué)家們可以更好地分工合作。

擅長(zhǎng) Lean 的專家可以專注于將項(xiàng)目的一部分轉(zhuǎn)化為 Lean，不太熟悉 Lean 的數(shù)學(xué)家可以繼續(xù)原來(lái)的工作，將用 Lean 將其程式化的工作留給其他人。雖然 Lean 不能做到完全精確。如果你懂這門(mén)語(yǔ)言，AI 給出答案是可讀的，但它看起來(lái)有點(diǎn)單薄并且不太符合常規(guī)。但它可以把任務(wù)分解，有一些人可以從宏觀角度審視整個(gè)項(xiàng)目，有的人可以專注于自己擅長(zhǎng)的一小部分。我認(rèn)為這種研究方式在數(shù)學(xué)領(lǐng)域?qū)⒃絹?lái)越常見(jiàn)。

使用這些工具仍然挺痛苦的。雖然這些工具正在降低門(mén)檻，變得對(duì)用戶更友好，但我們?nèi)匀恍枰邆湟恍┚幊虒I(yè)知識(shí)，比如改格式比手算要多花 10 倍的時(shí)間。

另一方面，比如圖中的定理中有一個(gè)數(shù)字 12，在證明過(guò)程中想要把這個(gè) 12 改成 11。但是這樣必須重寫(xiě)整個(gè)證明，或者一個(gè)一個(gè)地把 12 剪切粘貼成 11。但當(dāng)我們將其程式化后，這個(gè)效率大大提高了，把 12 更改為 11 只花了幾天時(shí)間。只把某處的 12 改成了 11，編譯器自動(dòng)在五個(gè)類似的地方報(bào)錯(cuò)了。

像這類工作已經(jīng)不需要親自處理了，我們直接針對(duì)它做優(yōu)化。因此，對(duì)于一些特定的數(shù)學(xué)研究，通過(guò)程式化的方法實(shí)際比傳統(tǒng)方法更快。

目前，也有相當(dāng)多這種用計(jì)算機(jī)輔助的大型數(shù)學(xué)證明項(xiàng)目正在進(jìn)行。其中最引人矚目的應(yīng)數(shù) Kevin Buzzard 正在用 Lean 證明費(fèi)馬大定理，他剛剛獲得了一筆巨額資助。他表示，完成這項(xiàng)工作的主要工作大概需要五年時(shí)間，實(shí)際上，該項(xiàng)目已經(jīng)開(kāi)始取得進(jìn)展。

下面來(lái)談?wù)剻C(jī)器學(xué)習(xí)對(duì)數(shù)學(xué)領(lǐng)域的應(yīng)用，我先跳過(guò)用機(jī)器學(xué)習(xí)來(lái)解偏微分方程的話題，談?wù)剻C(jī)器學(xué)習(xí)的另一個(gè)應(yīng)用。數(shù)學(xué)中的「紐結(jié)理論」（Knot Theory）是一個(gè)相當(dāng)有趣的領(lǐng)域。它是眾多的數(shù)學(xué)領(lǐng)域的交匯處。

2021 年，Alex Davies 等人通過(guò)機(jī)器學(xué)習(xí)拓展了對(duì)「紐結(jié)理論」的新認(rèn)知。

從本質(zhì)來(lái)看，一個(gè)結(jié)是一個(gè)在空間中閉合的環(huán)狀或曲線。如果能夠通過(guò)連續(xù)的變形，將一個(gè)結(jié)平滑地轉(zhuǎn)換為另一個(gè)結(jié)，且在整個(gè)過(guò)程中結(jié)不穿越自身，那么這兩個(gè)結(jié)在數(shù)學(xué)上被認(rèn)為是「同胚」的。這種連續(xù)變形的過(guò)程，確保了結(jié)的拓?fù)湫再|(zhì)得以保持，也就是說(shuō)，在拓?fù)鋵W(xué)的視角下，它們的類型是等價(jià)的。

我們可以通過(guò)機(jī)器學(xué)習(xí)來(lái)自動(dòng)地識(shí)別結(jié)的性質(zhì)，并對(duì)其變化的過(guò)程進(jìn)行一些分析，例如，對(duì)不同類型的結(jié)進(jìn)行分類，或者預(yù)測(cè)結(jié)的性質(zhì)，比如它們的形態(tài)是否穩(wěn)定，或者預(yù)測(cè)它可能轉(zhuǎn)變成什么新形狀。這些知識(shí)可以擴(kuò)展到材料科學(xué)、生物學(xué)等等領(lǐng)域，從而為這些領(lǐng)域帶來(lái)新的見(jiàn)解和解決方案。

「同胚」的結(jié)

「紐結(jié)理論」中的核心問(wèn)題之一便是判斷兩個(gè)結(jié)是否具有等價(jià)性。面對(duì)兩個(gè)結(jié)，我們是否能夠找到一種方式，將一個(gè)結(jié)變換為另一個(gè)？

通常，我們通過(guò)「結(jié)不變量」來(lái)解決這個(gè)問(wèn)題。「結(jié)不變量」往往是一系列數(shù)字或多項(xiàng)式，它們與結(jié)的結(jié)構(gòu)緊密相關(guān)，并且在結(jié)的任何連續(xù)變換下都保持恒定。換言之，這些數(shù)值或多項(xiàng)式的不變性為我們提供了一種可靠的判斷標(biāo)準(zhǔn)：如果兩個(gè)結(jié)的「結(jié)不變量」不相等，那么這兩個(gè)結(jié)就不可能是等價(jià)的。這是一種判斷結(jié)等價(jià)的定量方法。

「結(jié)不變量」也有多種類型，其中一種稱為「signature」。它通過(guò)一種特定的計(jì)數(shù)方法。首先，將結(jié)展平，然后計(jì)算交叉點(diǎn)的數(shù)量，區(qū)分哪些線段是相互跨越的，哪些是相互位于下方的?；谶@些交叉點(diǎn)的信息，我們可以構(gòu)造一個(gè)特定的矩陣。通過(guò)進(jìn)一步的數(shù)學(xué)處理，我們得到一個(gè)名為「signature」的整數(shù)。

此外，還有一些著名的多項(xiàng)式也是「結(jié)不變量」，如「瓊斯多項(xiàng)式」（Jones polynomial）和「霍姆費(fèi)利多項(xiàng)式」（HOMFLY-PT polynomial）。不過(guò)，在此我就不深入討論這些內(nèi)容了。這些多項(xiàng)式、不變量為我們提供了深入理解結(jié)的復(fù)雜性和多樣性的有力工具。

此外，還有一種判斷標(biāo)準(zhǔn)，名為「雙曲不變量」（hyperbolic invariants）。它源于幾何學(xué)。你可以取結(jié)的補(bǔ)集，被稱為雙曲空間（hyperbolic space）。這種空間帶有特定的幾何結(jié)構(gòu)，具備距離的概念，并且可以度量體積和其他一些不變量，它是實(shí)數(shù)或復(fù)數(shù)，可以用來(lái)判斷兩個(gè)結(jié)是否等價(jià)。

表格中展示了 1991 年由 Hildebrand 和 J. Weeks 進(jìn)行的關(guān)于結(jié)的雙曲不變量的研究。

這里列出了一系列關(guān)于結(jié)的假設(shè)，包括雙曲體積、同調(diào)尖頂形狀等等，它們涉及實(shí)數(shù)和復(fù)數(shù)。然而，沒(méi)人知道這兩者之間有什么聯(lián)系。因此，有兩種獨(dú)立的方式來(lái)生成關(guān)于結(jié)的統(tǒng)計(jì)數(shù)據(jù)，但它們之間沒(méi)有關(guān)聯(lián)。

直到最近，人們才開(kāi)始使用機(jī)器學(xué)習(xí)來(lái)解決這個(gè)問(wèn)題。他們創(chuàng)建了數(shù)百萬(wàn)個(gè)結(jié)的數(shù)據(jù)庫(kù)，并用這些數(shù)據(jù)訓(xùn)練了一個(gè)神經(jīng)網(wǎng)絡(luò)。結(jié)果發(fā)現(xiàn)，訓(xùn)練后的神經(jīng)網(wǎng)絡(luò)，可以根據(jù)所有的雙曲幾何不變量來(lái)預(yù)測(cè)簽名，大約 90% 的時(shí)候它可以猜對(duì)。

這就形成了一個(gè)黑箱，它能夠告訴你這些幾何不變量中某處隱藏了簽名的信息，但卻不能解釋這個(gè)黑箱的內(nèi)部原理。不過(guò)這仍然有用，因?yàn)橐坏┯辛诉@個(gè)黑箱，你就可以進(jìn)行實(shí)驗(yàn)。接下來(lái)他們進(jìn)行了顯著性分析。

這種分析的原理是黑箱接收大約 20 個(gè)不同的輸入，而輸出是一個(gè)簽名那么你可以通過(guò)改變每一個(gè)輸入，來(lái)觀察輸出的變化概率。20 個(gè)輸入中只有 3 個(gè)對(duì)輸出起了重要作用，其他 17 個(gè)幾乎沒(méi)有影響，而且這 3 個(gè)也不是他們最初預(yù)期的。比如，他們本以為體積會(huì)很重要，但結(jié)果顯示體積幾乎無(wú)關(guān)緊要。三個(gè)重要的輸入是長(zhǎng)程平移和子午線平移的實(shí)數(shù)部分和復(fù)數(shù)部分。

一旦他們確定了最重要的輸入就可以直接繪制簽名與這三個(gè)輸入之間的關(guān)系圖，然后用人的視覺(jué)網(wǎng)絡(luò)，而不是神經(jīng)網(wǎng)絡(luò)來(lái)觀察其中的明顯模式。通過(guò)觀察這些圖，他們可以提出一些關(guān)于問(wèn)題的猜想。

盡管他們最初的猜想是錯(cuò)誤的，但他們重新利用神經(jīng)網(wǎng)絡(luò)，證明了這個(gè)猜想的錯(cuò)誤性，并根據(jù)錯(cuò)誤之處進(jìn)行了修正，最終得出了正確的猜想，成功解釋了這個(gè)現(xiàn)象。一旦他們得出正確的陳述，他們就能夠證明這一點(diǎn)，說(shuō)明為什么簽名與這些特定的不變量有如此密切的關(guān)系。

我認(rèn)為這展示了機(jī)器學(xué)習(xí)在數(shù)學(xué)中的一個(gè)應(yīng)用方式，它并不直接幫你解決問(wèn)題，但能提供很多有用的提示，指引你去尋找關(guān)鍵的聯(lián)系，不過(guò)最終還是需要人類來(lái)做出真正的關(guān)聯(lián)。

最后，我們來(lái)談?wù)劥笮驼Z(yǔ)言模型，它們是最引人注目、也最為人所知的。神經(jīng)網(wǎng)絡(luò)已經(jīng)存在了 20 年左右，而大型語(yǔ)言模型大約在 5 年左右就已經(jīng)出現(xiàn)了，但直到最近，它們的輸出才接近人類水平。你們可能都聽(tīng)說(shuō)過(guò) GPT-4，這是 ChatGPT 的一個(gè)模型。

非常著名的是，當(dāng) GPT-4 發(fā)布時(shí)，有一篇論文描述了它的能力。研究人員給它輸入了 2022 年國(guó)際數(shù)學(xué)奧林匹克（IMO）的一道題，是一個(gè)稍微簡(jiǎn)化的版本。如果你研究過(guò) 2022 年的 IMO 題目，你會(huì)發(fā)現(xiàn)它不是完全相同的形式，這是一個(gè)簡(jiǎn)化版本。不過(guò) GPT-4 給出了完整且正確的解答，它確實(shí)解決了一道 IMO 的題目。

但其實(shí)這是他們挑出來(lái)的。他們測(cè)試了數(shù)百道國(guó)際數(shù)學(xué)奧林匹克（IMO）級(jí)別的問(wèn)題，成功率大概只有 1%。所以雖然這道特定的問(wèn)題能夠被解決，但他們必須以正確的方式來(lái)格式化問(wèn)題才能得到解答。不過(guò)，盡管如此，這依然相當(dāng)令人驚嘆。

另一個(gè)有意思的是，某些人類覺(jué)得困難的事情，AI 可能可以輕松完成。而人類覺(jué)得容易的事情，AI 卻常常難以處理。這是一種非常不同的解決問(wèn)題方式。有研究人員曾讓模型做一個(gè)簡(jiǎn)單的算術(shù)計(jì)算，像是 7×4 + 8×8。

模型只是根據(jù)輸入猜測(cè)最可能的輸出，結(jié)果它猜的答案是 120。然后它停頓了一下，說(shuō)：「也許我應(yīng)該解釋一下為什么是 120。」于是它逐步展開(kāi)解答，但當(dāng)它一步一步進(jìn)行計(jì)算時(shí)，實(shí)際上得出了正確的答案 ——92，而不是它最初猜的 120。如果你接著問(wèn)：「等等，你之前說(shuō)答案是 120。」 它會(huì)回復(fù)：「哦，那是個(gè)筆誤，抱歉，正確答案是 92?！?/span>

所以它們并不是通過(guò)從基本原理推導(dǎo)出答案，而是每一步都在猜測(cè)接下來(lái)最自然的輸出是什么。令人驚訝的是，有時(shí)候這種方法有效，但很多時(shí)候卻不奏效。而如何讓它們變得更加準(zhǔn)確，仍然是一個(gè)正在進(jìn)行的研究課題。

所以，人們正在嘗試各種方法來(lái)改進(jìn)這些模型。你可以將這些語(yǔ)言模型與其他更可靠的軟件連接起來(lái)。實(shí)際上，接下來(lái)的演示中你會(huì)看到一個(gè)大型語(yǔ)言模型與其他工具連接的案例。在這種情況下，你不需要自己進(jìn)行計(jì)算，而是將計(jì)算外包給 Python。不過(guò)你還可以做另一件事，強(qiáng)制語(yǔ)言模型只生成正確的答案，方法是讓它們輸出特定的編程語(yǔ)言格式。如果代碼不能編譯，你就把它返回給 AI，讓 AI 重新嘗試。

或者你也可以直接教它一些解決問(wèn)題的技巧，比如我用來(lái)解決國(guó)際數(shù)學(xué)奧林匹克（IMO）問(wèn)題的技巧，像是嘗試簡(jiǎn)單例子、反證法，或者一步一步地證明等等。人們正在嘗試各種各樣的方法。雖然目前我們還遠(yuǎn)遠(yuǎn)沒(méi)有能夠解決大多數(shù)數(shù)學(xué)奧賽問(wèn)題，更別提數(shù)學(xué)研究問(wèn)題了，但我們確實(shí)在不斷取得進(jìn)展。除了能夠直接解決問(wèn)題外，AI 還可以作為某種靈感來(lái)源。

實(shí)際上，我自己也使用過(guò)這些模型，并嘗試各種問(wèn)題。我曾遇到一個(gè)難題，嘗試了幾種方法都沒(méi)有成功。于是，作為實(shí)驗(yàn)，我向 GPT 詢問(wèn)它會(huì)建議使用哪些其他技術(shù)來(lái)解決這個(gè)問(wèn)題。它給了我一個(gè)包含 10 種技術(shù)的列表，其中大概有五種是我已經(jīng)試過(guò)但明顯無(wú)用的方法，還有幾種也不太有幫助。

但其中有一種技術(shù)我沒(méi)有嘗試過(guò)，那就是對(duì)這個(gè)特定問(wèn)題使用生成函數(shù)。當(dāng)它提出這個(gè)建議時(shí)，我意識(shí)到這確實(shí)是正確的方向，但我之前忽略了。所以，作為一個(gè)可以交流的人，它還是有一定用處的。雖然現(xiàn)在并不是特別出色，但也并非完全無(wú)用。

另一個(gè)已經(jīng)變得非常有用的 AI 輔助類型是用于證明輔助的工具。正如我所說(shuō)，寫(xiě)正式的證明是一項(xiàng)非常繁瑣的任務(wù)，就像任何非常嚴(yán)苛的計(jì)算機(jī)語(yǔ)言一樣，你必須確保語(yǔ)法完全正確，如果你漏掉一步，它就無(wú)法編譯。現(xiàn)在有一些工具，比如我用過(guò)的 GitHub Copilot。

你可以寫(xiě)下證明的一半，然后它會(huì)試著猜測(cè)下一行應(yīng)該是什么。在大約 20% 的情況下，Copilot 會(huì)猜出接近正確的內(nèi)容，然后你可以選擇接受它的建議。比如，在一個(gè)實(shí)例中，我正嘗試證明某個(gè)命題，灰色部分是 Copilot 建議的代碼。結(jié)果發(fā)現(xiàn)第一行沒(méi)什么用，但第二行卻上解決了這個(gè)問(wèn)題。所以，你不能完全依賴它的輸入，因?yàn)樗灰欢芫幾g成功。但如果你大致了解代碼的工作方式，它可以為你節(jié)省很多時(shí)間。

這些工具正在不斷改進(jìn)?，F(xiàn)在，如果證明只有一兩行，它們可能能夠自動(dòng)完成。還有一些實(shí)驗(yàn)在進(jìn)行中，嘗試讓 AI 生成證明，接著將其反饋給編譯器，如果編譯出錯(cuò)，再把錯(cuò)誤信息傳回 AI。

可以看到，這種方法可以處理大約四到五行的證明。當(dāng)然，一個(gè)完整的大型證明通常有數(shù)萬(wàn)行，因此我們還遠(yuǎn)沒(méi)有達(dá)到能夠立刻將證明完全形式化的水平。但即便如此，它已經(jīng)成為一個(gè)相當(dāng)有用的工具了。

我們現(xiàn)在處于什么階段？有人希望在未來(lái)幾年內(nèi)，我們能夠直接使用計(jì)算機(jī)來(lái)解決數(shù)學(xué)問(wèn)題。我認(rèn)為距離這個(gè)目標(biāo)，還有很長(zhǎng)的路要走。對(duì)于一些細(xì)分領(lǐng)域中的問(wèn)題，我們可以構(gòu)建一個(gè) AI 專家。但它們并不完全可靠。因此，至少在接下來(lái)的幾年里，AI 將大概率扮演一個(gè)輔助的角色。

除了我們熟知的那種 AI 輔助「蠻力計(jì)算」之外，我認(rèn)為還有一個(gè)特別令人興奮的方向。盡管目前還沒(méi)有真正成功，但是 AI 已經(jīng)非常擅長(zhǎng)生成猜想。我們已經(jīng)看到了一些例子，AI 已經(jīng)可以推測(cè)兩個(gè)統(tǒng)計(jì)數(shù)據(jù)之間的聯(lián)系。所以現(xiàn)在我們寄希望于創(chuàng)建龐大的數(shù)據(jù)集，將大量數(shù)據(jù)「喂」給 AI，然后它們就會(huì)自動(dòng)生成各種數(shù)學(xué)對(duì)象間的聯(lián)系。其實(shí)這還并沒(méi)有實(shí)現(xiàn)，我們還不清楚如何做到這一點(diǎn)。當(dāng)然，我們還沒(méi)做出那種大體量的數(shù)據(jù)集。但我認(rèn)為 AI 能生成數(shù)學(xué)猜想在將來(lái)很有可能成為現(xiàn)實(shí)。

證明數(shù)學(xué)定理是一個(gè)艱難、持久的過(guò)程。我們現(xiàn)在一次只能解決一個(gè)問(wèn)題，如果效率夠高，也許你也可以同時(shí)解決兩三個(gè)問(wèn)題。但是當(dāng)我們有了 AI，可以一次性處理 1000 個(gè)類似的問(wèn)題。你可以直接告訴 AI：「嘗試用這種方法解決這 1000 個(gè)問(wèn)題」，我們?cè)贆z查結(jié)果，可能其中 35% 的問(wèn)題已經(jīng)用這種方式解決了。

此外，我能夠?qū)⑾嗨频膯?wèn)題綜合起來(lái)一并解決。這種方法允許我們對(duì)整個(gè)問(wèn)題集進(jìn)行探索，而不是孤立地逐個(gè)擊破。這是目前無(wú)法做到的，因?yàn)樗赡苄枰獛资甑臅r(shí)間，通過(guò)幾十篇論文，用各種技術(shù)慢慢弄清楚。目前，我們?nèi)匀恍枰C明老式的定理。因?yàn)槲覀冞€沒(méi)找到引導(dǎo) AI 自動(dòng)證明的方法。

但是憑借未來(lái)強(qiáng)大的 AI 能力，你將真的可以開(kāi)始以一種真正前所未有的規(guī)模進(jìn)行數(shù)學(xué)運(yùn)算，未來(lái)將會(huì)非常激動(dòng)人心。