近日，菲爾茲獎得主、加州大學洛杉磯分校（UCLA）數學系教授陶哲軒（Terence Tao）在 YouTube 發佈了一段時長約 26 分鐘的實操視頻，詳細演示瞭如何利用 Anthropic 推出的 Claude Code 代理工具，在 Lean 定理證明器中完成一項數學證明的形式化全過程。
（來源：Youtube）
陶哲軒在視頻開始就明確了任務目標：將集合論中的“單例定律”（Singleton Law）從非形式化的自然語言描述，轉化爲 Lean 系統能夠編譯和嚴格驗證的代碼。簡而言之，該定律論證了對於任意集合 A 和元素 x，單例集合 {x}屬於 A 的條件等價於某些特定的子集屬性。
儘管這在數學概念上這屬於較爲基礎的引理，但要在類型論嚴苛的 Lean 系統中完成形式化，卻伴隨着大量瑣碎且對語法要求極高的代碼編寫工作。
這並非陶哲軒首次處理這一任務。大約九個月前，他曾在其主導的“方程理論”（Equation Theories）項目中，已經利用當時的主流工具（如 GitHub Copilot）手動完成了該證明。
（來源：Youtube）
這次引入 Claude Code 重做此題，陶哲軒是想直觀對比新一代“代理式編碼工具”與上一代代碼補全工具之間的代際差異。
與 GitHub Copilot 早期僅能基於光標位置提供幾行代碼自動補全不同，Claude Code 是一個運行在終端的代理系統，能夠理解複雜的自然語言指令，自主讀取文件目錄，規劃步驟，並自動執行代碼編輯和修改。在陶哲軒看來，這種能力的躍升或許讓 AI 有望真正接管數學研究中被稱爲“繁文縟節”的重複性勞作。
大佬用 AI 也會翻車
有趣的是，視頻中所展示的流暢流程並非一蹴而就。陶哲軒在錄製中坦言，這是他第三次嘗試用 Claude Code 完成該任務。在此之前，他因爲不同原因已經“翻車”了兩次。
在第一次嘗試中，陶哲軒直接給出了一個宏觀指令，要求 Claude“完成整個證明”。結果，AI 在連續運行了 45 分鐘後，消耗了海量 Token 並導致電腦崩潰，最終未能產出任何有效結果。
有網友直接在評論區@Anthropic：“給陶哲軒開個無限 Token 權限吧，說不定數學 2.0 時代能提前到來！”這話聽着像玩笑，卻也戳中了當前 AI 工具的一個現實痛點：真幹起精細活來，Token 消耗的速度是真快。
（來源：Youtube）
第二次嘗試時，他改變了策略，要求 AI 按引理（Lemma 1, 2, 3）分步執行，這次耗時 25 分鐘成功完成，但因錄屏軟件故障未能保存。
吸取了第一次的教訓，在第三次（即本次發佈的視頻）實操中，陶哲軒採用了高度結構化的“腳手架”（Scaffolding）策略。他在文件頂部撰寫了一份極其詳盡的“配方”（Recipe），將任務拆解爲初始定義、大綱搭建以及三個子引理的逐步證明，以此來約束 AI 的行動發散空間。
1. 搭建骨架（Skeletonization）
流程初期，陶哲軒指令 Claude Code 先不要急於推導，而是用 Lean 系統中的佔位符“sorry”搭建起整個證明的宏觀框架。這一步進行得異常順利，AI 準確識別了非形式化證明中的邏輯斷點，並將其轉化爲 Lean 代碼結構。陶哲軒指出，讓 AI 先寫出帶有“sorry”的骨架，隨後再逐一填補，是目前最高效的人機協作模式。
2. 陷入泥潭與人工干預
然而，在具體填補 Lemma 1 的證明細節時，Claude Code 的短板開始顯現。由於 Lean 的底層邏輯要求高度嚴謹，AI 在面對非形式化語言中的等式代換時，表現出“過度思考”的傾向。它試圖頻繁展開底層的數學定義，而不是機械地按照人類給出的步驟進行推演。
在視頻中，AI 在後臺進行了大量的回溯和自我試錯，消耗了大量計算資源，推導過程變得異常冗長。在這個過程中，陶哲軒的工作站甚至意外宕機了一次。系統恢復後，面對 AI 將簡單步驟複雜化的窘境，陶哲軒果斷選擇人工介入。他直接接管了鍵盤，迅速輸入了一個基於 congr（同餘/等式替換）指令的策略，瞬間突破了僵局。
他客觀評價道：“過度依賴工具可能會讓你失去對證明的直覺。當 AI 陷入死衚衕時，人類直接上手往往比等待它糾錯要快得多。”
3. 演化出“並行工作流”
隨着進程推進到 Lemma 2 和 Lemma 3，陶哲軒展示了令人眼前一亮的工作流創新。當他確認 AI 已經掌握了骨架搭建的技巧後，他不再單純扮演“監督者”，而是開始與 AI“雙線操作”。當 Claude Code 在後臺自主分析並試圖填補 Lemma 3 的底層邏輯時，陶哲軒則在代碼的前段手動補全 Lemma 2 中相對直觀的"sorry"部分。
這種人機並行作業的模式，最後將總耗時壓縮到了約半小時以內，並且最終代碼毫無報錯地通過了 Lean 編譯器的嚴格審查。陶哲軒總結稱，將任務切分，人類處理一目瞭然的邏輯，而將需要堆砌代碼的繁重任務交由代理，是現階段最具可行性的實踐。
AI 從“平庸助教”到“初級合作者”
若將此次視頻置於陶哲軒近年來對 AI 的系列實驗史中審視，我們能清晰地看到一條技術躍遷的軌跡。
早在此輪生成式 AI 爆發之初，陶哲軒就曾積極測試各類聊天機器人，並將其比作“平庸但不完全無能的研究生”。彼時的 AI 在處理如微積分中的 epsilon-delta 極限證明時，極易出現幻覺，頻繁混淆變量域或遺漏邊界條件，更多是作爲一種新奇的玩具存在。
到了 2025 年，隨着大模型基礎能力的提升，陶哲軒曾公開測試 GPT-5 級別模型在複雜學術文獻檢索上的表現。在那次測試中，AI 能夠快速在海量未完全結構化的論文庫中挖掘出特定的定理淵源，爲他節省了數週的案頭檢索時間。然而，當時 AI 扮演的仍是“高級圖書管理員”的輔助角色，而非直接介入證明的生成。
而進入 2026 年初，形勢發生了質的變化。以 ChatGPT 爲代表的大模型在著名的 Erdős 開放猜想庫中發力，試圖“獨立”解決這些涵蓋數論與組合學數百個未解之謎的問題。陶哲軒的 GitHub 主頁也記錄了利用這些系統自動化處理周邊猜想的嘗試，填補了人類因精力有限而忽略的邊緣地帶。
（來源：X）
本次利用 Claude Code 進行的演示，恰恰是連接上述“前沿探索”與“日常實踐”的橋樑。雖然不如谷歌 AlphaProof 解出國際數學奧林匹克（IMO）難題那般具有極高的公衆戲劇性，但在 Lean 這一類型論保障的確定性環境中，陶哲軒的演示更爲接地氣，也更貼近當代數學家真實的研究常態。
當然，在肯定 AI 帶來的效率革命的同時，陶哲軒及其代表的數學界並未迴避技術現存的侷限性。
一方面，學術界有聲音擔憂，高度依賴 AI 生成的證明可能會引入“黑箱化”問題。即便 Lean 編譯器能夠從邏輯底層保證代碼 100% 的正確性，但長篇累牘、由機器生成的機器語言缺乏人類數學特有的直覺美感和可讀性，這可能導致數學從一門“理解的藝術”異化爲單純的“符號驗證”。
對此，陶哲軒保持了科學家特有的客觀與中立。他傾向於將 AI 定義爲一種強大的“實驗數學”工具。對於高度依賴計算和模式匹配的任務，AI 無可替代；但涉及黎曼猜想這類需要顛覆性直覺和深層概念重構的核心領域，人類的主導地位依然穩固。
正如他此前在 IPAM 會議上所言：“只要 AI 爲你節省的時間，多於你爲了糾正它而浪費的時間，它就是一款成功的工具。”此次長達 26 分鐘的無剪輯視頻，正是對這一論斷的最好背書。
在未來的數學研究中，“人機共作”或將成爲一種新常態。屆時，也許 AI 能夠以“初級合作者”的身份，徹底打通數學從直覺構想到計算機形式化驗證之間的瓶頸。
參考鏈接：
視頻地址：
https://www.youtube.com/watch?v=JHEO7cplfk8&t=124s
運營/排版：何晨龍
