Axiom 稱 AI 代理已在 Lean 中將有限單群分類定理形式化

AI 數學公司 Axiom 在 X 上宣布，已完成有限單群分類定理的 Lean 自動形式化，並稱這項成果是「對稱性的週期表」。Axiom 表示，原始證明約有 15,000 頁，由數代共 100 多位數學家撰寫，並稱這是史上經電腦驗證的最大數學證明。

根據 Axiom 的開源儲存庫，AI 代理群在 24 天內產生約 4,310 萬行 Lean 程式碼，涵蓋 715 篇論文與書籍，並標出 34 處與已發表紀錄不符之處。AI 新聞帳號 TestingCatalog 的貼文補充說，這些代理像軟體團隊一樣分工，寫程式碼的速度比 Lean 檢查程式碼還快。

這些數據是 Axiom 單方面的說法；公告中未包含任何對這項形式化成果的獨立審查。截至 10 月 28 日，該貼文在 X 上約有 6,200 個讚。