AI 新聞 2026年10月29日

本週 · 研究頁 10 月 26 日

Axiom 自稱 24 天把證明翻成 Lean 程式

AI 數學公司 Axiom 說 24 天把一條 15,000 頁的數學證明寫成可機械檢查的 Lean 程式，推導由機器查，定理寫得對不對仍由人看

為什麼重要： 本報推論：把既有證明翻成 Lean 變快了，留給人核對的是定理本身有沒有寫對。

AI 數學公司 Axiom 10 月 26 日在研究頁宣布，用 AI 代理群完成有限單群分類定理第一代證明的 Lean 形式化。這條定理把所有有限單群列成清單。

Axiom 做的是把既有證明翻成機器能檢查的形式，不是新證明。原證明約 15,000 頁，由約 100 位數學家跨世代完成。Axiom 把這份證明翻成 Lean 定理證明器能逐步機械檢查的程式碼，約 4,310 萬行。10 月 2 日第一批代理群上線，歷時 24 天，由公司的工程師與數學家指揮數十個代理群。研究頁沒有說用了哪個模型，也沒寫人與機器各寫了多少行（Axiom 研究頁，2026-10-26）。

Lean 保證從前提一步步推到結論沒有錯，但前提與結論寫的是不是原定理要說的，仍要人讀。研究頁寫，人檢查主定理的陳述與主定理用到的定義，確認陳述表達了預期的分類，Lean 檢查建立主定理的形式推導；過程中找出 34 處與已發表文獻的偏差，另頁列勘誤，每一處是筆誤還是漏洞，研究頁沒寫。程式庫公開，說明檔自稱沒有未完成的占位、只用三條標準公理（GitHub AxiomMath/CFSG）。

還不能當真： 全是 Axiom 自述，沒有獨立團隊建置成功的回報 怎麼查的 →

接下來看 Lean 社群或 Mathlib 維護者有沒有公開的建置回報。任一獨立團隊建置失敗、找到未完成的占位，或指出主定理陳述與標準定義不符，「完成」就要收回。