AxiomProver 用 24 天完成有限單羣分類定理形式化

人類歷史上規模最大的數學證明，現已通過計算機形式化驗證。

有限單羣分類定理（CFSG，Classification of Finite Simple Groups），剛剛被AI徹底形式化！

百餘名全球頂尖數學家歷經大半個世紀、寫下長達15000頁的「數學天書」，被初創團隊Axiom研發的多智能體系統在短短24天內全部跑通。

更讓人頭皮發麻的是，AI構建了人類史上首個超4000萬行的Lean代碼庫。

按代碼行數計算，這現在是史上最大的開源軟件項目。它的規模超過了Linux內核、Chromium、Firefox、LLVM、GCC、FFmpeg等。

它甚至還在原有的證明中揪出了人類的漏洞，並親自證明瞭新的數學定理來完成修補！

知名數學家Ken Ono動情發文，悼念今年1月去世的數學家父親。

他回憶起童年時父親引薦自己走近羣論巨匠的歲月，在見證人機協作跨過這條歷史終點線時，這位數學大師忍不住當場淚崩。

數學的「對稱週期表」：巨型定理

在數學界，這個定理有一個如雷貫耳的綽號——「巨型定理」（The Enormous Theorem）。

在此之前，世界上沒有任何一個人能夠從頭到尾完整通讀它的所有證明。

到底什麼是「羣」？

簡單來説，羣是描述「對稱性」的數學語言。

比如，描述正六邊形的對稱性，對應一個二面體羣羣：

比如，用圖論看魔方，每個狀態是一個頂點，每一步移動是這張巨大圖中的一條邊。

這段動畫展示了排列如何穿越43百億億種配置，最終抵達解法。

而所有的有限羣，都可以像化學分子被分解為原子一樣，被分解為不可再分的「基本構件」——這就是有限單羣（Finite Simple Groups）。

分類定理的偉大之處就在於，它為全宇宙的對稱性開列了一張「元素週期表」。

它明確宣告：

所有的有限單羣，要麼屬於素數階循環羣，要麼屬於至少5個符號的交錯羣，要麼屬於16個無限家族的李型羣，要麼，就屬於26個極度特殊、無法歸類的「零散羣」（Sporadic groups）。

這26個零散羣中，最大的一個被數學家敬畏地稱為「魔羣」（Monster Group）。

順便提一句，1998年，Richard Borcherds因證明著名的「怪獸月光猜想」（Monstrous Moonshine），榮獲菲爾茲獎。這一猜想揭示了數學中一個令人震驚的聯繫：最大的散在單羣「魔羣」，竟然與數論中的模函數存在深刻的數學關聯。

2007年，物理學巨擘Edward Witten更是提出，這套包含魔羣的理論，可能被用來描述一個簡化宇宙中的引力，用來編碼黑洞在不同能級上的量子態分佈，從而計算黑洞的熵！

從1950年代開始，為了證明巨型定理，大約100位數學家在500多篇學術論文中，拼湊出了長達15000頁的證明，約14部《紅樓夢》。

它太龐大、太分散了，以至於1983年數學家Gorenstein宣佈證明完成時，其實還漏掉了一個巨大的缺口，直到2004年才由Aschbacher和Smith用1221頁的論文補上。

因為證明實在太長，人類極容易出錯。正如Aschbacher所言：「要寫出一個非常長且複雜的論證而不犯錯，是不可能的。」

既然人類的大腦已經逼近處理複雜邏輯的極限，那麼，是時候讓AI登場了。

AI出征：24天，幹了人類半個世紀的活

面對這座1.5萬頁的「數學珠穆朗瑪峯」，Axiom團隊沒有選擇傳統的蠻力計算，而是動用了多智能體蜂羣——AxiomProver。

把人類的自然語言證明翻譯成Lean代碼（即「形式化」），就等同於讓一台鐵面無私的機器，用放大鏡去檢驗那15000頁紙上的每一個標點符號。

2026年10月1日，Axiom團隊在一個Slack頻道里敲下了啓動的指令。

人類工程師和數學家將龐大的「巨型」拆解成108個里程碑和約380個小任務，生成了一張巨大的「證明地圖」。

10月2日，第一批AI「蜂羣」正式上線。

這羣AI智能體像一支訓練有素的軍隊一樣開始分工協作。領頭的AI負責拆解高難度的論證，其他AI則瘋狂搜索現有結果或埋頭編寫Lean代碼。如果一個AI遇到了還沒證明的先決條件，它會自動把這個任務外包給另一個AI。所有的結果都會匯聚到一個共享的代碼庫中。

整個過程並非一帆風順。由於AI編寫代碼的速度實在太快，Lean系統在重新檢查依賴項時甚至出現了算力瓶頸。

Axiom的工程師不得不臨時重構底層的工程基礎設施，開發了一套分佈式緩存系統，才勉強跟上AI那恐怖的產出速度。

10月10日，Slack頻道里彈出了一條讓所有人沸騰的消息：

我們證明瞭魔羣是單羣。

AI不僅從結構信息中識別出了魔羣，還通過代碼徹底形式化了它的存在！

僅僅24天！

在24個日日夜夜裏，這羣不知疲倦的AI智能體，產出了驚人的4310萬行Lean代碼，構建了人類目前最大的Lean代碼庫。

人類的智慧，經過了機器無情的檢驗，而且發現了其中的邏輯漏洞！

史詩級反轉：AI揪出人類大師的「致命Bug」並親手修復

人類的語言總是充滿省略。

有網友做詞一首，調侃數學證明中的思維跳躍：

西江月·證明

即得易見平凡，仿照上例顯然

留作習題答案略，讀者自證不難

反之亦然同理，推論自然成立

略去過程Q.E.D.

由上可知證畢

「顯然可得」、「同理可證」、「易證」……這些數學論文裏常見的詞語，對AI來説卻是行不通的。

形式化證明要求每一步都必須有明確的邏輯支撐。

在逐行掃描、強迫推理的過程中，AI智能體記錄下了數百處異常。其中大部分是人類的筆誤、表格錯誤或遺漏了前提條件，但有34處是重大的邏輯偏差！

而其中最驚險、最核心的一個「Bug」，出在至關重要的不平衡羣定理（Unbalanced Group Theorem,UGT）上。

UGT是整個分類定理中極為關鍵的一環，它的作用是「通過局部看整體」——通過研究一個羣的子羣結構，來推斷出整個大羣的真面目。

Axiom團隊最初選擇了John Walter在1986年發表的一篇權威文獻作為形式化的基礎。

然而，在翻譯這段人類自以為完美無缺的論證時，AI智能體突然發出了紅色警報！

AI發現，Walter證明中的一個關鍵閉包斷言，在邏輯上是站不住腳的。

AI不僅指出了錯誤，還給出了一個明確的反例：PSL₂(49)。在這個反例中，一個操作會產生一個被明確排除在目標家族之外的羣（因為7是梅森素數）。

人類引以為傲的證明，在這一刻斷鏈了。

長達1.5萬頁的邏輯大廈，隨時面臨崩塌的危險。

怎麼辦？如果去借用後人寫的「第二代證明」，不僅會引入海量的全新依賴，還會讓這24天的努力前功盡棄。

此時，人機協作的巔峯一幕上演了。

Axiom團隊緊急連線了當年參與CFSG原始工作的活化石——羣論泰斗Richard Lyons和Ronald Solomon。

在聽取了AI發現的漏洞後，人類大師的直覺與AI的算力展開了完美共振。基於Solomon在1976年提出的理論，人類數學家構思出了一條新的證明路線。

隨後，AxiomProver（AI系統）親自上陣，根據新思路，嚴絲合縫地證明瞭一個全新的羣論結果——Preservation of simple tops。

這個由AI主導證明的新定理，像一塊完美的定製補丁，精準地填補了人類大師當年留下的窟窿，成功推導出了分類定理所需的UGT形式！

定理依然成立，但證明已經不完全屬於人類了。

這是人類歷史上第一次，AI在最頂級的純數學研究中，不僅充當了「驗算器」，更成為了發現新定理、修補核心漏洞的「合作研究員」！

這不禁讓人想起數學史上類似的一幕：2002年菲爾茲獎得主Vladimir Voevodsky，發現自己的證明是錯的，而且救不回來。

1999–2000年，在普林斯頓高等研究院講課時，他發現早年關鍵引理有誤，原命題無法按原樣挽救。

2013年又確認1989年另一項結果也錯了——反例早在1998年就有人提出。

他不再相信人類能可靠地檢查複雜證明，轉向Coq、同倫類型論與單值基礎：讓計算機驗數學。

在追求數學真理的道路上，人類用血肉之軀和有限的大腦，進行了長達近兩百年的悲壯遠徵。

如今，人類有了新的合作伙伴，一起探索知識疆域的星辰大海。

參考資料：

https://x.com/KenOno691/status/2115090084861247680

https://axiommath.ai/research/the-enormous-theorem-formalized/