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

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

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

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

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

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

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

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

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

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

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

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

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

AI加持大神數學研究

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

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

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

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

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

現在的進度是，陶哲軒已經在Lean4中完成對論文第2節論點的修復了。

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

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

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

可以重排為：

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

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

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

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

其中，

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

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

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

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

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

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

Copilot竟能猜出后續步驟

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

很快，陶哲軒又發帖表示，自己已經在網友的推薦下入坑GitHub Copilot了！

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

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

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

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

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

除了專業相關的內容，陶哲軒在發現自己可以用DALL·E 3之后，就立刻玩了起來。

網友：LLM能讓優秀的人再優秀10000倍

大神在數學研究中如此癡迷AI工具，也引起了網友們的熱議。

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

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

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

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

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

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

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

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

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