近一個月以來，AI 正逐步探入數學研究的腹地。10 月 6 日，OpenAI 在程式碼託管平台 GitHub 上一次性公開了 722 份由內部模型生成的數學手稿，涉及數百個開放問題；10 月 26 日，OpenAI 團隊又公佈了其模型在調和分析、計算複雜性理論和量子場論上的新發現。
AI 產出證明的速度越來越快，如何確認這些證明可信，就成了數學界必須面對的問題。
其中一種應對辦法是形式化驗證，即借助證明助手 Lean 等工具，把數學家用自然語言寫成的證明逐句“翻譯”成電腦能夠檢查的形式語言。論文中常見的“顯然”“同理可得”在 Lean 裡行不通，任何省略的推導和隱含的條件都必須寫明，每一步推理都要經過 Lean 核心的逐條檢查才算通過。
10 月 27 日，美國 AI 數學公司 Axiom 公開了一項體量罕見的成果，宣佈其 AI 智能體已在 Lean 中為有限單群分類定理（CFSG）完成了完整的形式化。CFSG 的原始證明約 15,000 頁，分散在 500 多篇論文中，出自約 100 位數學家之手，是人類數學史上篇幅最長的證明，人稱“巨型定理”。
Axiom 的工程師和數學家調度數十個 AI 智能體，用 24 天寫出約 4,310 萬行 Lean 程式碼，目前已在 GitHub 將其開源。
01. 一份沒人能讀完的證明
數學家用“群”描述對稱性。一個正方體有 24 種旋轉方式能讓它看上去和原來一模一樣，這 24 種旋轉連同它們的組合規則就構成一個群。整數可以分解為質數的乘積，有限群也可以層層拆解，最終得到無法再拆分的基本單元，即有限單群。
CFSG 給出了所有有限單群的完整名錄：素數階循環群、交替群、16 個由有限域構造的李型群家族，外加 26 個不屬於任何家族的“散在群”。其中最大的魔群（Monster group）約有 8×1053 個元素。數學家常把這份名錄比作對稱性的元素周期表。
列出名錄相對容易，難的是證明名錄之外再無遺漏。這項工作從 20 世紀 50 年代起步，約翰·湯普森（John Thompson）因奠基性貢獻獲得 1970 年菲爾茲獎和 2008 年阿貝爾獎。1983 年，群論學家丹尼爾·戈倫斯坦（Daniel Gorenstein）宣佈分類完成，但很快有人發現，其中“擬薄群”一類情形只依靠一份未完成的手稿。
這個缺口直到 2004 年才由邁克爾·阿施巴赫（Michael Aschbacher）和斯蒂芬·史密斯（Stephen Smith）用一部 1,221 頁的專著補上，2008 年學界又修補了另一處漏洞。這些論文和專著共同構成了如今所說的“第一代證明”。
證明的分散也成了難題：不同年代的論文使用不同的記號和組織方式，結論之間層層引用，弄清它們如何拼接需要深厚的專門知識。
從 20 世紀 80 年代末開始，參與分類工作的學者著手撰寫更系統的“第二代證明”，到 2023 年已出版 10 卷，預計至少需要 12 卷，至今仍未寫完。與此同時，代數、數論、組合數學乃至數學物理中的大量結論都以 CFSG 為前提。
02. 一家想“形式化驗證一切”的公司
Axiom 成立於 2025 年 3 月，創始人兼 CEO 洪樂潼（Carina Hong）是在廣州長大的 00 後。她高中時入選廣東數學奧林匹克省隊，在麻省理工學院（MIT）用三年修完數學與物理雙學位，因本科期間的研究獲得美國本科生數學研究最高獎項摩根獎（Morgan Prize），並以羅德學者身份赴牛津大學深造，在進入史丹佛大學讀博期間輟學創業。
公司的“創始數學家”、數論學家小野健（Ken Ono）2025 年離開弗吉尼亞大學加入 Axiom，洪樂潼本科期間曾在他主持的暑期科研項目中做研究。公司先後完成 6,400 萬美元種子輪和 2 億美元 A 輪融資，估值已超 16 億美元。
Axiom 把“形式化驗證一切”當作使命，其智能體系統 AxiomProver 能調度多個 AI 智能體協同完成大型形式化任務。今年 8 月，團隊完成了素數間隙領域“246 定理”的形式化，這一定理表明存在無窮多對相差不超過 246 的素數。
用小野健的話說：世界即將運行在沒人讀過的程式碼之上，證明的形式化是應對這一挑戰的試驗場。
CFSG 把這個試驗場推到了極限。它體量最大、結構最分散，真正能讀懂全部論證的人卻越來越少。項目核心成員瓦西里·伊林（Vasily Ilin）在社交媒體上寫道，真正理解這個證明的人大多已經退休或離世。在一份靠集體記憶維繫的證明上做機器核驗，對數學界是一項基礎建設，也是對Axiom技術能力最直接的檢驗。
03. 24 天裡，推倒再重來
Axiom 並非從零起步。Lean 社區數百位貢獻者共同維護的數學庫 Mathlib 提供了大量基礎定義和定理。在丘成桐的倡導下，清華大學求真書院學生聯合丘成桐數學科學中心等機構推進的 CFSG 形式化項目此前已積累了大量群論程式碼，Axiom 將其中約 120 萬行納入了自己的工程。
團隊參照第二代證明的多卷著作繪製了一張證明地圖，把整套論證拆成 108 個里程碑、約 380 項子任務。但由於第二代證明尚未寫完，形式化的對象定為第一代證明。
10 月 2 日，第一批智能體叢集上線。負責統籌的智能體拆解複雜論證、稽核待證命題的表述，其餘智能體檢索已有結論、編寫 Lean 程式碼。某項任務依賴尚未完成的前置結論時，系統會把這部分交給其他智能體，完成的結果匯入共享程式碼庫供後續呼叫。人類數學家處理數學上的卡點，工程師維持系統運轉。
起初的推進並不順利。早期一些看似可控的里程碑背後藏著大量尚未證明的前提，智能體直接把它們當成既定事實寫了下去。團隊刪掉了建立在這些假設上的數萬行程式碼，部分工作因此必須推倒重來。
10 月 10 日，項目頻道里傳來消息，魔群的單群性證明完成。智能體還同時證明了魔群的存在，這是整個分類中最關鍵的環節之一。
公司記錄顯示，3 天後，進度突然陷入停滯，當天只完成了 1 個里程碑。工程師很快意識到，問題出在里程碑劃分過粗，剩餘工作量難以判斷，於是他們重新規劃，把未完成的里程碑拆成更小、表述更精確的定理。
程式碼規模膨脹也帶來了新的問題。智能體寫證明的速度超過了 Lean 重新檢查的速度，改動一處共享結論，所有依賴它的內容都要重新校驗，分佈在不同機器上的智能體還會重複計算。工程師為此搭建了快取分發系統，未改動的程式碼直接復用此前的檢查結果，整體校驗速度提升了幾個數量級。
10 月 26 日，形式化完成。Lean 核心確認，從基礎公理出發直到最終的分類定理，所有推理環節首尾相接。形式化陳述是否精準表達了數學家心目中的 CFSG，仍需要人類審閱，Axiom 在發佈時邀請群論學者和 Lean 社區重新運行檢查，並核對定理陳述與原定理是否一致。
逐行核對的過程，也是對文獻的一次徹底體檢。智能體在形式化中記錄下大量疑點，其中不少源於智能體自身的誤讀，需要人工逐一排查。已得到確認的問題大多是筆誤、表格資料錯誤和遺漏的前提條件，另有 34 處與已發表文獻的偏差需要專門處理。Axiom 表示將與群論學者合作，把整理好的勘誤表公開給學界。
最棘手的問題出現在非平衡群定理（Unbalanced Group Theorem）。分類證明的基本思路是反證：假設存在一個不在名錄上的單群，取其中最小的一個，再逐一排除它可能具有的結構。非平衡群定理負責排除其中一大類情形，是通往最終結論的必經環節。
團隊沿用群論學家約翰·沃爾特（John Walter）1986 年的論證，智能體卻在其中一條斷言上找到了明確的反例。原文認為某種操作產生的單群始終留在一個特定的群族之內，實際上它可以產生恰好被排除在該族之外的群。反例沒有推翻定理本身，但原論證的關鍵一步失去了依據。
換一條已發表的證明路線並不輕鬆，每條新路線都會牽出一批尚未形式化的前置結果，工作量可能成倍增長。
團隊為此請教了當年參與分類工作的理查德·萊昂斯（Richard Lyons）和羅納德·所羅門（Ronald Solomon）。理查德幫助梳理了可行的證明路線及其歷史脈絡，羅納德 1976 年提出的“極大 2-份量”理論則提供了替代論證的核心思路。
AxiomProver 據此構造並形式化了一條新的論證路線，其間證明了一個此前沒有的群論結果，相關論文已發佈在預印本平台 Hexagon。
形式化完成後，Axiom 的數學家又在第一代證明的方法框架內找到一條更短的推導，不借助這一新定理也能得到所需結論，論文因此同時保留了兩條路線。
04. 誰來理解機器寫下的證明？
就在 Axiom 發佈成果的前一周，陶哲軒與鄧煜在非營利機構 SAIR 基金會（SAIR Foundation）的播客中討論了 AI 與數學的關係。OpenAI 的批次發佈此前已在數學界引發激烈爭論，9 月，兩人與其他 23 位菲爾茲獎得主聯名發表聲明，批評 AI 公司把攻克數學難題當作模型能力的基準測試。
鄧煜在對談中區分了兩條邊界：一條圈定已經有證明的問題，另一條圈定人類能夠理解其證明的問題。過去，兩條邊界幾乎重合，有證明就有人懂；但如今出現了只有 AI 才懂的證明，兩條邊界開始分離。
他認為，AI 能把事情做好的前提，是人類已經充分理解問題、手裡有證明的整體思路。陶哲軒則把 AI 公司批次解題的產出形容為模型訓練中的某種“有毒廢料”，最終要由數學家來消化處理。他希望 AI 公司在項目啟動之初就請數學家加入，避免事後由學界收拾殘局。
CFSG 項目和兩人描述的理想狀態有不少重合之處。它處理的是一份已有路線圖的證明，第一代證明和第二代證明的多卷著作為智能體指明了方向；原始證明的參與者在關鍵節點介入，並將繼續以顧問身份參與勘誤整理。形式化過程也從方法層面回應了數學界對 AI 證明難以核驗的擔憂。
今年 6 月，得到國際數學聯盟（IMU）支援的《AI 與數學萊頓宣言》將結果不可靠列為 AI 帶來的風險之首，並強調人類應當為數學結論的正確性負責。
CFSG 被多個數學細分領域引用了幾十年，但它卻一直分散在數百篇論文中，沒人能完整核驗所有結論。如今，所有前提條件、推導依賴都變成了可追溯的程式碼，任何研究者可以順著依賴鏈查到每一步論證的源頭，也可以直接復用已完成的數學模組開展後續研究。正如 Axiom 在公告中所寫：這不是故事的終點，群論領域的工作仍在繼續。
數學的可靠性長久以來建立在同行之間的信任上，人們相信審稿人讀懂了論證，相信前人沒有出錯。
但當越來越多的證明出自機器之手，這份信任需要新的支點，比如一份任何人都能重新運行、逐步核對的形式化證明。如果 AI 能接手繁瑣的驗證過程，數學家就能留出更多心力解決機器尚不擅長的事：提出值得追問的問題，同時在證明之外尋求理解。 (DeepTech深科技)