10 月 26 日，Axiom Math 在官方網站公布，他們用幾十個 AI 代理，在 24 天內把有限單群分類定理（Classification of Finite Simple Groups，簡稱 CFSG）的第一代證明寫成了 Lean 程式碼，總量約 4,310 萬行。原本的證明散在 500 多篇論文裡，約 15,000 頁，由大約 100 位數學家花了數十年陸續完成。
先把一個容易搞混的地方講清楚：這個專案沒有發現新定理，定理本身早就被數學界接受。它做的是把一份人類讀過、但沒有人完整讀完過的證明，改寫成電腦可以逐步檢查的形式。這篇想談的是兩件事：它怎麼做到，以及它在過程中找到了什麼。後者比 4,310 萬行這個數字更值得看。
這個定理在說什麼，為什麼形式化這麼難
單群是群論裡最基本的零件，可以想成不能再被拆成更小部分的對稱結構。CFSG 說，所有有限單群只會落在四類：質數階的循環群、五個以上元素的交錯群、十六個無限的李型群族，以及 26 個散在群（把 Tits 群算進去則是 27 個）。其中最大的散在群叫 Monster。
這個分類的證明由 500 多篇文章拼成，作者約 100 位。Axiom 這次形式化的是所謂的第一代證明。第二代證明是把全部論證重新整理成更短的版本，但根據 Axiom 的說明，它到 2023 年出到十卷，預期至少十二卷，還沒有完成，所以沒辦法拿來當形式化的對象。
形式化難，是因為論文裡的許多步驟寫成「顯然」「同理可證」「由先前結果得到」。人類讀者靠經驗補上這些空白，Lean 不行。每一個步驟都要明確寫出來，並且通過檢查。論文裡省略的部分，在 Lean 裡就是要自己從頭寫的證明。
24 天怎麼做：分工、里程碑與工程修補
根據 Axiom 的文章，時間線是這樣：10 月 1 日開了 Slack 頻道協調專案，10 月 2 日第一批代理群開始運作，10 月 10 日代理回報證明了 Monster 是單群。到 10 月 13 日只關閉了一個里程碑，團隊因此重新規劃。文章附的進度圖涵蓋 10 月 2 日到 10 月 25 日。
人類負責方向。專案被拆成 108 個里程碑與約 380 個較小的任務，依一張內部的證明地圖進行，協調走 GitHub issue 與 Slack。主導代理負責拆解論證、審查陳述是否寫對；其他代理負責在文獻中找結果，或實際寫 Lean 證明。Axiom 沒有公開更細的代理架構，Crypto Briefing 的報導也只提到分解、搜尋、寫證明、審查這幾種角色。
工程面的修補同樣重要。Axiom 列出的包括分散式的建置快取、平行檢查，以及把耗時的有限計算抽成可以獨立檢查的憑證（certificate）。依他們的說法，這讓驗證速度快了好幾個數量級。程式庫的 README 也提到，團隊用了幾個尚未併回上游的 Lake 修改，並計畫把完整建置時間優化到 24 小時以內。換句話說，現在要自己跑完整驗證，不是一般筆電能輕鬆完成的事。
過程中也有走回頭路。文章承認早期的里程碑依賴了尚未證明的假設，於是有數萬行程式碼被刪掉，部分工作重來。Axiom 自己提醒，在額外假設下完成的證明看起來像進度，但完成的條件是「沒有任何未經證明的假設殘留」，而完成的里程碑數量只是組織工作的工具，不等於證明完整。
34 項偏差：機器逐行檢查之後，文獻裡露出了什麼
Axiom 說，形式化過程找出 34 處值得注意的偏差，多數很小：打字錯誤、表格錯誤、被漏掉的假設。完整的勘誤表預計公布在 cfsg.axiommath.ai/errata，我寫這篇時無法從官方文章裡逐項核對這 34 項的內容，所以下面只談官方文章裡寫出細節的兩個例子。
第一個例子在 Aschbacher 與 Smith 的 quasithin 群分類裡。文獻中有一個等式被證明是錯的：以 SL₂(5) 為例，某個量等於 1，而論證需要它等於 2。Axiom 的做法是把等式換成不等式，並重新調整情況的分法。這是典型的小錯誤：結論沒有倒，但論證的某一步需要改寫。
第二個例子比較嚴重，出現在不平衡群定理（Unbalanced Group Theorem，UGT）。這部分是 John Walter 在 1986 年的證明。代理找到了明確的反例，證明他用到的一個封閉性斷言不成立。官方文章給的例子是 PSL₂(49)：它有一個域對合，其中心化子是 PGL₂(7)，而它的單成分 PSL₂(7) 被排除在 Walter 的群族之外，原因是 7 是梅森質數。
缺口出現之後，Axiom 寫了一段替代的論證，過程中有 Richard Lyons 與 Ronald Solomon 提供意見，結果收在隨附論文的定理 2.3（Preservation of simple tops）。形式化完成後，團隊又找到一條更短的推導，記在論文的 Remark 9.5，不需要用到定理 2.3。論文仍保留較長的版本，因為那是實際被形式化的路線。
這一段值得多看一眼的是順序。這個缺口是代理在寫 Lean 時卡住、回報之後，才由人類數學家調查出來的。Axiom 說，後果比較大的回報都有人類數學家介入查證。
這份成果的邊界
README 說這是一個 sorry-free 的 Lean 4 證明（Lean 版本 v4.35.0-rc3，建在 Mathlib 與 TauCeti 之上），只用了 `Classical.choice`、`propext`、`Quot.sound` 三個標準公理，也沒有使用 `native_decide`。目標陳述 `ClassificationStatement` 取自 TauCeti 專案：每個有限單群都同構於 `CFSGIndex` 所列出的、明確構造出來的群之一。程式庫採 Apache-2.0 授權，公開可查。
這些設定把風險縮小到一個地方：陳述是否正確。Lean 只檢查推導，不會知道 `ClassificationStatement` 的定義有沒有漏掉某一類群，或把某個條件寫鬆了。Axiom 自己也寫了，人類必須確認形式陳述符合原本想要的分類。這一步需要懂這個領域的人讀過定義，而不是跑一次 `lake build`。
另一個邊界是來源。目前能查到的完整說明主要出自 Axiom 自己的文章與程式庫，Crypto Briefing 的報導也引用公司的公告，沒有獨立的第三方審查。官方文章列了核心貢獻者（Dean Cureton、Vasily Ilin、Bhavik Mehta、Niels Voss）、28 位其他貢獻者，以及 Lyons、Dan Nakano 與 Solomon 三位外部顧問，但沒有描述顧問以外的獨立稽核。程式庫在我查閱時只有 1 筆提交紀錄。
對學術審查與 AI 研究工具的影響
先說判斷，再說誰可能不同意。我的判斷是，這個專案最有價值的產出是勘誤表與可重跑的檢查，而不是 4,310 萬行這個數字。對期刊與審稿人來說，過去面對一份上百頁的證明，只能抽查；現在在少數高價值的領域，審查可以改成「請附形式化證明」。這會先在證明很長、又被大量引用的領域發生。
可能不同意的人有兩種。一種是數學家，他們會說形式化把證明變得可檢查，但沒有讓人更理解它，而數學的目的是理解。另一種是看成本的人：24 天由幾十個代理加上一組人類顧問完成，算力與人力的帳目 Axiom 沒有公布，一般實驗室短期內做不到同樣的事。
對軟體與產品團隊，值得帶走的是做法而不是題目。Axiom 的流程是：把大任務拆成有明確完成條件的里程碑，讓一部分代理審查另一部分的輸出，用可獨立檢查的憑證處理昂貴的計算，並且在發現早期成果依賴未證明假設時敢刪掉重來。這套做法放在任何「結果可以被機器驗證」的工作上都成立，例如程式碼遷移、型別證明、規格比對。結果不能被驗證的工作，就拿不到同樣的保證。
還不確定的地方
第一，34 項的內容還沒有逐項公開查核。Crypto Briefing 寫的是「發現並更正超過 2,000 個錯誤」，Axiom 的官方文章寫的是 34 處值得注意的偏差，我在官方文章裡找不到 2,000 這個數字，這篇採用官方的說法。兩個數字可能指不同的分類標準，也可能是報導出了錯，在勘誤表公開之前無法判斷。
第二，Crypto Briefing 稱這是有史以來最大的 Lean 程式庫，這個說法我沒有在官方文章裡找到，也沒有第三方比較，所以標題與正文都沒有採用。
第三，形式陳述是否等於原本的分類定理，還需要外部數學家與形式化專家讀過定義才算數。程式庫的 `Comparator/` 目錄與 `comparator.json` 看起來是為了這件事準備的，但 README 沒有說明它的用法，我不推測它的功能。
第四，這個成果依第一代證明完成。第二代證明完成之後，是否能沿用同樣的流程，目前沒有資料。