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

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

這個不太容易看出的bug能被及時捉住，多虧了Lean4。

原因是，Lean要求他構建0<n?3，但陶哲軒只假設了n>2。由此，Lean無法基于負的0<n?3得到反證。

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

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

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

或許在不久的將來，我們就可以在Lean之上構建一個AI層。

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

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

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

這期間，不斷有人證明著這一點。比如加州理工、英偉達、MIT等機構的學者，就構建出一個基于開源LLM的定理證明器。

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

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

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

在GPT-4的幫助下，他開始學習用Lean4寫論文、做數(shù)學研究。

這個過程無疑令他十分激動，因此隔三岔五（甚至每隔幾個小時）就會在mastodon上發(fā)帖，記錄自己的學習感悟和經(jīng)驗總結。

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

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

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

只不過這個過程這比他預想的要繁瑣得多，每一行證明都要花費大約一個小時來形式化。

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

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

可以重排為：

假設所有分母都是正數(shù)，這對于人工計算來說是一項非常快速的任務，在任何標準的計算機代數(shù)軟件包中也能相當容易地完成。

Lean雖然有著非常實用的自動工具來處理線性運算，但目前還沒有自動簡化涉及指數(shù)復雜表達式的工具。

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

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

其中，

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

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

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

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

甚至，在不久的將來，我們還可以設想在Lean之上構建一個AI層——

通過「數(shù)學英語」將證明中的各個步驟描述給AI，然后AI就可以嘗試利用Lean來執(zhí)行，或許在這個過程中還能調用計算機代數(shù)軟件包。

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

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

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

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

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

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

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

在這個過程中，GitHub Copilot表現(xiàn)出了種種神預測，神奇地推測出了陶哲軒的研究接下來的方向。

而Lean的重寫策略，讓他能通過有針對性的替換，來修改冗長的假設或目標。

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

相對來說，在LaTex中，這種操作就麻煩多了。

陶哲軒表示自己需要粗略地模擬Lean4的重寫策略，通過剪切、粘貼等操作，對從一行到下一行的冗長表達式進行有針對性的編輯。這會導致錯別字在文檔中一連傳播多行。

而Lean4就能以自動和驗證的方式，完成這種重寫。

當然，Lean 4目前還不是萬能的，也存在一些局限。比如重寫涉及約束變量的表達式，并不總能輕易完成。

陶哲軒表示自己很期待，什么時候很簡單地用自然語言，來要求LLM進行這樣的轉換。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

有人表示 ，大神是在本月初在GPT-4幫助下開始學習Lean4的，不時就會在mastodon上隨手記錄下自己的學習進展。

這也說明，對于最成功的人，LLM都能加速他們的工作。

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

不過，如果只有高技能人才才能有效利用LLM的話，結果就是可能會加劇人與人之間的不平等。

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

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

他的成功，大概就是因為他很會和LLM溝通。

有人預言，隨著時間的推移，使用LLM的人會獲得壓倒性的好處，無論本身智力如何，成為考試專家。

對于精英來說，他們或許會從LLM那里得到100倍的助力，而對于頂級工程師，這種助力大概能有10000倍。