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

（來源：Youtube）

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

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

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

（來源：Youtube）

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

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

大佬用 AI 也會翻車

有趣的是，視頻中所展示的流暢流程并非一蹴而就。陶哲軒在錄制中坦言，這是他第三次嘗試用 Claude Code 完成該任務(wù)。在此之前，他因為不同原因已經(jīng)“翻車”了兩次。

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

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

（來源：Youtube）

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

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

1. 搭建骨架（Skeletonization）

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

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

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

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

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

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

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

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

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

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

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

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

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

（來源：X）

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

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

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

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

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

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

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

運營/排版：何晨龍