近日，菲爾茲獎(jiǎng)得主、加州大學(xué)洛杉磯分校（UCLA）數(shù)學(xué)系教授陶哲軒（Terence Tao）在 YouTube 發(fā)布了一段時(shí)長約 26 分鐘的實(shí)操視頻，詳細(xì)演示了如何利用 Anthropic 推出的 Claude Code 代理工具，在 Lean 定理證明器中完成一項(xiàng)數(shù)學(xué)證明的形式化全過程。

（來源：Youtube）

陶哲軒在視頻開始就明確了任務(wù)目標(biāo)：將集合論中的“單例定律”（Singleton Law）從非形式化的自然語言描述，轉(zhuǎn)化為 Lean 系統(tǒng)能夠編譯和嚴(yán)格驗(yàn)證的代碼。簡而言之，該定律論證了對于任意集合 A 和元素 x，單例集合 {x}屬于 A 的條件等價(jià)于某些特定的子集屬性。

盡管這在數(shù)學(xué)概念上這屬于較為基礎(chǔ)的引理，但要在類型論嚴(yán)苛的 Lean 系統(tǒng)中完成形式化，卻伴隨著大量瑣碎且對語法要求極高的代碼編寫工作。

這并非陶哲軒首次處理這一任務(wù)。大約九個(gè)月前，他曾在其主導(dǎo)的“方程理論”（Equation Theories）項(xiàng)目中，已經(jīng)利用當(dāng)時(shí)的主流工具（如 GitHub Copilot）手動(dòng)完成了該證明。

（來源：Youtube）

這次引入 Claude Code 重做此題，陶哲軒是想直觀對比新一代“代理式編碼工具”與上一代代碼補(bǔ)全工具之間的代際差異。

與 GitHub Copilot 早期僅能基于光標(biāo)位置提供幾行代碼自動(dòng)補(bǔ)全不同，Claude Code 是一個(gè)運(yùn)行在終端的代理系統(tǒng)，能夠理解復(fù)雜的自然語言指令，自主讀取文件目錄，規(guī)劃步驟，并自動(dòng)執(zhí)行代碼編輯和修改。在陶哲軒看來，這種能力的躍升或許讓 AI 有望真正接管數(shù)學(xué)研究中被稱為“繁文縟節(jié)”的重復(fù)性勞作。

大佬用 AI 也會(huì)翻車

有趣的是，視頻中所展示的流暢流程并非一蹴而就。陶哲軒在錄制中坦言，這是他第三次嘗試用 Claude Code 完成該任務(wù)。在此之前，他因?yàn)椴煌蛞呀?jīng)“翻車”了兩次。

在第一次嘗試中，陶哲軒直接給出了一個(gè)宏觀指令，要求 Claude“完成整個(gè)證明”。結(jié)果，AI 在連續(xù)運(yùn)行了 45 分鐘后，消耗了海量 Token 并導(dǎo)致電腦崩潰，最終未能產(chǎn)出任何有效結(jié)果。

有網(wǎng)友直接在評論區(qū)@Anthropic：“給陶哲軒開個(gè)無限 Token 權(quán)限吧，說不定數(shù)學(xué) 2.0 時(shí)代能提前到來！”這話聽著像玩笑，卻也戳中了當(dāng)前 AI 工具的一個(gè)現(xiàn)實(shí)痛點(diǎn)：真干起精細(xì)活來，Token 消耗的速度是真快。

（來源：Youtube）

第二次嘗試時(shí)，他改變了策略，要求 AI 按引理（Lemma 1, 2, 3）分步執(zhí)行，這次耗時(shí) 25 分鐘成功完成，但因錄屏軟件故障未能保存。

吸取了第一次的教訓(xùn)，在第三次（即本次發(fā)布的視頻）實(shí)操中，陶哲軒采用了高度結(jié)構(gòu)化的“腳手架”（Scaffolding）策略。他在文件頂部撰寫了一份極其詳盡的“配方”（Recipe），將任務(wù)拆解為初始定義、大綱搭建以及三個(gè)子引理的逐步證明，以此來約束 AI 的行動(dòng)發(fā)散空間。

1. 搭建骨架（Skeletonization）

流程初期，陶哲軒指令 Claude Code 先不要急于推導(dǎo)，而是用 Lean 系統(tǒng)中的占位符“sorry”搭建起整個(gè)證明的宏觀框架。這一步進(jìn)行得異常順利，AI 準(zhǔn)確識(shí)別了非形式化證明中的邏輯斷點(diǎn)，并將其轉(zhuǎn)化為 Lean 代碼結(jié)構(gòu)。陶哲軒指出，讓 AI 先寫出帶有“sorry”的骨架，隨后再逐一填補(bǔ)，是目前最高效的人機(jī)協(xié)作模式。

2. 陷入泥潭與人工干預(yù)

然而，在具體填補(bǔ) Lemma 1 的證明細(xì)節(jié)時(shí)，Claude Code 的短板開始顯現(xiàn)。由于 Lean 的底層邏輯要求高度嚴(yán)謹(jǐn)，AI 在面對非形式化語言中的等式代換時(shí)，表現(xiàn)出“過度思考”的傾向。它試圖頻繁展開底層的數(shù)學(xué)定義，而不是機(jī)械地按照人類給出的步驟進(jìn)行推演。

在視頻中，AI 在后臺(tái)進(jìn)行了大量的回溯和自我試錯(cuò)，消耗了大量計(jì)算資源，推導(dǎo)過程變得異常冗長。在這個(gè)過程中，陶哲軒的工作站甚至意外宕機(jī)了一次。系統(tǒng)恢復(fù)后，面對 AI 將簡單步驟復(fù)雜化的窘境，陶哲軒果斷選擇人工介入。他直接接管了鍵盤，迅速輸入了一個(gè)基于 congr（同余/等式替換）指令的策略，瞬間突破了僵局。

他客觀評價(jià)道：“過度依賴工具可能會(huì)讓你失去對證明的直覺。當(dāng) AI 陷入死胡同時(shí)，人類直接上手往往比等待它糾錯(cuò)要快得多?！?/p>

3. 演化出“并行工作流”

隨著進(jìn)程推進(jìn)到 Lemma 2 和 Lemma 3，陶哲軒展示了令人眼前一亮的工作流創(chuàng)新。當(dāng)他確認(rèn) AI 已經(jīng)掌握了骨架搭建的技巧后，他不再單純扮演“監(jiān)督者”，而是開始與 AI“雙線操作”。當(dāng) Claude Code 在后臺(tái)自主分析并試圖填補(bǔ) Lemma 3 的底層邏輯時(shí)，陶哲軒則在代碼的前段手動(dòng)補(bǔ)全 Lemma 2 中相對直觀的"sorry"部分。

這種人機(jī)并行作業(yè)的模式，最后將總耗時(shí)壓縮到了約半小時(shí)以內(nèi)，并且最終代碼毫無報(bào)錯(cuò)地通過了 Lean 編譯器的嚴(yán)格審查。陶哲軒總結(jié)稱，將任務(wù)切分，人類處理一目了然的邏輯，而將需要堆砌代碼的繁重任務(wù)交由代理，是現(xiàn)階段最具可行性的實(shí)踐。

AI 從“平庸助教”到“初級合作者”

若將此次視頻置于陶哲軒近年來對 AI 的系列實(shí)驗(yàn)史中審視，我們能清晰地看到一條技術(shù)躍遷的軌跡。

早在此輪生成式 AI 爆發(fā)之初，陶哲軒就曾積極測試各類聊天機(jī)器人，并將其比作“平庸但不完全無能的研究生”。彼時(shí)的 AI 在處理如微積分中的 epsilon-delta 極限證明時(shí)，極易出現(xiàn)幻覺，頻繁混淆變量域或遺漏邊界條件，更多是作為一種新奇的玩具存在。

到了 2025 年，隨著大模型基礎(chǔ)能力的提升，陶哲軒曾公開測試 GPT-5 級別模型在復(fù)雜學(xué)術(shù)文獻(xiàn)檢索上的表現(xiàn)。在那次測試中，AI 能夠快速在海量未完全結(jié)構(gòu)化的論文庫中挖掘出特定的定理淵源，為他節(jié)省了數(shù)周的案頭檢索時(shí)間。然而，當(dāng)時(shí) AI 扮演的仍是“高級圖書管理員”的輔助角色，而非直接介入證明的生成。

而進(jìn)入 2026 年初，形勢發(fā)生了質(zhì)的變化。以 ChatGPT 為代表的大模型在著名的 Erd?s 開放猜想庫中發(fā)力，試圖“獨(dú)立”解決這些涵蓋數(shù)論與組合學(xué)數(shù)百個(gè)未解之謎的問題。陶哲軒的 GitHub 主頁也記錄了利用這些系統(tǒng)自動(dòng)化處理周邊猜想的嘗試，填補(bǔ)了人類因精力有限而忽略的邊緣地帶。

（來源：X）

本次利用 Claude Code 進(jìn)行的演示，恰恰是連接上述“前沿探索”與“日常實(shí)踐”的橋梁。雖然不如谷歌 AlphaProof 解出國際數(shù)學(xué)奧林匹克（IMO）難題那般具有極高的公眾戲劇性，但在 Lean 這一類型論保障的確定性環(huán)境中，陶哲軒的演示更為接地氣，也更貼近當(dāng)代數(shù)學(xué)家真實(shí)的研究常態(tài)。

當(dāng)然，在肯定 AI 帶來的效率革命的同時(shí)，陶哲軒及其代表的數(shù)學(xué)界并未回避技術(shù)現(xiàn)存的局限性。

一方面，學(xué)術(shù)界有聲音擔(dān)憂，高度依賴 AI 生成的證明可能會(huì)引入“黑箱化”問題。即便 Lean 編譯器能夠從邏輯底層保證代碼 100% 的正確性，但長篇累牘、由機(jī)器生成的機(jī)器語言缺乏人類數(shù)學(xué)特有的直覺美感和可讀性，這可能導(dǎo)致數(shù)學(xué)從一門“理解的藝術(shù)”異化為單純的“符號驗(yàn)證”。

對此，陶哲軒保持了科學(xué)家特有的客觀與中立。他傾向于將 AI 定義為一種強(qiáng)大的“實(shí)驗(yàn)數(shù)學(xué)”工具。對于高度依賴計(jì)算和模式匹配的任務(wù)，AI 無可替代；但涉及黎曼猜想這類需要顛覆性直覺和深層概念重構(gòu)的核心領(lǐng)域，人類的主導(dǎo)地位依然穩(wěn)固。

正如他此前在 IPAM 會(huì)議上所言：“只要 AI 為你節(jié)省的時(shí)間，多于你為了糾正它而浪費(fèi)的時(shí)間，它就是一款成功的工具?！贝舜伍L達(dá) 26 分鐘的無剪輯視頻，正是對這一論斷的最好背書。

在未來的數(shù)學(xué)研究中，“人機(jī)共作”或?qū)⒊蔀橐环N新常態(tài)。屆時(shí)，也許 AI 能夠以“初級合作者”的身份，徹底打通數(shù)學(xué)從直覺構(gòu)想到計(jì)算機(jī)形式化驗(yàn)證之間的瓶頸。

視頻地址：https://www.youtube.com/watch?v=JHEO7cplfk8&t=124s

運(yùn)營/排版：何晨龍