Axiom Math 發佈 43.1M 行 Lean 有限單羣分類證明

Axiom Math 於 2026 年 10 月 27 日表示，正發佈其所稱的首個完整、經電腦驗證的有限單羣分類證明。這項證明歷時 24 天，由工程師和數學家指揮數十個 AI Agent 組成的蜂羣完成；這些 Agent 在 Lean 證明助理中編寫了約 43.1 million 行程式碼。

「今天，我們發佈首個完整、經電腦驗證的有限單羣分類（CFSG）證明。」公司在公告中寫道。這項分類確定有限羣的基本構成單位；原始證明分散於 500 多篇文章，合共約 15,000 頁，由約 100 位數學家撰寫，規模之大令它得了「巨型定理」這個綽號。

Axiom 發佈的內容

CFSG 證明，每個有限單羣都是素數階循環羣、作用於至少五個符號的交錯羣、在有限域上構造的十六個李型羣無限族之一，或恰好 26 個孤立散在羣之一；公告指出，部分作者會將 Tits 羣計作第 27 個散在羣。最大的散在羣 Monster 由 Robert Griess 於 1980 年利用一個維度為 196,884 的代數構造出來。

人類的證明工作歷時數十年。1963 年，Walter Feit 和 John Thompson 在一篇長達 255 頁的論文中證明，每個非阿貝爾有限單羣的階都是偶數；該論文佔滿了整期《Pacific Journal of Mathematics》。Daniel Gorenstein 於 1972 年提出一套十六步計劃以完成這項分類，並於 1983 年宣稱分類已完成；但準薄情形當時仍依賴 Geoffrey Mason 一份未完成的手稿，直至 Michael Aschbacher 和 Stephen Smith 於 2004 年發表長達 1,221 頁的論述，才完成後來稱為第一代證明的工作。Gorenstein 和 Richard Lyons 展開了更有系統的第二代證明，Ronald Solomon 和 Inna Capdeboscq 其後加入，但這項工作至今仍未完成，因此 Axiom 將第一代證明形式化。

項目網頁介紹，這項形式化工作依循第一代證明，並由 Lean 的核心檢查每個邏輯步驟；網頁列出 43.1 million 行 Lean 程式碼、2.05 million 項宣告，以及文獻庫中的 715 篇論文和書籍。Axiom 表示，其證明路線圖參考了第二代證明的各卷；形式化工作亦納入約 1.2 million 行來自早期 Qiuzhen-CFSG 專案的程式碼，並以 Mathlib 為基礎，該專案有數百名貢獻者參與。項目列出的核心貢獻者包括 Dean Cureton、Vasily Ilin、Bhavik Mehta 和 Niels Voss，主要研究員則是 Letong Hong。

公開 GitHub 儲存庫將成果描述為不含 sorry 的 Lean4 證明，固定使用 4.35.0-rc3 版本，以 Mathlib 和 TauCeti 專案為基礎，並只使用標準公理 Classical.choice、propext 和 Quot.sound，不使用 native_decide。這項取自 TauCeti 的分類形式化陳述如下：「每個有限單羣都同構於分類清單中明確構造的其中一個羣。」README 指出，lake build 會檢查整個開發項目；對 Lake 建置工具作出的公開修改，以及團隊計劃回饋上游的最佳化，令建置時間降至 24 小時以下。程式碼採用 Apache-2.0 授權。

為期 24 天的 Agent 羣體協作

2026 年 10 月 1 日，Axiom 開設了一個 Slack 頻道，以協調這項計劃。團隊利用既有的 Lean 工作，以及根據已發表文獻整理的內部證明架構圖，將整項工作劃分為 108 個里程碑和約 380 項較小的任務；首批代理於 2026 年 10 月 2 日開始運作，透過 GitHub issues 認領里程碑，並在 Slack 回報已完成的工作。主導代理負責拆解困難的論證和審核命題，其他代理則搜尋現有結果或撰寫 Lean 證明；代理亦可把尚缺的前置結果交由其他代理處理，相關成果再納入共用儲存庫。

初期進展暴露了薄弱之處。一些表面上看來容易處理的里程碑，實際上隱含了龐大的前置工作，而代理把這些工作當作已成立，沒有加以證明；團隊因此刪除了數萬行建基於這些假設的內容，並以更可靠的計劃重新開始。其中一項早期里程碑涉及訊號子函子定理，其候選證明依賴一些仍有待論證的結構性假設。隨着代理產生證明的速度超越 Lean 重新檢查證明的速度，建置時間亦成為瓶頸。Axiom 表示，工程師把快取的建置結果分發至各工作節點、平行執行獨立檢查，並把成本高昂的有限計算交由外部處理，再產生可獨立檢查的證書；公司稱這些改動令驗證速度提升了數個數量級。

Axiom 回述，2026 年 10 月 10 日，頻道內有訊息宣佈代理已證明怪獸羣是單羣；代理亦透過 Griess 代數將怪獸羣的存在形式化，並證明一項識別 Monster 型羣與怪獸羣的定理。2026 年 10 月 13 日，團隊只完成了一個里程碑。工程師隨後展開重新規劃工作，把未完成的里程碑拆分為較小且陳述明確的定理；每項拆解都必須展示如何透過一段簡短的 Lean 證明，證明各部分足以得出原有的里程碑。

已發表證明中的漏洞

Axiom 表示，把證明轉換成 Lean 證明，暴露了已發表論證中的問題。大部分問題都很輕微，例如排字錯誤、表格錯誤或遺漏假設；但公司統計，當中有 34 項值得注意的差異偏離了已發表的記錄，最重大的問題涉及 Unbalanced Group Theorem（UGT）。

其中一個例子來自 Aschbacher 和 Smith 的準薄羣系列著作，當中的一項引理聲稱兩個數值相等。代理找到一個涉及羣 SL₂(5) 的反例，其中一個數值是 1，但該等式要求它應為 2。把等式改為不等式修正了引理，但後續論證曾利用等式排除某些情況，因此團隊擴展了較早的論證，以涵蓋這些情況。

UGT 有助根據子羣的資訊識別整個羣：根據配套論文的摘要，在分類定理的歸納假設下，若一個非平凡的奇數階子羣正規於某個對合元的中心化子，則所在的單羣必須是奇特徵的李型羣，或是特定次數的交錯羣。Axiom 參照 John Walter 1986 年的專論研究 UGT；在形式化該論證時，代理發現其中採用的一項封閉性斷言存在明確的反例：一項原以為能使相關單羣留在指定羣族內的運算，實際上卻可能產生一個明確被排除在該羣族之外的羣。

按該公司的説法，以 PSL₂(49) 為起點，其域對合的中心化子為 PGL₂(7)，而該操作會得出簡單分量 PSL₂(7)；由於 7 是梅森素數，這個分量不屬於該家族。Axiom 指出，這些反例並未推翻 UGT 本身，甚至沒有推翻 Walter 命題 II.5.9(ii) 的結論。

這項修補工作借鑑了 Solomon 於 1976 年提出的最大 2-分量理論。Axiom 表示，該理論為其 AxiomProver 系統生成並形式化的另一套論證提供了核心思路。論文將關鍵步驟列為定理 2.3（簡單頂層的保留）；Axiom 稱，這是由 AxiomProver 證明的羣論新結果。結合 Gilman 和 Solomon 的化約，以及 Foote 和 Harris 的識別定理，這項結果提供了分類所需的 UGT 簡單羣形式。完成形式化後，Axiom 的數學家在第一代方法的框架內找到一個更簡短的推導，並記錄為備註 9.5；該推導無須使用定理 2.3，也能得出相同結論。

該論文《The Unbalanced Group Theorem》由 Colin Defant 和 Ken Ono 撰寫，於 2026 年 10 月 27 日以版本 1 發表在 Hexagon 預印本伺服器，採用 CC BY 4.0 授權；專案頁面列明全文共 35 頁。Axiom 表示，正與羣論學者合作整理文獻中發現的勘誤，並會在專案的勘誤頁面上發布。Axiom 就 UGT 的修補工作諮詢了 Lyons 和 Solomon；他們的研究是這項分類工作的基礎。公司表示，將繼續在包括兩人在內的顧問委員會，以及外部顧問 Dan Nakano 的協助下，整理並處理勘誤。Axiom 將自身的貢獻定位為讓證明可以透過機器檢查、記錄遇到的障礙，並提供解決這些障礙的形式化論證；同時指出，這項分類工作仍是發現這些羣並發展相關論證的數學家的成就。