費馬說頁邊太窄，Claude 用 11 天寫成 1300 萬行程式碼
1637 年前後，法國律師費馬在丟番圖《算術》一書的頁邊留下一句註記：他發現了一個真正美妙的證明，可惜頁邊太窄，寫不下。這句話後來成了數學史上被引用次數最多的「下次再說」。
據 IT之家等公開報導，Anthropic 於當地時間 2026 年 9 月 4 日宣布（官方公告）：旗下模型 Claude 在基本自主運行 11 天後，完成費馬大定理首個端到端、經電腦檢查的形式化證明。頁邊確實太窄，這回寫下的是約 1300 萬行程式碼。
同一週的 AI 版面並不冷清。Meta 剛發表了會反問、會求助的 Muse Spark 1.3，把模型的新人守則寫成話題；Anthropic 端上桌的，則是一道 389 歲的老題目。
頁邊太窄，一窄就是三百多年
先把這樁懸案的規格交代清楚。費馬大定理可以用一行話說完：當整數指數 n 大於 2 時，不存在滿足 aⁿ+bⁿ=cⁿ 的正整數 a、b、c。題目中學生都看得懂，答案人類找了三百多年，這組反差是它跨越幾個世代的原因。
挑戰者絡繹於途。歐拉先啃下 n=3 的情形，庫默爾為此打造的工具把代數數論推進了一個時代，每個名字都替後人墊了磚，完整的證明始終缺一角。至於費馬自己有沒有那個「美妙的證明」，以十七世紀的工具回頭看，答案多半是沒有。
它也早早住進了大眾文化。《辛普森家庭》的編劇室裡藏著好幾位數學出身的寫手，曾在荷馬的黑板上寫下一個幾乎成立的反例等式，誤差小到尋常計算機顯示不出來；《銀河飛龍》某集裡，畢卡艦長還在感嘆這道題到了二十四世紀依然無解。一條定理能被動畫與影集輪流致敬，本身就是稀有物種。
1995 年，人類版本收尾
時間軸快轉到 1993 年 6 月。英國數學家安德魯·懷爾斯在劍橋的艾薩克·牛頓研究所連講三場，最後一句話只有「我想我就停在這裡」。臺下心領神會：三百五十六年的懸案收尾了。
劇情隨即拐彎。同儕審查階段，證明被查出缺口，數學界盯著這份手稿又熬了一年多；懷爾斯與理查·泰勒在 1994 年補上最後一環，論文於 1995 年正式刊出，全長 129 頁。依 Anthropic 公告中的說法，這份證明在發表之前，還經歷了數個月的人工核查。
129 頁的人類證明，配上數個月的同行檢查，這是二十世紀頂級數學的驗收規格。人讀得懂的數學，驗證起來就是這個價碼。
電腦蓋章的那 11 天
2026 年 9 月，規格換了一套。依 Anthropic 公告，Claude 生成了約 1300 萬行 Lean 程式碼，證明約 3.03 萬個定理，其中約 2.95 萬個中間定理被納入最終的完整證明；整份證明由 Lean 逐行檢查，全程只用了 Lean 的 3 條標準公理。路線上，它遵循 Darmon、Diamond 與 Taylor 對懷爾斯證明的簡化版本。有個漂亮的銜接是：簡化版作者之一的泰勒，當年正是幫懷爾斯補洞的那位合作者。
先說明 Lean 的身分：一種證明助手。數學家把證明寫成它認得的語言，它逐步檢查每一步邏輯，合格才放行。人類寫數學習慣省略「顯而易見」的步驟，也習慣引用尚未形式化的既有成果；Lean 不喫這兩套默契，每一環都要求攤開。正因如此，形式化向來以年為單位計價，Anthropic 自己原先的估計，這項工作可能要花上數年。
這次的人機分工也寫在公告裡：人類研究員給出少量高層次指令，例如排定某些數學物件或定理的優先順序；概念定義、中間定理與複雜命題的推導，交給多個 Claude 智慧體並行處理。專案發起人是 Anthropic 研究員 Tianyi Peng，2017 年自清華大學姚班本科畢業，2023 年取得 MIT 博士學位，學生時代拿過全國青少年資訊奧林匹克競賽選拔賽第八名，現任哥倫比亞大學助理教授。團隊使用他與哥大合作者開發的 Prove2Me 平臺，以有向無環圖記錄待證定理與依賴關係，讓多個智慧體各自認領題目。
帳面上另有兩個數字。整個專案消耗約 60 億個輸出 Token，使用的是一個與 Claude Fable 5.1 大致相當的通用內部研究模型；產出的證明規模，超過主要數學證明庫 Mathlib 的 5 倍。完整 Lean 證明已公開在 GitHub，任何人都能下載檢查。Token 這個詞今年的行情，可以從另一條新聞側面看出：它已經被寫上銀行貨架，成為一款抵押品從廠房換成詞元的Token 貸。
它翻譯了證明，數學還是 1995 年的
Anthropic 把界線畫得很清楚：這項工作並未重新發現費馬大定理的證明。Claude 做的是翻譯，把懷爾斯 1995 年的論證，轉成機器可以逐行驗證的語言。定理的功勞屬於 1990 年代的人類，自動化的部分屬於這 11 天。
打個比方，同一份作業有兩種批改方式。懷爾斯交 129 頁的論述，批改的是人，需要數個月；Claude 交 1300 萬行的形式化版本，批改的是程式，跑完就是跑完。形式化的價值在於，驗收一份頂級證明，從動員少數專家，變成執行一段程式。
倫敦帝國學院的數學家 Kevin Buzzard 審閱了這份證明。依 Anthropic 公告轉述，他的評語是：這項自動形式化成果顯示，AI 輔助形式化大型數學成果已經取得重要進展。
圍觀的人在看什麼
這則新聞好讀的地方，在於數字自己會講話。那句「頁邊太窄」被引用了將近四百年，如今有人用 1300 萬行把頁邊徹底鋪滿；懷爾斯閉門七年、修補一年才把證明交出去，Claude 跑了 11 天、燒掉約 60 億個 Token。兩組數字擺在一起，沒有人會弄混誰在證明、誰在驗核，只是那個「11」很難不多看兩眼。
再往深一層看，公眾對這則新聞的胃口，和「驗證」這件事的處境有關。這幾年從學界到內容平臺，人人都在重問：誰說的、能不能查。數學把問題推到極端，連教科書等級的定理，驗收也曾以年月計。一份任何人都能下載、由程式逐行蓋章的證明，剛好回應了這種集體的核對需求。
形式化圈子裡的人倒是不意外。Mathlib 這些年一磚一瓦地累積，陶哲軒也多次公開示範 AI 搭配 Lean 的工作流程；意外的是規模，一份原本以年計的工程被壓進 11 天，產出比整個 Mathlib 還大上數倍的證明體量。
驗證變便宜之後
Anthropic 對下一步的設想寫得節制：如果這類自動形式化能擴展到更多現代數學成果，驗證新證明的人工成本就有機會下降；當 AI 生成的數學越來越多，在供人閱讀的版本旁邊附一份機器可查的副本，未來或許會成為慣例。
費馬那句頁邊太窄，是謙虛、拖延，還是數學史上最成功的一次懸念經營，沒有標準答案。可以確定的是，這道題目把每個時代的書寫工具都用過一遍：1637 年的鵝毛筆寫不下，1995 年寫成了 129 頁，2026 年，輪到 GitHub 上人人可下載的倉庫把答案攤開。
至於新的問題只有一個：當驗證不再需要動員一個學界，省下來的時間會拿去追下一個費馬，還是去下一本書的頁邊，再留一句寫不下的話？