最近，熱衷于用GPT-4、Copilot做研究的數(shù)學(xué)大神陶哲軒，又在AI的幫助下發(fā)現(xiàn)了自己論文中的一處隱藏bug！

陶哲軒表示，自己在用Lean4形式化第6頁(yè)論點(diǎn)的過(guò)程中發(fā)現(xiàn)，表達(dá)式在n=3,k=2時(shí)，實(shí)際上是發(fā)散的。

這個(gè)不太容易看出的bug能被及時(shí)捉住，多虧了Lean4。

原因是，Lean要求他構(gòu)建0<n?3，但陶哲軒只假設(shè)了n>2。由此，Lean無(wú)法基于負(fù)的0<n?3得到反證。

好在，這只是一個(gè)小bug，只存在于n值很小的情況。此時(shí)，只需修改論文中的一些常數(shù)就可以了。

一些數(shù)學(xué)愛(ài)好者粉絲在此帖中驚呼：這太驚人了，很高興看到AI證明助手的傳播，為數(shù)學(xué)研究的未來(lái)奠定了更堅(jiān)實(shí)的基礎(chǔ)。

而陶哲軒表示，這是完全有可能的事。

或許在不久的將來(lái)，我們就可以在Lean之上構(gòu)建一個(gè)AI層。

只要把證明中的各步描述給AI，AI就可以利用Lean來(lái)執(zhí)行證明了，過(guò)程中還能各種調(diào)用計(jì)算機(jī)代數(shù)軟件包。

今年6月，陶哲軒就曾在GPT-4試用體驗(yàn)的博客中預(yù)言——

2026年，AI將與搜索和符號(hào)數(shù)學(xué)工具相結(jié)合，成為數(shù)學(xué)研究中值得信賴的合著者。

這期間，不斷有人證明著這一點(diǎn)。比如加州理工、英偉達(dá)、MIT等機(jī)構(gòu)的學(xué)者，就構(gòu)建出一個(gè)基于開(kāi)源LLM的定理證明器。

而陶哲軒也身體力行，新論文已經(jīng)開(kāi)始用GPT-4寫(xiě)了，并屢屢驚呼——GitHub Copilot的驚人能力，讓我感到不安！

AI加持大神數(shù)學(xué)研究

最近這個(gè)月，陶哲軒是徹底「入坑」AI了。

在GPT-4的幫助下，他開(kāi)始學(xué)習(xí)用Lean4寫(xiě)論文、做數(shù)學(xué)研究。

這個(gè)過(guò)程無(wú)疑令他十分激動(dòng)，因此隔三岔五（甚至每隔幾個(gè)小時(shí)）就會(huì)在mastodon上發(fā)帖，記錄自己的學(xué)習(xí)感悟和經(jīng)驗(yàn)總結(jié)。

在寫(xiě)一篇關(guān)于麥克勞林不等式研究的論文中，陶哲軒就大量用到了GPT-4、Copilot、Lean4等AI工具。

論文地址：https://arxiv.org/abs/2310.05328

現(xiàn)在的進(jìn)度是，陶哲軒已經(jīng)在Lean4中完成對(duì)論文第2節(jié)論點(diǎn)的修復(fù)了。

只不過(guò)這個(gè)過(guò)程這比他預(yù)想的要繁瑣得多，每一行證明都要花費(fèi)大約一個(gè)小時(shí)來(lái)形式化。

在項(xiàng)目的第一周，他的瓶頸在于不熟悉Lean語(yǔ)法和工具；但目前的瓶頸在于工具本身——不如計(jì)算機(jī)代數(shù)軟件包中的工具先進(jìn)。

例如，他在論文的一行中指出，不等式：

可以重排為：

假設(shè)所有分母都是正數(shù)，這對(duì)于人工計(jì)算來(lái)說(shuō)是一項(xiàng)非常快速的任務(wù)，在任何標(biāo)準(zhǔn)的計(jì)算機(jī)代數(shù)軟件包中也能相當(dāng)容易地完成。

Lean雖然有著非常實(shí)用的自動(dòng)工具來(lái)處理線性運(yùn)算，但目前還沒(méi)有自動(dòng)簡(jiǎn)化涉及指數(shù)復(fù)雜表達(dá)式的工具。

因此，我們必須一步一步地處理指數(shù)定律以及上述其他運(yùn)算，而這個(gè)過(guò)程非常耗時(shí)。

最后，陶哲軒決定不在這部分論證中使用漸進(jìn)符號(hào)，而是建立了一個(gè)帶有確定常數(shù)C的不等式：

其中，

最開(kāi)始，陶哲軒認(rèn)為用諸如C=7這樣的值來(lái)證明不等式會(huì)「更簡(jiǎn)單」。但利用現(xiàn)有工具去嚴(yán)格證明C≤7非常繁瑣，于是就放棄了這個(gè)想法，轉(zhuǎn)而使用形式上更可操作的C值。現(xiàn)在所選的，數(shù)值大約為6.16。

對(duì)此，有好奇的網(wǎng)友問(wèn)道：「與手算相比，AI在證明速度方面做得如何？」

陶哲軒表示，根據(jù)自己的觀察，那些對(duì)計(jì)算機(jī)代數(shù)軟件包和計(jì)算器來(lái)說(shuō)是機(jī)械性的任務(wù)類型，對(duì)形式化證明助手來(lái)說(shuō)未必是機(jī)械性的。

但隨著LLM的出現(xiàn)，我們應(yīng)該可以將所有的計(jì)算機(jī)輔助工具統(tǒng)一成一個(gè)對(duì)用戶非常友好的通用工具。而這個(gè)工具將擁有每個(gè)組件的全部?jī)?yōu)點(diǎn)。

甚至，在不久的將來(lái)，我們還可以設(shè)想在Lean之上構(gòu)建一個(gè)AI層——

通過(guò)「數(shù)學(xué)英語(yǔ)」將證明中的各個(gè)步驟描述給AI，然后AI就可以嘗試?yán)肔ean來(lái)執(zhí)行，或許在這個(gè)過(guò)程中還能調(diào)用計(jì)算機(jī)代數(shù)軟件包。

Copilot竟能猜出后續(xù)步驟

此前，在這篇麥克勞林不等式研究的論文中，陶哲軒就驚詫地發(fā)現(xiàn)，Copilot竟然能夠預(yù)測(cè)出自己下一步想要做什么！

它不僅能正確預(yù)測(cè)出用于各種例行驗(yàn)證的多行代碼，還能根據(jù)陶哲軒提供定理的名稱，推斷出他想要往哪個(gè)方向做研究。

這讓陶哲軒連連驚呼：太不可思議了！

在證明論文定理1.3的過(guò)程中，陶哲軒用Lean4完成了定理證明的形式化。

在論文中，證明過(guò)程中只有一頁(yè)紙，不過(guò)形式化證明卻使用了200行Lean4。

比如在論文中，陶哲軒只是假定在任何a>0的實(shí)數(shù)上都是凸的，并在之后調(diào)用了詹森不等式。但相關(guān)代碼卻需要差不多50行。

在這個(gè)過(guò)程中，GitHub Copilot表現(xiàn)出了種種神預(yù)測(cè)，神奇地推測(cè)出了陶哲軒的研究接下來(lái)的方向。

而Lean的重寫(xiě)策略，讓他能通過(guò)有針對(duì)性的替換，來(lái)修改冗長(zhǎng)的假設(shè)或目標(biāo)。

這個(gè)功能極為重要，它可以讓人們自由操縱這些表達(dá)式，而不必總是完整地輸入它們。

相對(duì)來(lái)說(shuō)，在LaTex中，這種操作就麻煩多了。

陶哲軒表示自己需要粗略地模擬Lean4的重寫(xiě)策略，通過(guò)剪切、粘貼等操作，對(duì)從一行到下一行的冗長(zhǎng)表達(dá)式進(jìn)行有針對(duì)性的編輯。這會(huì)導(dǎo)致錯(cuò)別字在文檔中一連傳播多行。

而Lean4就能以自動(dòng)和驗(yàn)證的方式，完成這種重寫(xiě)。

當(dāng)然，Lean 4目前還不是萬(wàn)能的，也存在一些局限。比如重寫(xiě)涉及約束變量的表達(dá)式，并不總能輕易完成。

陶哲軒表示自己很期待，什么時(shí)候很簡(jiǎn)單地用自然語(yǔ)言，來(lái)要求LLM進(jìn)行這樣的轉(zhuǎn)換。

入坑GPT-4+GitHub Copilot，瘋狂安利

早在9月初，陶哲軒就曾發(fā)帖大贊ChatGPT生成Python代碼的效果——直接節(jié)省了半小時(shí)的工作量！

作為實(shí)驗(yàn)，他要求ChatGPT寫(xiě)一段Python代碼，為每個(gè)自然數(shù)n計(jì)算1,...,n的最長(zhǎng)子序列的長(zhǎng)度??(??) ，其中歐拉全能函數(shù)?不遞減。

例如，??(6)=5，因?yàn)?在1,2,3,4,5（或 1,2,3,4,6）上是非遞減的，但在 1,2,3,4,5,6 上不是。

有趣的是，它生成了一段極其巧妙的代碼來(lái)計(jì)算全能函數(shù)，這段代碼如此之巧妙，以至于陶哲軒不得不盯著它看了幾分鐘，才明白代碼背后的原理究竟是什么。

當(dāng)然，這段代碼也存在偏差——它只考慮了連續(xù)整數(shù)的子序列，而不是任意子序列。

不過(guò)，這已經(jīng)足夠接近了，用ChatGPT生成的這段初始代碼作為起點(diǎn)，陶哲軒最終手動(dòng)生成了自己想要的代碼，這大概節(jié)省了他半個(gè)小時(shí)的工作量。

由于ChatGPT給出的結(jié)果非常好，陶哲軒表示，自己以后還會(huì)經(jīng)常使用它，為類似的計(jì)算提供初始代碼。

很快，陶哲軒又發(fā)帖表示，自己已經(jīng)在網(wǎng)友的推薦下入坑GitHub Copilot了！

不出所料，Copilot隨后的表現(xiàn)著實(shí)讓他喜出望外——只給了開(kāi)頭一段外加一句話，AI就推薦了和自己的構(gòu)想非常接近的內(nèi)容。

陶哲軒只需對(duì)這些建議稍作修改，就可以用不到原計(jì)劃一半的時(shí)間完成了。

時(shí)間來(lái)到10月，陶哲軒在進(jìn)行自然數(shù)游戲研究時(shí)發(fā)現(xiàn)，雖然GPT-4不能為游戲提供直接的幫助，但當(dāng)他開(kāi)始使用Lean時(shí)，GPT-4就變得非常有用了。

隨著關(guān)卡變得越來(lái)越難，GPT的作用開(kāi)始逐漸顯現(xiàn)出來(lái)。

在Z顯而易見(jiàn)是X和Y的結(jié)果的情況下，向GPT提問(wèn)「如果我已經(jīng)知道X和Y，該如何證明Z呢」，就可以解決過(guò)程中各種微妙的語(yǔ)法問(wèn)題。

除了專業(yè)相關(guān)的內(nèi)容，陶哲軒在發(fā)現(xiàn)自己可以用DALL·E 3之后，就立刻玩了起來(lái)。

網(wǎng)友：LLM能讓優(yōu)秀的人再優(yōu)秀10000倍

大神在數(shù)學(xué)研究中如此癡迷AI工具，也引起了網(wǎng)友們的熱議。

有人表示 ，大神是在本月初在GPT-4幫助下開(kāi)始學(xué)習(xí)Lean4的，不時(shí)就會(huì)在mastodon上隨手記錄下自己的學(xué)習(xí)進(jìn)展。

這也說(shuō)明，對(duì)于最成功的人，LLM都能加速他們的工作。

有人表示，即使不會(huì)寫(xiě)代碼的人，只要是一個(gè)優(yōu)秀的LLM溝通者，都能快速實(shí)現(xiàn)功能的自動(dòng)化。

不過(guò)，如果只有高技能人才才能有效利用LLM的話，結(jié)果就是可能會(huì)加劇人與人之間的不平等。

馬上有人現(xiàn)身說(shuō)法表示，是這樣的，自己的朋友此前除了Excel公式外不會(huì)寫(xiě)任何東西，但現(xiàn)在，他已經(jīng)能用GPT-4編寫(xiě)Python應(yīng)用程序了！

而自己作為擁有30年開(kāi)發(fā)經(jīng)驗(yàn)的碼農(nóng)，還需要懇求他教一教自己這項(xiàng)技術(shù)。

他的成功，大概就是因?yàn)樗軙?huì)和LLM溝通。

有人預(yù)言，隨著時(shí)間的推移，使用LLM的人會(huì)獲得壓倒性的好處，無(wú)論本身智力如何，成為考試專家。

對(duì)于精英來(lái)說(shuō)，他們或許會(huì)從LLM那里得到100倍的助力，而對(duì)于頂級(jí)工程師，這種助力大概能有10000倍。