清华 FormaTheoria 用 AI 形式化 CFSG 四定理

清华求真书院与丘成桐数学科学中心、智能产业研究院、华威大学的研究团队提出 **FormaTheoria**——一套让 AI 从原始数学文献出发、自动梳理依赖关系并构建形式化证明的工作流。

截至 2026 年 8 月，它已完成**有限单群分类(CFSG**)中四个关键定理的 Lean 形式化：Feit–Thompson 奇数阶定理、Glauberman Z* 定理、Brauer–Suzuki 定理与 Bender–Suzuki 定理，产出超过 **99.4 万行可核验代码**。

💡 为什么值得看AI 7 个月产出 99.4 万行 Lean 代码，并发现原文献错误。