Claude以Lean形式化費馬最後定理,11天寫出1300萬行證明

Anthropic於2026年9月4日宣布,其人工智慧Claude完成了費馬最後定理的第一個從頭到尾都能由電腦驗證的證明。該定理指出,當整數n大於2時,不存在能滿足a^n+b^n=c^n的正整數a、b、c。數學家安德魯·懷爾斯於1995年發表了長達129頁的證明,三十多年來,始終沒有人對其邏輯進行過完整的機器驗證。Claude在近乎自主的狀態下工作了11天,以證明助理系統Lean寫下約1300萬行程式碼。

這項計畫由Anthropic研究員、專注於AI數學形式化研究的彭天翼(Tianyi Peng)主導。過程中,Claude以電腦可驗證的形式證明了約3萬300條中間定理,其中約2萬9500條實際用於最終證明。產出的程式碼量超過Lean社群數學函式庫Mathlib的5倍以上。數十個Claude代理程式並行工作,分別定義概念、證明中間定理,再逐步挑戰更困難的命題。最初的嘗試曾多次失敗:各代理程式逐漸失去對專案整體進度的掌握,無法有效重複利用彼此的成果。最終證明中約7%的非樣板程式碼,正是來自這些失敗的嘗試。

什麼是電腦驗證的形式證明

面向人類讀者撰寫的數學論文,往往會省略被視為「顯而易見」的步驟。但像Lean這樣的證明助理系統做不到這一點:無論多麼瑣碎的步驟都必須完整寫出。將既有證明改寫成這種形式的工作,稱為「形式化」。由於邏輯鏈中只要有一處斷裂,後續所有結論都可能失效,一份形式化證明唯有通過Lean的機器檢查後,才能獲得不依賴人工複核的正確性保證。Claude的證明僅依賴Lean的三條標準公理,完全沒有使用「sorry」——那個能讓某個步驟暫時跳過不證的佔位符。一項比對工具確認了Claude所證明的命題,與Mathlib本身對費馬最後定理的敘述完全一致;而一個以Rust獨立寫成的Lean核心「nanoda」,也對超過100萬條宣告進行了零錯誤的檢驗。

為何費馬最後定理是如此具代表性的案例

這個定理得名於法國數學家皮埃爾·德·費馬,約在1637年於丟番圖《算術》一書的頁緣寫下的一句話:他聲稱發現了「一個真正美妙的證明」,卻表示頁緣太窄寫不下。此後350多年間,一代又一代數學家苦尋這個證明卻始終未果。1908年,有人懸賞一筆相當於今日一、兩百萬美元的獎金,徵求正確證明,光是第一年就收到621份錯誤的證明。1993年6月,安德魯·懷爾斯在為期三天的系列演講中宣布了自己的證明,但約兩個月後,一位審查者在複核過程中發現了一個關鍵漏洞。懷爾斯與他過去的學生理查·泰勒花了近一年時間才修正這個漏洞,並於1995年5月發表最終版本——長達129頁,數學界花了數月才完成驗證。對國際讀者而言值得一提的是,支撐懷爾斯證明的谷山-志村猜想,正是由日本數學家谷山豐與志村五郎在1950年代提出的。而Claude這次形式化的,是達爾蒙(Darmon)、戴蒙德(Diamond)與泰勒(Taylor)提出的懷爾斯證明簡化版本。

這項非凡的自動形式化成果,據Anthropic研究人員表示僅花了11天,在不需要任何超出數學公理的額外假設下證明了費馬最後定理。過程中,我們見到了代數、調和分析、幾何與數論的自動形式化,也了解到AI產出的自動形式化成果如今已足夠穩健,可以在其基礎上繼續建構——這份證明是多層次的。

• 工作時長:11天,大部分自主完成
• 產出的Lean程式碼:約1300萬行,超過Mathlib的5倍以上
• 證明的定理數量:約3萬300條,其中2萬9500條用於最終證明
• 消耗的輸出token數:約60億,使用與Claude Fable 5.1相當的通用研究模型
• 所依賴的公理:僅Lean的3條標準公理,零使用「sorry」

Claude究竟做了什麼,又有哪些侷限

必須釐清的是,Claude並不是獨自「發現」了懷爾斯的原始證明。數學推理本身是懷爾斯與其合作者在1995年建立起來的;Claude所做的,是把這套推理的簡化版本改寫成Lean能夠驗證的嚴謹符號形式,再交由電腦進行機械檢查——這是「形式化」,而不是「發現」。這與近期AI在黎曼猜想上的研究性質不同,後者是為了產出真正嶄新的數學成果。Anthropic明確表示,這項工作的創新之處在於驗證,而非發現。整個計畫仰賴由彭天翼開發的數學形式化協作平台Prove2Me,該平台以有向無環圖管理各定理間的依賴關係,讓多個Claude代理程式能知道接下來該挑戰哪條定理。人類的介入僅限於彭天翼給出的高層次指示,例如「應優先處理作為概形的雅可比簇」。

隨著AI能產出愈來愈多數學證明,由人工逐一核驗的負擔也隨之加重。Anthropic預期,未來在面向人類讀者的論文之外,同時提供一份可由電腦驗證的形式化證明,將變得愈來愈普遍。自2024年起在帝國理工學院主導一項多年期社群計畫、以Lean形式化費馬最後定理的凱文·巴澤德(光是計畫初期的工作藍圖就已達86頁),稱這項成果是邁向現代數學文獻自動形式化的重要一步:它有助於揪出既有數學體系中的錯誤、減輕審稿人的負擔,並能夠嚴謹核驗由AI產出的數學內容。

對台灣的科技產業而言,這件事的意義不僅止於一次數學上的壯舉。用來驗證這個定理的證明助理系統,同樣已被用於驗證密碼協定、編譯器正確性,以及航太與晶片設計等領域的關鍵程式碼——而形式驗證正是台灣半導體產業長期仰賴的把關工具之一,用來確保晶片電路設計在量產前不出錯。一個AI代理程式能在數天內、而非數年內產出數百萬行經機器核驗的證明,是一個具體訊號:長期以來被視為過於緩慢、過於專精而難以規模化的形式驗證,或許會變得更容易被純數學領域以外的工程團隊採用——前提是,正如Anthropic自己所強調的,這種驗證能力絕不能被誤認為是自主發現新數學的能力。