1,300 萬行 Lean 程式碼：Claude 寫出費馬最後定理首個機器驗證證明

大約西元 1637 年，皮耶・德・費馬（Pierre de Fermat）在丟番圖《算術》的頁邊寫下一個主張：不存在正整數 a、b、c，在 n > 2 時滿足 aⁿ + bⁿ = cⁿ。他還補了一句讓後世數學家咬牙切齒的話 —— 他已經發現一個「真正了不起的證明」，可惜頁邊太窄寫不下。人類直到 1995 年才由安德魯・懷爾斯（Andrew Wiles）以 129 頁的論文解決這個問題。如今，Anthropic 宣布其 AI 模型 Claude 完成了人類與機器都不曾做到的事：費馬最後定理的第一個完整、端到端、經電腦驗證的形式化證明，而且是在 11 天內以近乎全自主的方式、用 Lean 證明語言寫成。

官方宣布了什麼

Anthropic 在名為「Formalizing Fermat’s Last Theorem」的研究文章中，描述了這個他們稱之為首個完整機器驗證證明的成果。Claude 寫下約 1,300 萬行 Lean 程式碼，途中證明了 29,500 個中間定理，整個過程消耗約 60 億個輸出 token，使用的是一個 Anthropic 表示「大致相當於 Claude Fable 5.1」的通用內部研究模型。

這裡的區別很重要、也很容易被誤解。Claude 並沒有「發現」費馬最後定理的新證明 —— 證明的數學內容沿用懷爾斯的路線，改編自 Darmon、Diamond 與 Taylor 的精簡闡述，並沿用帝國學院 FLT 專案的部分成果。Claude 做的事，從另一個角度來看或許更難：它把一大片抽象數學翻譯成嚴謹到讓電腦能逐步驗證的形式語言。Lean 證明檢查器完成了這件事，最終成品只依賴 Lean 的三條標準公理。另一個比較器（comparator）也確認定理敘述與 Mathlib 對 FLT 的敘述完全一致，堵住了「證明了另一個相似但不同的命題」這個漏洞。

規模感：形式化 FLT 原本被認為是多年的工程。數學社群用來描述專案初始階段的藍圖，本身就有 86 頁。

11 天的攻堅過程

整個專案由 Tianyi Peng 主導 —— 這位 Anthropic 研究員在哥倫比亞大學的團隊專門打造 AI 形式化工具，這次搭配的是以 Claude Code 為基礎的多代理人架構。最關鍵的元素是 Prove2Me，一個由 Peng 與其合作者設計的開放數學形式化協作平台。Prove2Me 維護一張定理敘述的有向無環圖（DAG），讓代理人據以決定下一步該攻哪個證明；它把定理敘述與證明拆成不同檔案以加速 Lean 編譯，並為每個敘述保留自然語言描述，簡化證明路徑。

最早的嘗試失敗得很有教育意義。初期的代理人有階段性進展，但很快失去對專案狀態的掌握、無法有效協作；這些被捨棄的工作仍佔最終證明非樣板程式碼的約 7%。人類的介入刻意保持在最低限度 —— Peng 只給了零星的高層指示，例如「Jacobian as a scheme 聽起來優先級很高」、「儘快把 Mazur 定理做完」。

Anthropic 公開的 Claude 思考節錄，讀來意外地有人味。當最後幾塊拼圖歸位時，代理人自己寫下：「🏁🏁🏁 The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.」（FLT 根節點在 prove2me 上顯示已證明。此一戰役的歷史性時刻。）

為什麼「形式化」才是真正的新聞

查核一個數學證明，不像按計算機那麼簡單。證明是一長串推理鏈，只要一個環節斷裂，下游的一切可能悄然失效。懷爾斯 1995 年的論文花了數個月才通過審查；1908 年的沃夫斯凱爾獎（10 萬德國金馬克，約今日 100 至 200 萬美元）光是第一年就湧入 621 個宣稱的證明，幾乎全錯。形式化承諾把這種驗證負擔從「數個月的專家勞動」壓縮成「機器時間」—— 但在此之前，形式化本身的成本高得驚人。這正是 Jan Bergstra 提出形式化懷爾斯證明後沉寂十年的原因，也是 Kevin Buzzard 2024 年發起的社群專案以多年為期規劃的原因。

Buzzard —— 帝國學院數學家、該社群專案的領導者 —— 審閱了 Claude 的證明後說得直白：「如果現在連 FLT 都能自動形式化，那我們已朝自動形式化整個現代數學文獻跨出一大步。這類自動形式化技術將催生新工具，挖出現有數學知識體系裡的錯誤，並減輕審查者的負擔。」

他這段話的另一半，指向 AI 時代的真正利害：形式化正是人類能對 AI 產生的數學建立信心的途徑 —— 目前這類驗證倚賴極其昂貴的人工審查。當模型產出的「宣稱證明」比以往任何時候都多，一份機器可查核的正確性保證，就是「有趣的說法」與「已定案的數學」之間的分界線。

從前沿實驗室到消費級訂閱

整篇公告中最發人深省的細節，或許是一個小型後續實驗。Anthropic 研究員用了三個個人 Claude Max 訂閱 —— 消費級方案，而非前沿實驗室的運算叢集 —— 來形式化 Hardy–Littlewood 圓法的應用。代理人完全透過 Prove2Me 協作，三天內完成了 Vinogradov 三質數定理的形式化。Anthropic 的結論是：只要鷹架正確，用一般消費級訂閱協作形式化重大結果是可行的。該公司也表示已擴大對純數學與形式化領域數學家的免費與折扣訂閱及研究點數。

當然也有誠實的但書。整個過程消耗了 60 億個 token —— 即使成品是有史以來最大的 Lean 證明，以前沿研究的標準而言仍然極耗 token。所用模型是「大致相當於」正式產品的內部研究模型，並非人人可用的能力。而且形式化一個 1995 年的證明，無論多宏偉，與產生全新數學仍是兩回事。

但方向已經很清楚。形式數學社群以「年」為單位規劃的里程碑，在十一天內倒下；同一套技術堆疊，用消費級方案在三天內重現了一個解析數論的經典結果。正如 Anthropic 所言，形式化是他們「對 AI 的角色感到毫無保留地正面」的領域 —— 一個既能抓出人類數學知識體系錯誤、又能讓機器產生的數學終於可被驗證的工具。費馬的頁邊對他的證明而言太窄；Claude 的證明，恐怕塞不進他整座圖書館。