AI 代理 24 日驗證萬頁數學證明

AI 代理把 15,000 頁證明轉成電腦可檢查版本

據 Axiom Math 美國時間 10 月 26 日發表的研究文章，這間總部設於美國 Palo Alto 的初創，用數十個 AI 代理（能自行執行多步驟任務的 AI 程式）在 24 日內，把「有限單群分類定理」完整轉寫成證明輔助程式 Lean 的程式碼，公司稱這是該定理首個完整的電腦檢查證明。

Lean 是一種程式語言，數學家把證明寫成程式碼後，電腦會逐步檢查每一步推理是否成立。把人手寫成的證明轉成這種格式，稱為「形式化」。

有限單群分類被稱為「巨大定理」

有限單群是對稱結構最基本的組成單位，好比化學的元素周期表；分類定理列出所有可能的有限單群。據 Axiom 的文章，原有證明約 15,000 頁，散落在 500 多篇論文，由約 100 名數學家花數十年完成，因篇幅龐大被數學界稱為「巨大定理」（Enormous Theorem）。

過程找出 34 處與文獻不符

Axiom 表示，大部分不符屬於筆誤、表格錯誤或漏寫前提。最嚴重的一處涉及「不平衡群定理」：AI 代理在數學家 John Walter 1986 年的專著中，找到其中一個推論的反例。公司表示，這些反例並未推翻該定理，團隊改用另一條證明路線，並由其 AI 系統 AxiomProver 證明了一條新定理補上缺口。

程式碼已在 GitHub 以 Apache 2.0 授權公開。公司表示，形式化跟隨第一代證明，第二代證明仍未完成；部分輔助結果亦未在今次工作中形式化。

仍未有外界獨立重建

Axiom 創辦人兼行政總裁 Carina Hong 接受 Runtime Wire 訪問時表示，暫時未有公司以外的人獨立建置及檢查整個證明，公司公開建置檔案，正是希望外界自行重現。Axiom 的文章亦提醒，Lean 只檢查推理步驟，形式化的定理陳述是否準確表達原有分類，仍需要數學家審閱。

來源

• Formalizing the Enormous Theorem（原始文件）
• AxiomMath/CFSG: A Lean formalization of the Classification of Finite Simple Groups（GitHub）
• Axiom publishes Lean proof artifacts to support independent reproduction（Runtime Wire）