Anthropic 表示，其 Claude AI 已產出費馬大定理的首個完整電腦檢驗證明，在 11 天內幾乎獨立完成這項工作，並寫下迄今最長的數學證明。

倫敦帝國學院的一個由人類主導的專案自 2024 年起一直在進行完全相同的任務，且尚未接近完成。Claude 搶先抵達終點。領導該帝國學院專案的數學家 Kevin Buzzard 審查了 Claude 的證明，並確認它僅使用數學最基本的邏輯規則便能成立。

據 Anthropic 稱，Claude 寫下了有史以來最長的數學證明，並用它正式證明了困擾數學家 358 年的費馬大定理。這個 AI 在 11 天內、大多獨立完成，產出 1,300 萬行程式碼，可由電腦逐行檢驗，而無須依賴數學家的片面之詞。

費馬大定理指出，不存在三個正整數，在各自取高於 2 的冪之後，前兩者之和等於第三者。Pierre de Fermat 於 1637 年將這一主張匆匆寫在一本數學書的頁邊，並聲稱自己有一個「真正絕妙的證明」，只是頁邊太窄寫不下。隨後他便去世了。此後 358 年間，數學家不斷嘗試重建他當年所想的證明。

證明與驗證是兩回事

數學證明是一連串邏輯步驟，只要其中一環斷裂，整個證明便告崩塌。要在上百頁的密集論證中找出那一個斷裂的環節，可能耗費其他數學家數年的光陰。

將證明形式化，意指將其轉換成一種極度字面的語言，讓電腦能自行驗證每一步，而不涉及任何主觀判斷。

數學家在驗證方面的困境由來已久。1908 年的一項德國獎項——以今日幣值約 100 萬至 200 萬美元，用於獎勵該定理的首個有效證明——僅第一年就收到 621 份錯誤的提交。

正如 Anthropic 在 X 上所寫：

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

真正的證明直到 1995 年才問世，出自英國數學家 Andrew Wiles 之手，而且過程一波三折。Wiles 於 1993 年 6 月透過三場演講公布其解法，隨後卻被審查者發現漏洞。他與昔日學生 Richard Taylor 花了將近一年時間修補，一度瀕臨放棄，最終於 1995 年 5 月發表修正後的 129 頁證明。該證明依賴的數學工具在費馬的時代並不存在，這也是數學家如今懷疑費馬本人的「絕妙證明」是否真正成立的主要原因。

電腦驗證的數學本身已有數十年歷史。最早著名的案例是 1976 年借助電腦完成的四色定理證明，引發了關於「無法由人類完整閱讀的證明是否算數」的長期爭論。Lean 等形式化證明語言——由最初任職於 Microsoft Research 的 Leonardo de Moura 創建——正是源自這種張力，讓軟體承擔檢驗工作，使人類仍能信任結果。

2024 年，倫敦帝國學院數學家 Kevin Buzzard 啟動了一個專案，目標正是 Claude 剛完成的工作：將 Wiles 的證明轉換為電腦可檢驗的 Lean 語言。這類工作需要一大群志願數學家——該專案的綱要本身就有 86 頁，且經費已確保至 2029 年。Claude 在 11 天內完成了全部工作。

Claude 究竟如何做到

Anthropic 在一篇更深入的文章中解釋，在哥倫比亞大學帶領團隊開發 AI 形式化工具的 Tianyi Peng 決定測試 Claude 獨立完成的能力。數十個 Claude 智能體並行工作，撰寫定義、證明小型結果，再將其堆疊成更大的成果，人為介入幾乎僅限於偶爾的提示，例如「下一步優先處理這個定理」。

起初進行得並不順利。早期，這些智能體經常忘記自己已證明過的內容並停止協作；這些錯誤的嘗試仍佔最終證明約 7% 的行數。

解決問題的關鍵是由 Peng 團隊開發的工具 Prove2Me，它為每個智能體提供相同的即時待辦清單，列出仍待完成的小型證明，避免重複工作或偏離方向。它還整理檔案結構以加快 Lean 的檢驗速度，並為每個結果保留淺白的英文筆記，讓智能體能複用彼此的成果而非重複造輪子。

完成時，Claude 已證明超過 30,000 個輔助定理，消耗了數十億個 token，所用的是 Anthropic 稱大致相當於 Claude Fable 5.1 的研究模型——即該公司後來向公眾發布的版本。最終證明長達 1,300 萬行——是數學家在此類工作中使用的共享庫 Mathlib 的五倍以上。

一部典型小說約 8 萬字。Claude 的證明相當於 160 部純邏輯論證的小說。

這真的重要嗎？

Buzzard——他自己的專案版本仍獲資助至 2029 年——審查了 Claude 的證明並予以認可，表示該證明「除數學公理外不依賴任何假設」地證明了這一定理。

這並不等同於 Claude 發現了全新的數學——Anthropic 今年稍早也曾以其密碼學研究提出類似主張。Wiles 早在三十年前就證明了費馬大定理——Claude 只是為其建立了一份可供機器檢驗的憑證。這一點之所以重要，是因為數學家正日益被未經驗證的證明（包括 AI 撰寫的證明）淹沒，其出現速度已超出人類手工查驗的能力。此外，這類形式化證明是確定性的，不易出現人為錯誤，這在數學中極為重要。

這並非新問題。克卜勒猜想的電腦輔助證明耗時四年，審查小組最終只願承諾「99% 確定」；Grigori Perelman 對龐加萊猜想的證明，也花了差不多同樣長的時間才被完全消化。

如果不願盡信 Anthropic 的說法，也無須如此。這份完整的 1,300 萬行證明目前就在 GitHub 上，任何有足夠閒暇的數學家都可以免費逐行檢視拆解。