新智元報道
編輯：Aeneas 好困
【新智元導(dǎo)讀】瘋狂入坑AI工具的數(shù)學(xué)大神陶哲軒，最近又被Lean4和Copilot震驚了它們竟然幫他發(fā)現(xiàn)了自己論文中的一處錯誤！2026年AI成為數(shù)學(xué)論文合著者的預(yù)言，已經(jīng)愈發(fā)逼近了。
最近，熱衷于用GPT-4、Copilot做研究的數(shù)學(xué)大神陶哲軒，又在AI的幫助下發(fā)現(xiàn)了自己論文中的一處隱藏bug！
陶哲軒表示，自己在用Lean4形式化第6頁論點的過程中發(fā)現(xiàn)，表達式在n=3,k=2時，實際上是發(fā)散的。
這個不太容易看出的bug能被及時捉住，多虧了Lean4。
原因是，Lean要求他構(gòu)建02。由此，Lean無法基于負的0
好在，這只是一個小bug，只存在于n值很小的情況。此時，只需修改論文中的一些常數(shù)就可以了。
一些數(shù)學(xué)愛好者粉絲在此帖中驚呼：這太驚人了，很高興看到AI證明助手的傳播，為數(shù)學(xué)研究的未來奠定了更堅實的基矗
而陶哲軒表示，這是完全有可能的事。
或許在不久的將來，我們就可以在Lean之上構(gòu)建一個AI層。
只要把證明中的各步描述給AI，AI就可以利用Lean來執(zhí)行證明了，過程中還能各種調(diào)用計算機代數(shù)軟件包。
今年6月，陶哲軒就曾在GPT-4試用體驗的博客中預(yù)言
2026年，AI將與搜索和符號數(shù)學(xué)工具相結(jié)合，成為數(shù)學(xué)研究中值得信賴的合著者。
而陶哲軒也身體力行，新論文已經(jīng)開始用GPT-4寫了，并屢屢驚呼GitHub Copilot的驚人能力，讓我感到不安！
AI加持大神數(shù)學(xué)研究
最近這個月，陶哲軒是徹底「入坑」AI了。
在GPT-4的幫助下，他開始學(xué)習(xí)用Lean4寫論文、做數(shù)學(xué)研究。
這個過程無疑令他十分激動，因此隔三岔五（甚至每隔幾個小時）就會在mastodon上發(fā)帖，記錄自己的學(xué)習(xí)感悟和經(jīng)驗總結(jié)。
在寫一篇關(guān)于麥克勞林不等式研究的論文中，陶哲軒就大量用到了GPT-4、Copilot、Lean4等AI工具。
論文地址：https://arxiv.org/abs/2310.05328
現(xiàn)在的進度是，陶哲軒已經(jīng)在Lean4中完成對論文第2節(jié)論點的修復(fù)了。
只不過這個過程這比他預(yù)想的要繁瑣得多，每一行證明都要花費大約一個小時來形式化。
在項目的第一周，他的瓶頸在于不熟悉Lean語法和工具；但目前的瓶頸在于工具本身不如計算機代數(shù)軟件包中的工具先進。
例如，他在論文的一行中指出，不等式：
可以重排為：
假設(shè)所有分母都是正數(shù)，這對于人工計算來說是一項非�？焖俚娜蝿�(wù)，在任何標(biāo)準(zhǔn)的計算機代數(shù)軟件包中也能相當(dāng)容易地完成。
Lean雖然有著非常實用的自動工具來處理線性運算，但目前還沒有自動簡化涉及指數(shù)復(fù)雜表達式的工具。
因此，我們必須一步一步地處理指數(shù)定律以及上述其他運算，而這個過程非常耗時。
最后，陶哲軒決定不在這部分論證中使用漸進符號，而是建立了一個帶有確定常數(shù)C的不等式：
其中，
最開始，陶哲軒認為用諸如C=7這樣的值來證明不等式會「更簡單」。但利用現(xiàn)有工具去嚴格證明C≤7非常繁瑣，于是就放棄了這個想法，轉(zhuǎn)而使用形式上更可操作的C值�，F(xiàn)在所選的，數(shù)值大約為6.16。
對此，有好奇的網(wǎng)友問道：「與手算相比，AI在證明速度方面做得如何？」
陶哲軒表示，根據(jù)自己的觀察，那些對計算機代數(shù)軟件包和計算器來說是機械性的任務(wù)類型，對形式化證明助手來說未必是機械性的。
但隨著LLM的出現(xiàn)，我們應(yīng)該可以將所有的計算機輔助工具統(tǒng)一成一個對用戶非常友好的通用工具。而這個工具將擁有每個組件的全部優(yōu)點。
甚至，在不久的將來，我們還可以設(shè)想在Lean之上構(gòu)建一個AI層
通過「數(shù)學(xué)英語」將證明中的各個步驟描述給AI，然后AI就可以嘗試利用Lean來執(zhí)行，或許在這個過程中還能調(diào)用計算機代數(shù)軟件包。
Copilot竟能猜出后續(xù)步驟
此前，在這篇麥克勞林不等式研究的論文中，陶哲軒就驚詫地發(fā)現(xiàn)，Copilot竟然能夠預(yù)測出自己下一步想要做什么！
它不僅能正確預(yù)測出用于各種例行驗證的多行代碼，還能根據(jù)陶哲軒提供定理的名稱，推斷出他想要往哪個方向做研究。
這讓陶哲軒連連驚呼：太不可思議了！
在證明論文定理1.3的過程中，陶哲軒用Lean4完成了定理證明的形式化。
在論文中，證明過程中只有一頁紙，不過形式化證明卻使用了200行Lean4。
比如在論文中，陶哲軒只是假定在任何a>0的實數(shù)上都是凸的，并在之后調(diào)用了詹森不等式。但相關(guān)代碼卻需要差不多50行。
在這個過程中，GitHub Copilot表現(xiàn)出了種種神預(yù)測，神奇地推測出了陶哲軒的研究接下來的方向。
而Lean的重寫策略，讓他能通過有針對性的替換，來修改冗長的假設(shè)或目標(biāo)。
這個功能極為重要，它可以讓人們自由操縱這些表達式，而不必總是完整地輸入它們。
相對來說，在LaTex中，這種操作就麻煩多了。
陶哲軒表示自己需要粗略地模擬Lean4的重寫策略，通過剪切、粘貼等操作，對從一行到下一行的冗長表達式進行有針對性的編輯。這會導(dǎo)致錯別字在文檔中一連傳播多行。
而Lean4就能以自動和驗證的方式，完成這種重寫。
當(dāng)然，Lean 4目前還不是萬能的，也存在一些局限。比如重寫涉及約束變量的表達式，并不總能輕易完成。
陶哲軒表示自己很期待，什么時候很簡單地用自然語言，來要求LLM進行這樣的轉(zhuǎn)換。
入坑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ù)，這段代碼如此之巧妙，以至于陶哲軒不得不盯著它看了幾分鐘，才明白代碼背后的原理究竟是什么。
當(dāng)然，這段代碼也存在偏差它只考慮了連續(xù)整數(shù)的子序列，而不是任意子序列。
不過，這已經(jīng)足夠接近了，用ChatGPT生成的這段初始代碼作為起點，陶哲軒最終手動生成了自己想要的代碼，這大概節(jié)省了他半個小時的工作量。
由于ChatGPT給出的結(jié)果非常好，陶哲軒表示，自己以后還會經(jīng)常使用它，為類似的計算提供初始代碼。
很快，陶哲軒又發(fā)帖表示，自己已經(jīng)在網(wǎng)友的推薦下入坑GitHub Copilot了！
不出所料，Copilot隨后的表現(xiàn)著實讓他喜出望外只給了開頭一段外加一句話，AI就推薦了和自己的構(gòu)想非常接近的內(nèi)容。
陶哲軒只需對這些建議稍作修改，就可以用不到原計劃一半的時間完成了。
時間來到10月，陶哲軒在進行自然數(shù)游戲研究時發(fā)現(xiàn)，雖然GPT-4不能為游戲提供直接的幫助，但當(dāng)他開始使用Lean時，GPT-4就變得非常有用了。
隨著關(guān)卡變得越來越難，GPT的作用開始逐漸顯現(xiàn)出來。
在Z顯而易見是X和Y的結(jié)果的情況下，向GPT提問「如果我已經(jīng)知道X和Y，該如何證明Z呢」，就可以解決過程中各種微妙的語法問題。
除了專業(yè)相關(guān)的內(nèi)容，陶哲軒在發(fā)現(xiàn)自己可以用DALLE 3之后，就立刻玩了起來。
網(wǎng)友：LLM能讓優(yōu)秀的人再優(yōu)秀10000倍
大神在數(shù)學(xué)研究中如此癡迷AI工具，也引起了網(wǎng)友們的熱議。
有人表示 ，大神是在本月初在GPT-4幫助下開始學(xué)習(xí)Lean4的，不時就會在mastodon上隨手記錄下自己的學(xué)習(xí)進展。
這也說明，對于最成功的人，LLM都能加速他們的工作。
有人表示，即使不會寫代碼的人，只要是一個優(yōu)秀的LLM溝通者，都能快速實現(xiàn)功能的自動化。
不過，如果只有高技能人才才能有效利用LLM的話，結(jié)果就是可能會加劇人與人之間的不平等。
馬上有人現(xiàn)身說法表示，是這樣的，自己的朋友此前除了Excel公式外不會寫任何東西，但現(xiàn)在，他已經(jīng)能用GPT-4編寫Python應(yīng)用程序了！
而自己作為擁有30年開發(fā)經(jīng)驗的碼農(nóng)，還需要懇求他教一教自己這項技術(shù)。
他的成功，大概就是因為他很會和LLM溝通。
有人預(yù)言，隨著時間的推移，使用LLM的人會獲得壓倒性的好處，無論本身智力如何，他們都將在梯子上越爬越高，成為考試專家。
對于精英來說，他們或許會從LLM那里得到100倍的助力，而對于頂級工程師，這種助力大概能有10000倍。
