文章來源：新智元
最近，熱衷於用GPT-4、Copilot做研究的數學大神陶哲軒，又在AI的幫助下發現了自己論文中的一處隱藏bug
陶哲軒表示，自己在用Lean4形式化第6頁論點的過程中發現，表達式
在n=3,k=2時，實際上是發散的。
這個不太容易看出的bug能被及時捉住，多虧了Lean4。
原因是，Lean要求他建造02。由此，Lean無法基於負的0
好在，這只是一個小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倍的助力，而對於頂尖工程師，這種助力大概可以有10,000倍。
參考資料：
https://mathstodon.xyz/@fanf42@treehouse.systems/111294362321849062
資訊來源：由0x資訊編譯自8BTC。版權所有，未經許可，不得轉載