Anthropic Claude 11 日完成費馬最後定理 Lean 形式證明：AI 寫碼之後，形式驗證成下一戰場

Anthropic 於 2026 年 9 月 4 日公布，其 Claude 多代理系統在約 11 日內，以 Lean 證明助手完成費馬最後定理（Fermat's Last Theorem）的端到端、可機器檢查形式證明。本文已核對 Anthropic 官方研究頁、證明倉庫說明，以及《New Scientist》等獨立報道；同日（9 月 6 日）Zoho 創辦人 Sridhar Vembu 在 X 的公開評論，亦反映業界對「AI 解題／寫碼＋形式驗證」組合的即時反應。本文重點包括：技術機制、代理協作架構、對數學審稿與軟件工程的啟示，以及香港企業可如何部署可控的私有 AI。

一、核心事件：把「證明」變成可執行程式

技術細節

費馬最後定理指出：對任意整數 n > 2，不存在正整數 a、b、c 滿足 aⁿ + bⁿ = cⁿ。Andrew Wiles 與 Richard Taylor 在 1990 年代完成人類可讀證明後，數學界仍長期推動把該證明「形式化」——改寫為證明助手可逐步檢查的邏輯程式。英國帝國學院 Kevin Buzzard 主導的 Lean 形式化項目，原本預期需以年計。

Anthropic 研究人員 Tianyi Peng（其團隊亦開發協作平台 Prove2Me）測試 Claude 能否推進該工作。結果超預期：約 11 日內，多個 Claude 代理協作產出端到端、經 Lean 檢查的證明；過程寫下約 1,300 萬行 Lean，並證明約 29,500 個中間定理（整體產生約 30,300 個可驗證定理證明）。證明依賴 Lean 的三個標準公理，定理陳述經比對工具確認與 Mathlib 中 FLT 陳述一致。Imperial College London 的 Kevin Buzzard 評價，該成果「除了數學公理外不作假設」，並指自動形式化產物已足夠穩健，可作為後續工作的基礎。

官方亦澄清：這次重點是「驗證」既有人類證明路徑（主要依循 Darmon、Diamond、Taylor 對 Wiles 論證的闡述），而非像部分黎曼猜想相關工作那樣提出全新數學命題。人類介入主要是高層指引（例如優先處理某些子定理），而非逐行手寫證明。

二、技術原理深度解析

早期嘗試顯示，多個代理容易「失去項目狀態」、協作失效；失敗嘗試約佔最終非樣板程式碼的 7%。關鍵轉折是改用 Prove2Me：以有向無環圖（DAG）管理定理陳述與依賴，讓代理決定下一步該證明什麼；把陳述與證明分檔以加速 Lean 編譯；並以自然語言描述定理，便於搜尋與重用。

執行層面採用 Claude Code 式多代理編排，消耗約 60 億輸出 token，底層為大致相當於 Claude Fable 5.1 的內部研究模型。最終證明規模約為 Mathlib 主庫的五倍以上，屬目前公開的最大 Lean 證明之一。完整產物已公開於 GitHub（anthropics/fermats-last-theorem），並附瀏覽用說明。

這套架構的啟示，不只屬於純數學：當 AI 代理要完成長程、多步驟工程任務，共享狀態圖、可檢查中間產物、失敗可回滾，比單代理「一路寫到底」更關鍵。形式證明助手提供的是極嚴格的「編譯器」——錯一步就無法通過；企業若把同類門禁用於關鍵業務邏輯，可把「AI 寫得多」轉成「AI 寫得可證」。

三、日常應用場景

1. 開發者與技術團隊

Lean／形式方法過去多見於關鍵系統與研究代碼。當 AI 能自動產出可機器檢查的中間引理，團隊可把「高風險模組」改為：AI 草擬實作 → 形式或屬性測試／證明助手檢查 → 人類審核介面與產品假設。Vembu 同日指出，Lean 等證明系統今日用於數學，很快也會用來驗證 AI 產出的軟件程式碼——重點不是「AI 全做完」，而是「還需要多少人、人做什麼」。

2. 企業與隱私敏感行業

金融、法律、醫療若把客戶資料送進公有聊天模型做長鏈推理，合規與外洩風險高。形式驗證與私有模型並非同一件事，但方向一致：把關鍵推理留在可控環境，並對輸出設硬閘。香港企業可把領域知識（合約條款、審核清單、內部 SOP）做成私有數據集與微調模型，再在閘道層加上規則與驗證，而非只依賴公有聊天框。

3. 一般用戶

對一般讀者而言，意義在於「可信度」：AI 產出的長篇論證，若能附帶機器檢查證明或至少可重現的形式化步驟，審稿與公眾討論成本有望下降。Buzzard 認為，自動形式化有助揪出既有文獻錯誤，並減輕審稿負擔；但官方亦強調，形式證明不應取代人類可理解的文字闡述。

4. 香港與亞洲市場視角

香港軟件外包與金融科技團隊，正同時面對「交付速度」與「正確性／合規」壓力。AI 編碼助手已普及；下一步競爭力更可能落在：私有模型是否掌握公司知識、輸出能否被自動驗證、事故能否披露與追溯。亞洲軟件服務商（包括印度 Zoho 創辦人的公開警告）亦在提醒同業：純「寫 code」崗位會被壓縮，能設計驗證流程、領域模型與代理編排的人才更值錢。

四、專業評價與潛在考量

優勢

把原本預期以年計的形式化工作，壓縮到約兩週級別，展示多代理＋共享狀態圖的實用性。
證明公開、可檢查，利於學術與工程社群複現。
直接對接軟件工程痛點：AI 產碼速度已超前人類審核速度，形式／自動驗證是補齊可信度的一條路。

需要留意的地方

這是「形式化既有證明」，不是 AI 獨立發現全新數學定理；對外溝通時不宜誇大為「AI 取代 Wiles」。
產物極長（千萬行級），尚未達 Mathlib 收錄品質；後續仍需人類整理、精簡與社群審視。
早期代理協作會失控，說明長程代理仍需工程化編排與硬閘；企業落地不能只靠「開一個聊天框」。
算力與 token 成本高（官方披露約 60 億輸出 token），並非所有團隊可複製同等規模實驗。

結語

Claude 在 11 日內完成費馬最後定理的 Lean 形式證明，標誌 AI 代理已能在高度結構化領域完成「可機器驗收」的長程協作。對企業而言，下一題不是會不會用 AI 寫碼，而是如何把私有數據、代理編排與驗證門禁做成可控系統。若香港團隊需要在本地部署企業私有 LLM（數據集 → QLoRA／LoRA → 私有 API，年費 HK$88,000 起，100% 數據不出境），可參考 YSK Limited 的企業私有 LLM 全託管（https://ysk.hk/services/ai-automation）。

參考來源