近日，菲爾茲獎得主、加州大學洛杉磯分校（UCLA）數學系教授陶哲軒在 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 的行動發散空間。
一、搭建骨架
流程初期，陶哲軒指令 Claude Code 先不要急於推導，而是用 Lean 系統中的佔位符「sorry」搭建起整個證明的宏觀框架。這一步進行得異常順利，AI 準確識別了非形式化證明中的邏輯斷點，並將其轉化為 Lean 程式碼結構。陶哲軒指出，讓 AI 先寫出帶有「sorry」的骨架，隨後再逐一填補，是目前最高效的人機協作模式。
二、陷入泥潭與人工干預
然而，在具體填補 Lemma 1 的證明細節時，Claude Code 的短板開始顯現。由於 Lean 的底層邏輯要求高度嚴謹，AI 在面對非形式化語言中的等式代換時，表現出「過度思考」的傾向。它試圖頻繁展開底層的數學定義，而不是機械地按照人類給出的步驟進行推演。
在影片中，AI 在背景進行了大量的回溯和自我試錯，消耗了大量計算資源，推導過程變得異常冗長。在這個過程中，陶哲軒的工作站甚至意外當機了一次。系統恢復後，面對 AI 將簡單步驟複雜化的窘境，陶哲軒果斷選擇人工介入。他直接接管了鍵盤，迅速輸入了一個基於 congr（同餘/等式替換）指令的策略，瞬間突破了僵局。
他客觀評價道：「過度依賴工具可能會讓你失去對證明的直覺。當 AI 陷入死胡同時，人類直接上手往往比等待它糾錯要快得多。」
三、演化出「並行工作流」
隨著進程推進到 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 進行的演示，恰恰是連接上述「前沿探索」與「日常實踐」的橋樑。雖然不如 Google AlphaProof 解出國際數學奧林匹亞（IMO）難題那般具有極高的公眾戲劇性，但在 Lean 這一類型論保障的確定性環境中，陶哲軒的演示更為接地氣，也更貼近當代數學家真實的研究常態。
當然，在肯定 AI 帶來的效率革命的同時，陶哲軒及其代表的數學界並未迴避技術現存的局限性。
一方面，學術界有聲音擔憂，高度依賴 AI 生成的證明可能會引入「黑箱化」問題。即便 Lean 編譯器能夠從邏輯底層保證程式碼 100% 的正確性，但長篇累牘、由機器生成的機器語言缺乏人類數學特有的直覺美感和可讀性，這可能導致數學從一門「理解的藝術」異化為單純的「符號驗證」。
對此，陶哲軒保持了科學家特有的客觀與中立。他傾向於將 AI 定義為一種強大的「實驗數學」工具。對於高度依賴計算和模式匹配的任務，AI 無可替代；但涉及黎曼猜想這類需要顛覆性直覺和深層概念重構的核心領域，人類的主導地位依然穩固。
正如他此前在 IPAM 會議上所言：「只要 AI 為你節省的時間，多於你為了糾正它而浪費的時間，它就是一款成功的工具。」此次長達 26 分鐘的無剪輯影片，正是對這一論斷的最好背書。
在未來的數學研究中，「人機共作」或將成為一種新常態。屆時，也許 AI 能夠以「初級合作者」的身份，徹底打通數學從直覺構想到電腦形式化驗證之間的瓶頸。
參考連結：
影片網址：https://www.youtube.com/watch?v=JHEO7cplfk8&t=124s
營運/排版：何晨龍