Axiom CFSG 形式化解析：巨型證明如何驗收，AI 貢獻怎麼看？（2026）

2026 年 10 月 26 日，Axiom 在官網發布〈Formalizing the Enormous Theorem〉，宣布完成有限單群分類定理的 Lean 形式化。這次 Axiom CFSG 公告最值得追問的是：一份跨越大量文獻的證明，如何從「許多段各自成立的推導」，變成能一路追到最後結論的整體？

先讀原文的成果與工作方式，再核對公開程式碼及數學材料，最後判斷這件事改變了什麼。目前能確認的是公告、原始碼與檢查入口已公開；本文沒有完成整庫的獨立建置，也不把廠商回報改寫成 AlphaLab 實測。

Axiom CFSG 到底要證明什麼？先分清「積木表」與「所有組裝方式」

群可以用來描述對稱：把一個物件變換後，再接另一個變換，仍落在同一套規則內。有限單群則是有限群的一類基本組件；這裡的「單」指它非平凡，而且沒有其他非平凡真正規子群，並不是說它的結構簡單。

分類定理給出的清單包括質數階循環群、一定範圍的交錯群、李型單群，以及 26 個散在單群。這張表回答「基本組件有哪些」，不等於已列出有限群的每一種組裝方式。這個區別也見於 這次 UGT 論文的開頭說明。

更難的部分是清單的完備性：不論拿來哪一個有限單群，都得能對上清單中的某個群。Axiom 採用的 TauCeti 定理陳述，正是把「每個有限單群，都同構於清單中的一個具體群」寫成明確命題。

這不是從零發明 CFSG。早在 2012 年的原始公告，Gonthier 團隊就已宣布用 Coq 完整檢查 Feit–Thompson 奇數階定理；其 2013 年論文記錄六年的協作與可重用數學函式庫。Axiom 的公開 README 明列主要遵循第一代證明，並建立在 Mathlib 與 TauCeti 上。兩段工程的規模、起點與工具不同，不能用年數相除，宣告 AI 的通用數學生產力提高了多少倍。

4,310 萬行與 24 天：先讀成專案紀錄

approximately 43.1 million lines of code

中文：約 4,310 萬行程式碼。

Axiom，原文

原文把這個數字放在 24 天的專案敘述中：工程師與數學家指揮多個 AI Agent，拆題、撰寫、檢查並整合。這是 Axiom 自報的產出量與期間，不是獨立測得的效率指標。這個期間應與既有文獻、前置函式庫及人類知識一起理解。

原文的工程紀錄稱，團隊先用證明地圖分工，曾刪除建立在未證明前提上的工作，再把大目標拆成更小的精確命題；共享建置快取與可另行檢查的計算憑證，則協助降低重複檢查的負擔。致謝也記錄納入約 120 萬行 Qiuzhen-CFSG 程式碼。這些都是團隊對工作過程的回報。

這類專案可以把工作量分散出去，但交接會創造新的約束：甲證出來的結論，必須正好符合乙所需的假設；兩人對同一個物件的定義，也得接得起來。否則每段推導都成立，最後仍可能拼不出目標。

把這張圖想成一張供應關係圖：圓心要用到周圍許多結果。真正有用的問題是「最終定理需要的前提，是否都已接上」，而不是「又新增多少行」。這與 Agent Harness 的分工與執行迴圈有相通之處：增加工作者能擴大產出，完成條件仍要在整體系統中驗收。

UGT 的修補：一條推論有反例，與整個定理被推翻不同

Axiom 公告稱，形式化過程處理了 34 項值得注意的文獻偏離，並指出 Unbalanced Group Theorem（UGT，不平衡群定理）是較重大的部分。這個總數仍是團隊整理的口徑；要評估數學內容，應逐項讀反例、修正與依賴。

2026 年 10 月 27 日公開的 UGT 論文 v1提供了一個具體入口。論文 Remark 1.6 明列 UGT 已有其他證明路線；Axiom 主要形式化第一代證明，所以還要考量替代路線能否接入這次的依賴。作者指出，Walter 的一條既有證明路線用到了某個封閉性判斷：做完特定操作後，得到的群仍應留在指定家族內。但論文給出的例子從 PSL₂(49) 出發，取域的二階自同構，其中心化子同構於 PGL₂(7)，其中的簡單組件是 PSL₂(7)。這個自同構不是原群內的元素；PSL₂(7) 則因 7 是梅森質數，被排除在該家族之外。

論文的 Remark 1.8 把範圍說得很清楚：反例針對這個推論步驟，不是 UGT 本身或該命題結論的反例。因此，「AI 推翻了整套有限單群分類」會把局部論證問題誇大成最終結論失效。

同一篇論文提供替代論證，Theorem 2.3 討論在特定條件下保存簡單商群的型別；Remark 9.5 又記錄一條較短推導，並明說它不需要 Theorem 2.3；保留較長路線，是因為 AxiomProver 形式化了這條路線，而且它還給出更強的保存結果。這些是作者提出、可供群論研究者檢查的數學結果，不能只用「程式庫可下載」替它們完成外部認證。

這個案例的意義，在於修補會向後傳遞：改掉一個錯誤的中間步驟，還要確認後面原本依賴它的論證仍能前進。若只是把每個缺口各自補一塊，卻沒把下游重新接通，整份證明的完成狀態仍不清楚。

Axiom CFSG 的公開碼：可以看到什麼，還需驗什麼？

截至 2026 年 10 月 29 日，本次讀取的儲存庫版本為 69cb972。README宣稱使用 Lean 4.35.0-rc3、沒有 sorry 的完成證明，並只依賴 Classical.choice、propext、Quot.sound 三個標準公理；這些是專案對驗證狀態的聲明。

實際可讀的 Comparator 解答檔，把 Certified 模組的 classification_finite_simple_groups 接到 TauCeti 的分類命題。設定檔則指定目標定理與允許的三個公理。這讓外部檢查有具體對象；設定檔的存在，本身不代表這次執行已成功。

如果打開 Challenge 題目檔，會看到 sorry。它在此用來放置待匹配的題目陳述，解答另在 Solution 檔。題目模板的佔位符，和最終解答的依賴中留下未證明假設，是不同位置、不同問題。只做全庫文字搜尋，既不能據此判整份證明失敗，也不能替整份證明背書。

README 給出的整庫建置入口是 lake build，並稱團隊透過 Lake 的修改與最佳化，把其建置時間降到 24 小時內。本文未在本機完成這條重建流程，也未取得一份可由本文確認的第三方整庫重建紀錄；因此，完整通過的判斷仍保留為團隊宣稱。若要親自驗證，應在隔離環境固定版本、檢查建置檔，再保存完整輸出與資源條件，別把它當成幾秒就能跑完的示範。

Lean 檢查與人類審閱，各自回答哪一題？

Humans inspect that statement and the definitions it uses

中文：人類檢查那個定理陳述，以及它使用的定義。

Axiom，原文

Lean 官方驗證指南同樣把「命題有有效證明」與「命題到底是什麼意思」分開。它說明公理盤點、重新檢查編譯產物，以及 Comparator 比對可信題目陳述等不同層次；未經審閱的 AI 程式，也需要考慮誤導或繞過檢查的風險。

原文已明確區分人類檢查陳述、Lean 檢查推導這兩種責任。接下來的外部問題，是其他人如何重做這些檢查、建立自己的信心。可以用三個問題理解它。第一，題目對嗎？定義、範圍與假設，是否真的表達人們想說的 CFSG？第二，推導對嗎？證明是否在允許的公理下接通，並經過對應的檢查？第三，證據能交給別人嗎？其他人能否從指定版本、工具鏈與步驟重現同一結果？前兩題關係到數學內容，第三題讓外界更容易累積信心。

這不是說每次都要讀完數千萬行程式，才有資格討論成果。讀者可以先確認可信目標、驗證紀錄與外部檢查者各在哪裡；當一份報告只回答其中一題，就把信心停在相應範圍。本站的 形式驗證與安全證明邊界解析，也處理了規格與現實問題如何接合。

AlphaLab 的判讀：值得期待的是可累積的數學基礎

我同意：把隱藏依賴攤開，成果才更容易被接著使用

一個已知定理的形式化，仍然可以帶來新價值。過去用一句話引用的成果，若變成定義與依賴明確的元件，後續工作就更容易看清到底借用了什麼。判斷這次發布的長期份量，我會看外部研究者能否重用其中結果、修正是否被清楚討論，以及維護者能否持續讓全體依賴保持一致。

原始碼公開使這些問題變得可以追問。它也把成果的一部分，從「相信這個團隊的敘述」移到「針對某個版本提出可重做的檢查」。這個轉變值得肯定；接下來每一份獨立驗證與有效重用，都能增加具體證據。

我存疑：把長度與速度，直接換成人類數學家的替代率

Human expertise remained essential.

中文：人類專業仍然不可或缺。

Axiom，原文

這句原文提醒我們，這次成果屬於人、Agent、既有文獻、函式庫與檢查基礎設施的組合。若要估計 AI 的額外貢獻，就得有可比較的起點、工作範圍、投入資源及完成標準。單一專案的行數與日數，無法分離這些因素。

同樣地，把一個已知定理形式化，與挑選重要研究問題、發現有效概念、找到新定理，是相連卻不同的能力。UGT 材料中的新論證值得研究，但不能因此預先宣告所有數學研究任務都已跨過同一道門檻。若想比較新研究主張的發布方式，可接著讀 OpenAI 的 ETH、Kakeya 與量子場論證據分析。

下一個瓶頸，可能是維護與理解的成本

當寫出更多證明變容易，外部研究者仍需要找到相關結果、讀懂假設、信任介面，並在版本變動後繼續使用。假如生成速度遠高於審閱與重建速度，單純累積檔案會讓驗證負擔加重。值得追蹤的進步，是每份可重用且可信的數學成果，總共需要多少人力、算力與維護時間。

接下來怎麼追？先保存一張四欄表

一般讀者可以記四欄：定理目標、公開版本、驗證紀錄、外部回應。看到「已完成」時，先找到它是哪個定理、哪次提交、哪一種檢查；看到「發現錯誤」時，再看反例攻擊的是中間步驟、命題本身，還是最終分類。這比把每次公告都壓成「AI 又贏了」更能保留成果的真實差異。

若你在做 Agent 系統，則可從這個案例帶走一個設計問題：子任務交回結果時，是否同時交回了假設、依賴與驗收證據？可參考 建立 Agent Harness 的流程，再用 AI Evals 的評分觀念把完成條件寫成檢查項。形式化的經驗能啟發工程；一般商業任務的正確性，仍要用各自的資料與規格驗收。

Axiom CFSG 最有份量的承諾，是讓一座龐大的證明可以被逐段追問、修補與接著使用。判斷它是否兌現，下一步應追定理與驗證紀錄；把視線從「產出多少行」，移到「哪些推導真的接上、誰能重做，以及誰已用它走出下一步」。