AIREITER看到「Claude 解出了費馬最後定理」這個標題時，最該留意的是「形式化」三個字。Anthropic 公開了一份 Lean 產物，表示它能從頭到尾檢查這個定理；但其中採用的數學路線，仍是既有的 Frey–Serre–Ribet–Wiles–Taylor-Wiles 論證，不是 Claude 新發現的證明。
先把兩個說法分開
如果問題是 Anthropic 有沒有發布一份 Lean 4 形式化的費馬最後定理（FLT），答案是有。公開儲存庫也附上了建置與驗證說明。但若進一步說 Claude 獨立解決了這道著名難題，那就不準確了；真正帶來數學突破的是 Andrew Wiles 和 Richard Taylor，時間則在數十年前。
FLT 的內容是：當 n > 2 時，正整數不存在符合 a^n + b^n = c^n 的解。Wiles 的證明於 1995 年發表；Anthropic 這次做的，是把這條既有的證明路線轉化為可由電腦檢查的形式化產物。想了解歷史背景，可以參考 Lean Community 的 FLT 專案公告。
Lean 證明回答的問題，和非形式化論文並不相同。它可以證明：在指定環境中，某個經過精確編碼的命題，確實能由已檢查的定義、依賴項與公理推出。但它無法證明 AI 發明了背後的數學，也無法保證定理名稱真的符合其描述。
Anthropic 實際發布了什麼
Anthropic 在 2026 年 9 月 4 日的研究文章中表示，Claude 花了 11 天完成首份完整、端到端、由電腦檢查的 FLT Lean 形式化。文章提到，專案約包含 1,300 萬行 Lean、30,300 個已證明的定理陳述，其中 29,500 個用於最終證明；另外也產生了約 60 億個輸出 token。
這項工作使用了 Prove2Me。Anthropic 將它描述為一個維護定理陳述有向無環圖、並協調多個代理程式的平台。Anthropic 表示，這份形式化採用的是一條簡化版既有證明路線，相關數學工作者包括 Frey、Serre、Ribet、Wiles 與 Taylor-Wiles。
如果目的是核對這項說法，公開的 GitHub 儲存庫比研究公告更有用。它的預設目標是 FinalCheck.lean，其中的定理宣告如下：
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n儲存庫明確說明，這是一份不維護、也不接受貢獻的研究產物。它鎖定 Lean 4.33.1 與 Mathlib v4.33.0，附有 PROOF-PATH.md，也提供可離線瀏覽定理與定義依賴圖的 HTML 版本。
儲存庫的最終檢查設計成：如果證明依賴額外公理、sorry、native_decide、unsafe 或其他類似的逃生門，就應該失敗。這讓讀者能直接檢視產物，而不是只能相信截圖或文章摘要。
如何重現驗證流程
認真驗證時，第一步應該是使用儲存庫鎖定的環境，而不是把單獨的 .lean 檔案複製到另一個專案中。Lean Community 的驗證指南解釋了原因：Lean 每月發布新版本，Mathlib 也經常變動，向後相容性並沒有保證。
建置前先鎖定環境
儲存庫表示，建置預計在 Linux 或 macOS 上進行，並需要 elan、Git、Python、GNU coreutils，以及網路連線，讓 Lake 能下載並建置鎖定版本的依賴項。它估計 .lake 目錄約需 67 GB，另外還會產生約 220 GB 的 C 檔案，之後可以刪除。
儲存庫也指出，每個平行工作大約需要 5 GB 記憶體，部分模組則最多需要 36 GB。在 96 個工作執行緒下，儲存庫回報的建置時間是 5 小時 32 分鐘，記憶體峰值達 153 GB。這些是儲存庫提供的數字，不是本文實測結果；把它們當成硬體規劃上的警示，不要視為保證的執行時間。
選擇適合的驗證方式
- 只做檢視：閱讀
FinalCheck.lean、PROOF-PATH.md與ATTRIBUTION.md，不實際建置。 - 完整 Lean 建置：使用鎖定的工具鏈，執行
lake build。 - 獨立重播：成功建置並匯出後，執行 comparator 與 nanoda 腳本。
從全新的 clone 開始，儲存庫提供的基本流程如下：
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build
# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh
# Run after the comparator check.
verification/nanoda/run.sh這幾個階段各自負責不同工作：
| 階段 | 儲存庫回報的細節 | 用途 |
|---|---|---|
lake build | 60,475 個模組；回報的 96 工作執行緒建置時間為 5 小時 32 分鐘 | 從原始碼建置專案，並讓 Lean 核心檢查建置內容中的宣告 |
| Comparator | 回報的執行時間為 14 小時 46 分鐘；記憶體峰值 230 GB | 檢查公開的定理與引用的常數，是否符合預定的 Mathlib challenge 陳述 |
nanoda | 匯出後以 16 執行緒執行約 30 分鐘 | 透過一個以 Rust 撰寫、獨立實作的核心，重播匯出的環境 |
Comparator 不能取代閱讀定理陳述。它主要用來降低這種風險：專案表面上證明了某件事，實際上卻是較弱、或細節略有不同的命題。儲存庫的 PROOF-PATH.md將具名的數學步驟對應到 Lean 宣告；產生的 HTML 頁面則讓你不用啟動 Web 應用程式，也能檢視依賴關係。
儲存庫表示，第二輪檢查還有額外成本：寫入 37.8 GB 的匯出檔可能需要約 90 GB 記憶體，而 nanoda 工作流程在檢查期間可能需要約 40 GB。
證據能證明什麼，又不能證明什麼
| 證據層級 | 可以確立 | 無法確立 |
|---|---|---|
| Lean 核心建置 | 提交的證明項能在鎖定的 Lean 環境中通過型別檢查 | Claude 發現了這套數學，或非形式化說明與每個定理名稱都完全相符 |
FinalCheck.lean 與公理防護 | 儲存庫的最終定理會依照回報的公理清單進行檢查，並拒絕數種列出的捷徑 | 除非實際檢查命題本身，否則無法確定它就是歷史上的 FLT 陳述 |
#print axioms 輸出 | 在預期檢查通過時，依賴項包含 Lean 標準的 propext、Classical.choice 與 Quot.sound，而不是隱藏的使用者自訂公理 | 整個軟體供應鏈都已經過獨立驗證 |
| Comparator | 已證明結果與引用的常數，符合儲存庫使用的 Mathlib-only challenge | 專案中的每段自然語言描述都清楚，或具備足夠的教學性 |
| nanoda 重播 | 匯出的環境可被另一個以 Rust 撰寫的 Lean 核心實作接受 | 匯出檔、腳本或作業系統不存在任何可能的錯誤 |
PROOF-PATH.md 與出處資訊 | 提供人類檢視數學對應關係與既有來源的路徑 | 機器產生的定理名稱無須人工審查，就一定能準確描述其陳述 |
Lean Community 的「Did you prove it?」檢查清單提出一項關鍵原則：編譯能驗證的是編碼後的命題，而不是定理名稱是否符合原本想表達的非形式化主張。對這份產物來說，comparator 及其對 Mathlib 的運用降低了這項風險，但仍不能免除閱讀定理宣告與證明路徑的必要。
這份產物展現了什麼，又沒有展現什麼
這套系統確實產生了一份規模異常龐大的 Lean 形式化產物，而且通過了正式檢查。但它沒有展示新的 FLT 證明路線、新的初等證明，也不能證明 Claude 進行了獨立的數學發現。
Anthropic 表示，這份證明採用 Wiles 路線的簡化版本。儲存庫也列出了既有工作的貢獻：其中的 ATTRIBUTION.md指出，有 106 個檔案包含來自倫敦帝國學院 FLT 專案或 flt-regular 的內容，此外也使用了 Mathlib。要準確描述這份發布的產物，就不能忽略這些來源。
專案回報在執行期間證明了 30,300 個定理陳述，其中約 29,500 個用於最終證明；儲存庫則描述了 29,511 個定理頁面。這些是形式化宣告與依賴項，不是 29,511 個新發現的數學結果。形式化證明必須明確展開人類證明可以交給專家默會理解的隱含步驟、型別、強制轉換、定義與函式庫依賴。
儲存庫表示，這些來源檔案的首要目的不是供人閱讀，而是通過檢查：名稱由機器產生，像 P2M 這類標籤只是流程標記，真正有權威的是陳述本身，而不是名稱。這也正是證明路徑與 comparator 和標題中的定理同樣重要的原因。
更早期的 Lean 工作，也不應被混同於 2026 年這項說法。一篇2023 年關於正則質數之費馬最後定理的論文，回報已完整、無 sorry 地形式化 Kummer 定理在正則質數情況下的 Case I，同時指出 Case II 與 Kummer 引理仍需要大量工作。一篇2025 年修訂版則將正則質數形式化描述為該較窄情況的完整證明。
| 工作 | 範圍 | 實際角色 |
|---|---|---|
flt-regular 研究 | 正則質數結果，以及支援代數數論的基礎設施 | 較早期的形式化建構基礎與來源材料 |
| Imperial FLT 專案 | 圍繞 FLT 的現代數論長期、可重用形式化 | 函式庫與協作基礎設施 |
| Anthropic 儲存庫 | 宣稱以 Lean 4 完成端到端 FLT 定理，並附建置與重播檢查 | 以通過檢查的結果為優先、而非長期維護的大型研究產物 |
Imperial/Lean FLT 專案將形式化現代數論描述為更廣泛的基礎設施工作，而不只是翻譯一條定理。Anthropic 的發布，較適合被理解為：它補充展示了協調多個 AI 代理程式在既有形式化生態系中能做到什麼，而不是證明早期專案的目標已經不再重要。
不同問題，應該相信哪些證據
| 如果你想知道…… | 負責任的答案是…… | 下一步 |
|---|---|---|
| Anthropic 是否真的發布了產物 | 是；有官方公告，也有公開且鎖定版本的儲存庫 | 把研究文章與儲存庫一起閱讀 |
| 編碼後的定理是否就是 FLT | 儲存庫提供了具體的定理宣告、comparator 與證明路徑 | 檢查 FinalCheck.lean、comparator 與 PROOF-PATH.md |
| 程式碼是否能乾淨建置 | 儲存庫記錄了從零開始的建置流程，也回報了自己的結果 | 如果硬體符合要求，使用 Lean 4.33.1 與 Mathlib v4.33.0 重新建置 |
| Claude 是否發明了新的證明 | 沒有證據支持這種描述；採用的是既有的 Wiles/Taylor-Wiles 數學 | 將它描述為 AI 輔助的形式化或證明工程 |
| 這份產物是否容易維護 | 不容易；儲存庫明確稱其不受維護，程式碼也由機器產生 | 把它視為研究產物，而不是可直接放進 Mathlib 的函式庫 |
| 這是否證明 AI 已具備一般性的數學自主性 | 不是；它展示的是 AI 在高度規格化的形式化目標上，搭配大量基礎支援時的表現 | 把形式驗證能力與開放式定理發現分開評估 |
如果你只想了解新聞，官方發布與儲存庫已足以證明這個專案確實存在。如果你要進行稽核，就重現鎖定版本的建置並檢查命題。如果你是在評估 AI 研究，還應把協調機制、既有函式庫、先前的形式化工作與運算資源，都納入對整個系統的評估。
常見問題
Claude 發現了費馬最後定理的新證明嗎？
沒有。Anthropic 的產物形式化的是一條與 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 相關的既有證明路線。這項成果的重點在於，以異常的規模與速度產生可由機器檢查的 Lean 產物，而不是提出新的數學解法。
Lean 建置成功，就代表非形式化定理已經被證明嗎？
它證明的是：在該 Lean 環境中，編碼後的命題可以由經過檢查的依賴項推出。你仍然必須確認這個命題及其定義，確實對應到你想宣稱的非形式化定理。
儲存庫有使用 sorry 或額外公理嗎？
儲存庫表示，最終檢查會拒絕 sorry、額外公理、native_decide、unsafe 以及數種相關捷徑。它預期的公理清單是 Lean 的三個標準公理：propext、Classical.choice 與 Quot.sound；請自行重現檢查，不要只依賴公告內容。
一般筆電能重現這項結果嗎？
你或許可以檢視儲存庫，或完成部分建置，但完整驗證並不是一般筆電能輕鬆處理的工作。儲存庫回報建置時的記憶體峰值為 153 GB，comparator 最多達 230 GB，磁碟需求也很高，因此硬體是主要限制。
如果要準確核對這項說法，請先從鎖定版本的 GitHub 產物開始，先讀定理宣告再看標題，並將成果描述為一份大規模、由 AI 輔助完成的既有數學形式化。