陶哲軒親測Claude跑崩電腦，全靠這份保姆級指令清單翻盤

新智元報道

編輯：元宇

【新智元導讀】從電腦崩潰到半小時拿下Lean形式化證明，數學大神陶哲軒用親身踩坑經歷警告：AI越強大，人類越不能偷懶，應時刻保持「人類在環」的絕對清醒。

連跑45分鐘，燒光Token，最后電腦直接死機。

你可能很難想象，這竟是全球頂尖數學家陶哲軒在實測最新AI編程工具時，遭遇的一次真實翻車現場。

九個月前，他曾在一個視頻中向大家展示如何將一段復雜的數學證明形式化。

九個月后，面對被業界瘋狂追捧的新一代AI助手Claude Code，他本以為這會是一場降維打擊。

沒想到，第一次完全放權給AI，不僅沒有完成數學證明，還把自己的電腦搞崩潰了。

在接到一句宏大的指令后，AI陷入了瘋狂的回溯與試錯，狂跑了45分鐘，不僅沒寫出一行可用代碼，龐大的計算過載還把電腦弄死機了。

眼下整個科技圈都在狂熱地討論AI智能體。

仿佛只要隨手拋出一句話，AI就能替你打理好全部工作。陶哲軒這場硬核實測，卻像一劑清醒劑，終結了這種技術幻覺：

即使面對再強大的AI，人類也不能完全「關掉大腦」。

保持參與，才是最好的使用AI的方式。

「一波流」幻想破滅

AI智能體的「過載陷阱」

故事要從九個月前說起。

在當時的Equations of Theories項目里，為了證明等式1689能夠推導出等式2（即singleton law），陶哲軒使用GitHub Copilot和一個名叫conical的輔助工具，靠著人類的智慧和輕度的AI輔助，一步步手動完成了證明的形式化。

如今，全面升級的智能體來了。

由于對AI的過度信任，陶哲軒在第一次嘗試Claude時進入了一個極其普遍的誤區，他給Claude下達了一個大而籠統的指令：「請把整個事情都做完。」

他原本以為，AI會自動拆解任務、理清邏輯、輸出完美代碼。

然而這句不加限制的指令，直接觸發了機器的「過載陷阱」。面對復雜的邏輯鏈條，Claude在底層引理的證明泥潭里迷失了方向。

它花了大把時間去猜測該怎么做，接著犯錯，然后瘋狂回溯、推倒重做。

就這樣，在燒掉大量Token之后，AI狂跑了整整45分鐘仍然一無所獲。而且，龐大的計算壓力，也讓陶哲軒的電腦崩潰了。

事實證明，當人類下達給AI的任務指令缺乏清晰邊界時，AI的勤奮只會像無頭蒼蠅式的亂撞，最終演變成一場徒勞無益的消耗。

這次慘痛的教訓，也戳破了當下人們對AI的一個幻覺：認為有了智能體，自己就可以當「甩手掌柜」了。

「保姆級」指令的勝利

真正的轉折，發生在第二次和第三次嘗試里。

第二次，其實已經成功了。

陶哲軒把任務拆開，不再要求Claude Code一次完成全部證明，而是先形式化引理1、引理2、引理3，再逐步把證明補進去。

最后大約用了25分鐘，完整證明做出來了。

在第三次，他還摸索出了一套防AI「暴走」的干貨步驟，核心秘訣，就是專門建一個Markdown文件，把所有指令按步驟寫清楚，再交給Claude Code執行。

只是這次他并沒這么做，而是把這些步驟直接寫進Lean文件的注釋里。

這套流程的精髓，不在于復雜，而在于克制。

第零步，先形式化S和F這兩個記號。先把符號系統立住，別急著證明。

第一步，創建證明骨架。把引理1、引理2、引理3的陳述都形式化出來，但這個階段嚴禁AI嘗試證明，一律用「sorry」占位。

這一步看似保守，實際上非常高明。因為他已經從第一次失敗里看明白了：

一旦讓Claude Code過早進入「我要把它證出來」的狀態，它就會在證明細節里瘋狂打轉，反復試、反復錯、反復回退，最后什么都做不完。

與其讓它一上來就沖刺，不如先讓它把結構搭好。

然后才是第二步：把非形式化證明里的每一行，逐行轉成Lean代碼。

理由先不補，能用「sorry」的地方先用「sorry」。

這個動作特別像搭腳手架。先把房子的梁柱立起來，再慢慢砌墻，而不是抱著一堆磚頭就想直接蓋完。

也是在這里，陶哲軒點出了Claude Code一個很有意思的弱點：它在最底層、最機械的步驟上，反而容易「想太多」。

本來人類可能覺得「這一步一兩行就該結束了」，它卻會繞出更長的路徑。

在陶哲軒的第一次嘗試時，AI甚至不愿意沿用S和F這些簡寫，而是把式子不斷展開，導致證明越來越難讀。

這正是很多人今天會誤判AI的地方。

你以為它最擅長的是細活，它偏偏會在最該老實執行的時候，突然開始「發揮創造力」。

而在形式化證明這類任務中，過度發揮，往往不是加分項，反而可能是事故源頭。

在這套「保姆級」指令的約束下，Claude終于不再像脫韁的野馬。它老老實實地跟著人類給定的證明，幾秒鐘就吐出了規整的代碼框架。

「人機并行協作」

你做你的填空，我修我的Bug

真正讓這次實踐變得好看的，是中間那段非常絲滑的人機配合感。

做到一半，電腦又崩了一次。

但這一次，崩潰沒有毀掉進度。

原因很簡單：因為任務已經被拆成了一段一段的小步驟，所以恢復起來并不痛苦。

分步推進，不只是為了防止AI暴走，也是為了人類后期修改方便。

更精彩的戲碼是在修Bug階段。

在填補細節時，Claude卡在了某個底層步驟上。陶哲軒發現，AI把記號SA展開了兩次，而實際上只需展開一次。

面對這個邏輯死結，AI試圖換一種極其復雜的思路去繞過它，甚至給出了一段冗長代碼。

這個時候，人類的作用顯現了。

陶哲軒果斷出手，他調出Info View面板，親自接管了這行邏輯。

面對多余的展開項，他直接使用congruence（消掉同類項），瞬間清空了報錯信息。連他自己都忍不住感慨：「這也太強了，居然直接就成了。」

隨后，他又意識到，這里其實可以把H1抽出來，單獨作為一個關鍵方程引理，因為后面兩個地方都能復用它。

此時，全場高潮的「人機結對編程」畫面出現了。

當陶哲軒在前方手動修復復雜邏輯、提取引理時，Claude Code根本沒有閑著。

它在后臺默默同步，聰明地把過去代碼里的H1替換成了一行簡練的證明，并自動給后續的引理三搭好了骨架。

這才是這次實驗最舒服的一幕：不是你命令，我執行；也不是你放手，我亂跑；而是兩者在同一個代碼庫里獨立運轉，互不干擾卻又完美配合。

像一場真正的結對編程，只不過你的搭檔，不是另一個人類，而是一個需要被約束、但又確實能干活的智能體。

拒絕「多智能體焦慮」

要把手放在方向盤上

最后，這份證明完成了。

總耗時大約半小時，里面還算上了一次系統崩潰。對比第一次45分鐘空轉到電腦死機，這個結果已經足夠說明問題。

但在復盤階段，這位數學大神給出的，不是某種神話式結論，而是一種很清醒的技術態度。

他顯然看到了自動化的誘惑。

Claude Code足夠強，大多數人很容易生出一種沖動：干脆讓它全包，我少操點心。

可問題在于，一旦你真這么做，它很可能直接扔掉你原本已經很好的非形式化思路，按它自己的方式重寫一遍。

結果，就是代碼變得晦澀難懂，一旦跑不通，你連調試都無從下手。

他還順手吐槽了當下很流行的一種趨勢：

讓多個智能體同時跑，再用另一個智能體去管理前面那幾個智能體。

理論上當然可以。

可至少在這次任務里，他已經對單個、聽話、受控的Agent非常滿意了。再往上疊，不一定是效率提升，也可能只是另一種形式的復雜化焦慮。

此外，在這場技術洪流中，人類必須保持參與感。

最頂級的AI工作流，不是關掉大腦，而是始終把手放在方向盤上。

因為一旦完全依賴工具，出了問題，你能做的往往只剩下一遍遍重新調用，像是在對一個黑箱許愿。

而當你把「人類在環」這件事堅持到底，局面就完全不同了。

這時候，AI不是替你思考的大腦，而是你手里那把越來越鋒利的劍。真正決定它往哪兒揮的人，仍然還得是你。

參考資料：

https://mathstodon.xyz/@tao/116190707979654536%20

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/equational.lean%20

https://www.youtube.com/watch?v=JHEO7cplfk8