數學 AI 公司 Axiom 宣布，旗下的 AxiomProver 智慧體集群在 24 天內完成了有限單純群分類定理（CFSG）的 Lean 形式化，並稱這是該定理的第一份完整電腦檢查證明。程式碼已在 GitHub 以 Apache-2.0 授權開源，儲存庫聲明最終版本中沒有 sorry 佔位、沒有使用 native_decide，只依賴命題外延性、古典選擇公理與商的可靠性這三條標準公理。
有限單純群分類常被稱為「對稱性的元素週期表」。它指出所有有限單純群，要嘛屬於 18 個無限族，要嘛是 26 個散在群之一。原始證明分散在 500 多篇論文中，約 1.5 萬頁，由大約 100 位數學家從 1955 年前後寫到 2004 年，最後一塊 quasithin 部分出自 Aschbacher 與 Smith，單篇就有 1221 頁。
24 天裡發生了什麼
依 Axiom 公布的過程，專案在 10 月 1 日建立了 Slack 協作群組，10 月 2 日第一批智慧體上線。整份證明被拆成 108 個里程碑、約 380 個小任務，智慧體在 GitHub issue 上認領任務，並在 Slack 中回報進度。主導智慧體負責拆題與審查命題，其餘智慧體檢索既有成果或撰寫 Lean 證明，缺少前提時再往下派工。
過程並不順利。早期一批程式碼因隱含假設出錯而整批刪除，團隊重新規劃；之後建置速度成為瓶頸，工程師利用快取、平行檢查，並把有限計算外移成可驗證的憑證，將完整建置時間壓到 24 小時以內。10 月 10 日，專案另行宣布證明 Monster 群是單純群。
語料方面，Axiom 表示共讀入 715 篇論文與書籍，並重複利用先前 Qiuzhen-CFSG 專案約 120 萬行程式碼，以及 Mathlib、Tau Ceti 等既有形式化函式庫。
順帶挑出的錯誤
形式化過程中，團隊記錄了 34 處較明顯的數學偏差。最受矚目的一處出現在「不平衡群定理」（UGT）路線上：Walter 1986 年回憶錄中的一項閉包斷言有反例，從 PSL₂(49) 出發會推到 PSL₂(7)，而後者恰好被該族排除在外。Aschbacher–Smith 的一條引理也找到了 SL₂(5) 反例，等式改為不等式後，後面的論證也得跟著擴充。
Axiom 為此另外發表一篇 35 頁的論文，提出替代論證，並在 Lyons、Solomon 等顧問參與下修補這條路線。公司一再強調，這些反例並未推翻 UGT 本身，更沒有動搖分類定理。
"the classification remains the achievement of the mathematicians who discovered the groups"
（分類仍是發現這些群的數學家們的成就。）
與以往機器驗證的比較
橫向來看，最常被拿來對照的是 Gonthier 團隊 2012 年在 Coq 中完成的奇數階定理驗證。該定理源自 Feit 與 Thompson 1963 年 255 頁的論文，專案前後約六年，是分類證明裡的一塊基石。Axiom 這次涵蓋的是整棟大樓，耗時以天計算。
兩者不能直接比較速度。奇數階專案當年幾乎從零建構函式庫，Axiom 則站在 Mathlib 與先前 120 萬行 CFSG 程式碼之上，智慧體數量為「數十個」，背後的算力、硬體與總成本都沒有揭露，工時也未公開。24 天是形式化專案本身的週期，並不包含它所依賴的數十年人類工作。
幾項保留意見也寫得很明白。專案中繼資料把審查標註為「自我評估」，目前還沒有第三方在乾淨環境中重現完整建置；機器檢查只能保證推導從寫下的假設出發成立，分類陳述的定義是否忠實於原定理，仍須群論學者逐條核對。那篇 UGT 論文發表在不做同儕審查的預印本平台上，勘誤表 Axiom 表示會放在專案頁面。
對從事形式化的人來說，接下來要看兩件事：社群能否獨立跑通這 4310 萬行，以及 34 處偏差中有多少能獲得原作者一方的確認。
參考來源：Axiom 專案公告與 GitHub 儲存庫、Unite.AI、CocoLoop、Kingy AI；Lean 程式碼行數、宣告數、里程碑數與偏差數以 Axiom 公布的口徑為準，奇數階定理驗證週期依據微軟研究院資料。