白板在那晚的數學推導中沒派上用場。

陶哲軒盯著屏幕，Lean像刻薄裁判吐出一行行紅字。

反復拉扯后，報錯忽然安靜。

1125行Lean代碼落定——埃爾德什第613號問題的復雜反例，被逐行核查進了形式化世界。

寫手是ChatGPT，思路由陶哲軒調度，判決由機器拍板。

在一個著名的未解數學問題上，菲爾茲獎得主陶哲軒請出了ChatGPT和數學證明助手Lean，來聯手完成一項繁瑣而嚴謹的任務：形式化一個復雜的反例證明。

這個反例源自保羅·埃爾德什（Paul Erd?s）提出的第613號問題，一道困擾數學家幾十年的難題。

https://www.erdosproblems.com/forum/thread/613

早在本世紀初，就有數學家給出了一個反例證明，將這一問題「證偽」（也就是找到反例證明原猜想不成立）。

但把這個證明徹底翻譯成計算機可核查的形式卻一直沒人嘗試，因為這意味著要將所有推理細節寫成正式的邏輯代碼，工作量驚人。

而陶哲軒決定嘗鮮：讓ChatGPT先當他的「翻譯官」和「小工」，把人類的紙筆證明轉化為Lean語言的嚴謹代碼。

ChatGPT讀論文

數學黑話翻譯官上線

陶哲軒首先讓ChatGPT閱讀論文中的證明構造。

論文里的數學描述往往充滿符號和行話，但ChatGPT就像一位不知疲倦的助教，可以逐段解釋這些構造是什么意思，再嘗試用更「機械」的方式表述。

比如，論文構造了一個特殊的圖（滿足某些頂點與邊的計數條件）作為反例，ChatGPT能根據文字描述提煉出關鍵條件，甚至將它翻譯成Lean所需的定義。

它好比把晦澀的古文譯成白話，確保每一步都清晰明了。

當然，ChatGPT并非真的理解深奧的數學理念，它更多是模式匹配和概率生成。

但在這種場景下，它的確展現出驚人的「閱讀理解」能力。

陶哲軒要求它把論文中的命題用Lean語言表述出來，ChatGPT幾乎立刻就給出了正確的定義和命題陳述。

有時候，它甚至會主動「發揮」一下，比如在沒有提示的情況下就證明了一個引理的性質。

這種時刻令陶哲軒都感到驚喜，仿佛AI學生一下子開竅了。

然而興奮沒持續太久，ChatGPT很快卡在了證明的最后一步。

它能讀懂并重述大部分內容，卻在真正需要創造性跳躍的地方卡殼。

畢竟，它不是真正的數學家，只是扮演了一個熟練的翻譯加初級解題助手。

人機協作

1125行代碼橫空出世

接下來就是耐心活：一步一步引導ChatGPT編寫Lean代碼，也就是所謂「vibe coding」的過程。

所謂「vibe coding」，指的是人類不給出過于詳細的嚴苛指令，而是憑直覺和整體思路一步步讓AI搭建代碼，就像即興合奏一樣。

在這個過程中，陶哲軒更像一位樂隊指揮，提供方向和節奏，ChatGPT則即興「演奏」出代碼片段。

Lean充當嚴格的裁判，每寫一段就立刻檢查對不對，如果不對，報錯信息就是「音準」偏了，需要調整。

這一人機協作的體驗既神奇又讓人啼笑皆非。

ChatGPT有時展現出高超的「琴技」：它居然能猜出數學家想要證明的中間引理，并直接給出對應的Lean證明思路！

很多常規定義、基本引理，它張口就來，速度飛快。

這讓陶哲軒省去了大量查閱Lean庫和語法的時間，等于身邊多了個熟悉Lean語言的超級速記員。

然而，當涉及比較復雜或微妙的地方，AI就開始「跑調」了：經常寫出一長串Lean代碼卻無濟于事，不是邏輯不通就是和之前的定義對不上。Lean會毫不留情地報錯，而ChatGPT有時還一臉無辜地看不出錯在哪，需要人類耐心指正。

AI不斷繞彎子，不是遺忘前提，就是引錯定理，把簡單問題搞得撲朔迷離。

陶哲軒不得不一次次提示：「嘿，你該證明的是這個基本性質，別走遠了。」

就這樣來回拉鋸，才終于把這個「小目標」攻克。

經過將近一周的「磨煉」，ChatGPT和陶哲軒終于完成了整個反例證明的形式化。

Lean代碼整整1125行，儼然一部迷你巨著。

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_613.lean

回頭看這些代碼，作者笑稱完全是一坨「意大利面條代碼」——結構盤根錯節，充滿了AI生成的冗長繞行和中途更改的思路。

正常情況下，程序員看到這樣的代碼可能要頭疼不已；但在數學證明里，這反倒不是什么大問題。

因為Lean最終驗證通過了，就意味著每一句話、每一個推理步驟在邏輯上都是正確的。

就算代碼看起來冗繁，只要能被Lean接受，那證明就在嚴謹意義上成立了。

正如陶哲軒所說，Lean簡直是「vibe coding」的宏大舞臺。

AI鬧烏龍，人類擦屁股

誰更耗時間？

可能有人會問：讓AI瞎折騰一通，吐出上千行絮絮叨叨的代碼，這真的省時間嗎？

陶哲軒的回答是肯定的。

雖然和ChatGPT互動有時讓人抓狂，但對比他親自動手從零寫這1125行Lean證明，AI至少幫他節省了一半以上的時間和精力。

更有趣的是，ChatGPT在對話中還能及時發現陶哲軒提要求時的一些小錯誤，比如參數取值不當等，然后自動糾正再生成代碼。

它不僅是聽話的碼農，偶爾還兼職「質檢」，替人類把關。

這種體驗讓陶哲軒直呼過癮——過去覺得不值得一試的繁瑣計算，現在敢放心交給AI跑，他則專注于更有創意的部分。

當然，并不是說AI已經萬能。

其實在正式編寫Lean證明的過程中，大量低級而重復的收尾工作最后還是人類在做。

ChatGPT寫出的代碼片段往往需要陶哲軒仔細檢查、微調格式，然后粘貼進Lean運行，看是否通過。

一旦報錯，再回頭提示ChatGPT修改。

許多時候AI會陷入一個狹窄思路，不停產出同樣錯的代碼，需要人類耐心引導它跳出死循環。

這一切都說明，AI目前充當的是「能力強大的助理」角色，而非獨立的數學家。

正如Nature雜志的每日簡報所指出，這些工具可以幫助數學家確認某些近乎不可琢磨的證明、為困難問題出謀劃策，但離自動產出完整新證明還有距離。

人類的智慧仍是不可或缺的。至少現在來看，最精彩的創意和洞見，AI還給不出來。

{1, 2, 4, 8, 13}推翻了Erd?s猜想

另一則引發轟動的案例發生在Erd?s第707號問題上。

這道問題關乎組合數學中的Sidon集合與完美差集的關系——聽上去高深莫測，但簡單來說，Erd?s猜想任何一個特殊的「Sidon數集」都能擴充成某種「完美差集」。

這個猜想懸而未決幾十年，獎金為1000美元。

直到最近，兩位數學家鮑里斯·阿列克謝夫（Boris Alexeev）和達斯汀·米克森（Dustin G. Mixon）找到了令人意外的反例：集合{1, 2, 4, 8, 13}就是一個無法擴充成完美差集的Sidon集！

五個看似普通的數字，就這樣終結了一個長期懸而未決的猜想，令數學界既興奮又驚訝。

發現反例只是故事的一半。

這兩位研究者做了一個大膽決定：讓AI來驗證他們的發現。

他們聽說陶哲軒成功用ChatGPT編寫Lean證明，于是如法炮制，請出最新的大模型來協助，把反例證明從頭到尾寫成Lean代碼。

他們不僅形式化了自己找到的新反例，還讓AI把幾十年前一位數學家馬歇爾·霍爾（Marshall Hall Jr.）曾給出的另一個反例也寫成Lean證明。

其實霍爾的結果早在1940年代就發表了，但長期被學界忽視了。

Marshall Hall Jr. 在 1947 年的論文《Cyclic projective planes》（Duke Math. J. 14(4): 1079–1090）里，在定理 4.3 后的下一段，給出了不能擴展為任何有限完美差集（λ=1 的差集，亦稱平面差集）的具體反例。

原文里他舉的例子就是：

「For example the set {?8, ?6, 0, 1, 4} may not be so extended.」（「例如集合{?8, ?6, 0, 1, 4}不能如此擴展。」） 

https://projecteuclid.org/journals/duke-mathematical-journal/volume-14/issue-4/Cyclic-projective-planes/10.1215/S0012-7094-47-01482-8.short

這一切聽起來就像讓AI一邊考古、一邊蓋新樓——把人類數學遺產用現代工具重做一遍，以確保萬無一失。

結果如何呢？

ChatGPT不負眾望，經過無數次人機對話和嘗試，最終吐出了長達數千行的Lean證明代碼，把新舊兩個反例案例統統嚴絲合縫地驗證了一遍。

論文作者感嘆：「正式證明幾乎每一行都是ChatGPT寫的」。

可以說，沒有AI幫忙，這樣繁瑣的形式化工作幾乎不可能在短時間內完成。

這也是他們為何在論文初稿中大膽署名ChatGPT和Lean為共同作者的原因——一個寫了證明，一個審了證明。

這一舉動由于arXiv的規定，最后發表時還是去掉了AI作者的名字。

更令人好奇的是，他們采用的也是類似「vibe coding」的交互式編程方式。

不是預先設計好完整證明步驟，再讓AI去填空，而是邊想邊讓AI試，一步步把想法轉化為代碼。

這樣做的好處是人類不需要過多操心Lean的語法細節，而由AI根據上下文「自由發揮」提案，然后人類再篩選糾正。

這種人機協作方式頗有即興創作的味道：AI提供源源不斷的靈感火花，人類負責辨別哪些是寶石、哪些只是火花。

然而這種自由也帶來了大量「垃圾代碼」和反復嘗試。

作者直言，最終的Lean證明簡直是一鍋夾生的「意大利面」，里面充滿了AI走彎路留下的冗余邏輯。

好在有Lean這個「蜻蜓隊長」把關，每個步驟都嚴格審核，否則真不敢相信AI產出的證明就一定可靠。

正如兩位作者所強調的，大模型常常幻覺、出錯，如果沒有形式化驗證（如使用Lean），根本無法信任這樣的證明。

AI+人類

數學證明的新范式

AI與人類在數學中協作的藝術想象。

國外權威媒體也開始關注這一趨勢：數學證明正悄悄進入「AI輔助時代」。

Quanta Magazine就報道了數學家們對于AI助手的看法，許多人已經在為這種范式轉變做準備，思考在AI時代如何重新定義「證明」。

畢竟從歷史看，每當出現新工具，數學家的工作方式就會隨之改變：計算器、計算機代數系統，現在輪到了智能AI。

即使只能把證明中枯燥繁瑣的部分外包給AI，也將「極大改變我們從事數學的方式」。

的確，當人類不再需要手動檢查每個細節，就能把更多精力放在創造性的思考上。

另一方面，也有數學家提出謹慎的聲音。

蒙特利爾大學的安德魯·格蘭維爾（Andrew Granville）坦言，他擔心過度依賴AI驗證會讓研究者失去鍛煉思維的機會：

真正的理解往往來自于親自動手，「弄臟雙手」。

Andrew Granville

這種顧慮不無道理：如果AI成了拐杖，年輕一代會不會變得不善于獨立證明？

然而，多數專家認為，與其抗拒AI，不如主動擁抱、學習駕馭。

畢竟紙和鉛筆的時代早已過去，電腦驗算、機器證明正成為新常態。

未來的數學家或許更像是總指揮，調度AI這個強大的工具完成證明，就像科學家使用實驗儀器那樣。

陶哲軒把這種前景稱作「數學的工業化時代」，要用AI擴充數學家的能力版圖。

一如當年國際象棋出現計算機助手，頂尖棋手學會與電腦共舞，開辟出人機融合的新境界。

數學領域如今也站在類似的門檻上：AI不會取代數學家，但正在成為數學家工作桌上的標配工具。

也許若干年后，我們回顧這段歷史時，會驚嘆地發現：正是從ChatGPT與Lean的「合奏」開始，證明的方式被重新定義，人類對真理的探索奏響了新的樂章。

在AI的陪伴下，數學家的征途不再是孤軍奮戰，而更像是一場人與機器聯袂出演的華麗冒險。

定理未必更容易求證了，但證明的旅程，變得前所未有的精彩。