2026-10-31 05:39:57
AI 在 24 天內完成 CFSG 的 4000 萬行形式化證明
據格隆匯 10 月 31 日消息，Axiom 的多智能體 AI 系統完成了對有限單群分類定理（CFSG）這項人類規模最大的數學證明的形式化驗證。這項定理的證明歷時超過一個世紀，由全球 100 多位頂尖數學家撰寫，共 15,000 頁，而 AI 系統僅用 24 天便完成了全部形式化工作。這項工作產生了一個超過 4,000 萬行的 Lean 程式碼庫，現已成為以程式碼行數計算規模最大的開源軟體專案，超越 Linux kernel、Chromium、Firefox、LLVM、GCC 和 FFmpeg。AI 系統也找出了原始人類證明中的缺漏，並提出新的數學定理來彌補這些缺漏。
