新智元報道

編輯：元宇

【新智元導(dǎo)讀】從電腦崩潰到半小時拿下Lean形式化證明，數(shù)學(xué)大神陶哲軒用親身踩坑經(jīng)歷警告：AI越強(qiáng)大，人類越不能偷懶，應(yīng)時刻保持「人類在環(huán)」的絕對清醒。

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

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

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

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

沒想到，第一次完全放權(quán)給AI，不僅沒有完成數(shù)學(xué)證明，還把自己的電腦搞崩潰了。

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

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

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

即使面對再強(qiáng)大的AI，人類也不能完全「關(guān)掉大腦」。

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

「一波流」幻想破滅

AI智能體的「過載陷阱」

故事要從九個月前說起。

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

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

由于對AI的過度信任，陶哲軒在第一次嘗試Claude時進(jìn)入了一個極其普遍的誤區(qū)，他給Claude下達(dá)了一個大而籠統(tǒng)的指令：「請把整個事情都做完?！?/p>

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

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

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

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

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

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

「保姆級」指令的勝利

真正的轉(zhuǎn)折，發(fā)生在第二次和第三次嘗試?yán)铩?/p>

第二次，其實(shí)已經(jīng)成功了。

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

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

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

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

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

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

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

這一步看似保守，實(shí)際上非常高明。因?yàn)樗呀?jīng)從第一次失敗里看明白了：

一旦讓Claude Code過早進(jìn)入「我要把它證出來」的狀態(tài)，它就會在證明細(xì)節(jié)里瘋狂打轉(zhuǎn)，反復(fù)試、反復(fù)錯、反復(fù)回退，最后什么都做不完。

與其讓它一上來就沖刺，不如先讓它把結(jié)構(gòu)搭好。

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

理由先不補(bǔ)，能用「sorry」的地方先用「sorry」。

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

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

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

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

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

你以為它最擅長的是細(xì)活，它偏偏會在最該老實(shí)執(zhí)行的時候，突然開始「發(fā)揮創(chuàng)造力」。

而在形式化證明這類任務(wù)中，過度發(fā)揮，往往不是加分項(xiàng)，反而可能是事故源頭。

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

「人機(jī)并行協(xié)作」

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

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

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

但這一次，崩潰沒有毀掉進(jìn)度。

原因很簡單：因?yàn)槿蝿?wù)已經(jīng)被拆成了一段一段的小步驟，所以恢復(fù)起來并不痛苦。

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

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

在填補(bǔ)細(xì)節(jié)時，Claude卡在了某個底層步驟上。陶哲軒發(fā)現(xiàn)，AI把記號SA展開了兩次，而實(shí)際上只需展開一次。

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

這個時候，人類的作用顯現(xiàn)了。

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

面對多余的展開項(xiàng)，他直接使用congruence（消掉同類項(xiàng)），瞬間清空了報錯信息。連他自己都忍不住感慨：「這也太強(qiáng)了，居然直接就成了?！?/p>

隨后，他又意識到，這里其實(shí)可以把H1抽出來，單獨(dú)作為一個關(guān)鍵方程引理，因?yàn)楹竺鎯蓚€地方都能復(fù)用它。

此時，全場高潮的「人機(jī)結(jié)對編程」畫面出現(xiàn)了。

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

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

這才是這次實(shí)驗(yàn)最舒服的一幕：不是你命令，我執(zhí)行；也不是你放手，我亂跑；而是兩者在同一個代碼庫里獨(dú)立運(yùn)轉(zhuǎn)，互不干擾卻又完美配合。

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

拒絕「多智能體焦慮」

要把手放在方向盤上

最后，這份證明完成了。

總耗時大約半小時，里面還算上了一次系統(tǒng)崩潰。對比第一次45分鐘空轉(zhuǎn)到電腦死機(jī)，這個結(jié)果已經(jīng)足夠說明問題。

但在復(fù)盤階段，這位數(shù)學(xué)大神給出的，不是某種神話式結(jié)論，而是一種很清醒的技術(shù)態(tài)度。

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

Claude Code足夠強(qiáng)，大多數(shù)人很容易生出一種沖動：干脆讓它全包，我少操點(diǎn)心。

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

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

他還順手吐槽了當(dāng)下很流行的一種趨勢：

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

理論上當(dāng)然可以。

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

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

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

因?yàn)橐坏┩耆蕾嚬ぞ撸隽藛栴}，你能做的往往只剩下一遍遍重新調(diào)用，像是在對一個黑箱許愿。

而當(dāng)你把「人類在環(huán)」這件事堅(jiān)持到底，局面就完全不同了。

這時候，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