Claude花11天「證明」費瑪最後定理，1300萬行程式碼做了哪些事？

可能有些人已經知道這件事了，不過我們還是用白話文跟大家說一下好了，費瑪最後定理是個幾百年的人類智慧結晶，他值得我們給他一個篇幅。

Anthropic 上禮拜公布一件事:他們的 Claude 花了 11 天,完成費瑪最後定理第一個「電腦可驗證」的完整證明。標題聽起來像是 AI 解開三百多年的數學謎題,但先說，這件事不是「AI 證明了什麼新東西」，是「AI 把一個人類早就證明過的東西，翻譯成電腦看得懂、驗證得了的語言」。這兩件事差很多，搞懂差在哪，才知道這件事真正厲害在哪裡。

先講清楚：證明的人不是 Claude

費瑪最後定理 1637 年由費瑪提出:當 n 大於 2,不存在正整數 a、b、c 讓 aⁿ+bⁿ=cⁿ 成立。真正把這個定理證出來的,是英國數學家安德魯·懷爾斯,1995 年發表,證明本身厚達 129 頁,耗掉他七年的時間。

Claude 是把懷爾斯這份 129 頁的人類證明,翻譯成 Lean 這套「形式化證明語言」寫出來的程式碼——每一步推理都要拆到電腦可以逐行檢查、無法用直覺矇混過去的地步。這個過程叫「形式化」——把已經存在的證明,翻譯成電腦看得懂的語言,不是重新發現一次證明。

這個區分不是我在挑語病。判斷一件事有多厲害,起點必須先搞清楚它到底做了什麼——把「翻譯」講成「證明」,是把兩種完全不同難度的工作混為一談。

先講，光寫程式就花了11天。

規模數字攤開來看

Claude 這次的產出:1,300 萬行 Lean 程式碼,是 Lean 社群最大公開數學庫 Mathlib 全部程式碼量的五倍以上。過程中證明了 30,300 個中間定理,最後有 29,500 個被用進最終證明裡。整個過程消耗大約 60 億個輸出 token,人類這邊只做高層次的方向指導,不用逐行盯著寫。

整個工作靠多個 Claude 智能體協同分工完成,沒有單一個模型從頭寫到尾:有的負責定義概念,有的負責證明中間定理,有的負責處理更複雜的命題推導,彼此用一張「有向無環圖」管理定理之間誰依賴誰,確保拼起來的時候邏輯順序是對的。整個工作是在哥倫比亞大學設計的 Prove2Me 協作平台上完成。

這件事為什麼值得認真看

數學界對這件事的反應,比新聞標題謹慎。形式化數學圈的指標人物 Kevin Buzzard 稱這是「了不起的自動形式化成就」,證明過程只用到數學公理本身,沒有任何隱藏假設。但也有聲音提醒:費瑪最後定理在 Lean 裡的形式化,原本就是一個持續進行中的社群計畫(最知名的是帝國理工學院 Buzzard 主持的專案),Claude 這次的產出是接上這條長期工程,站在一整個社群已經蓋了好幾年的地基上,做的是把最後、也是最龐大的一段搭完。

這仍然是真本事——把 60 億 token 的推理組織成 1300 萬行邏輯自洽、電腦能逐行驗證的程式碼,一般模型做不到這個規模。只是「Claude 一個人從頭解出費瑪最後定理」這種論述,把它的貢獻誇大了一層。

Anthropic 自己講的重點,其實不是「我們解出了難題」,是「形式化可以解決一個更實際的問題」:數學論文的審查,現在常常要耗上好幾年,因為審稿人得自己一步步驗證每個推理有沒有漏洞。形式化把這件事變成電腦可以自動檢查的工作——這對維護整個數學知識體系的可信度,尤其在 AI 也開始產出數學結果的時代,是個實際的護城河做法。