FormaTheoria 七个月完成四个关键定理形式化

清华大学求真书院领军班学生，以及丘成桐数学科学中心、智能产业研究院和华威大学研究团队提出 FormaTheoria，利用人工智能辅助超大规模数学证明的形式化与核验。2026 年 1 月 22 日首次提交代码后，项目在 7 个月内打通了延伸至 Bender–Suzuki 定理的关键理论链。

为什么核验有限单群分类

有限单群分类是现代数学中规模庞大的证明工程，由上百位数学家耗时数十年完成，成果散落在数百篇论文和专著中，总篇幅接近两万页。由于不同文献使用的定义、符号和默认条件并不一致，依赖关系也可能跨著作延伸，完整复核并非简单拼接即可完成。

形式化验证的目标，是把这些分散知识转化为可追踪、可重复检查的证明链。有限单群分类又被许多后续研究所依赖，因此其正确性不仅关系群论本身，也可能影响建立在相关结论之上的大量成果。

FormaTheoria 如何推进证明

FormaTheoria 从原始文献出发，依次完成文献检索、依赖补齐、命题翻译、证明构造、Lean 机器核验和独立审查。系统通过持续更新的证明地图拆解长期任务，并对相互依赖的工作进行协调。论文中的对照实验显示，其依赖感知并行策略在所测试任务上实现了 4.2 倍加速。

工程主要处理四类问题：前置资料数量无法预先确定；不同定义可能无法直接写入同一套理论；Lean 只能检查逻辑自洽，不能自动判断代码是否忠实于原文；历史文献本身也可能存在条件遗漏、整除关系或下标错误。为此，项目设置独立审查环节，在分析的 14 个文献小节中，有 11 个小节的首轮翻译被退回修改。

七个月形成多大工程

截至 2026 年 8 月 2 日，项目依次完成 Feit–Thompson 奇数阶定理、Glauberman Z* 定理和 Brauer–Suzuki 定理，并延伸至 Bender–Suzuki 定理。项目快照包括超过 99.4 万行 Lean 代码、850 多个代码文件，以及 15 部书籍与论文共计 1037 页材料，其中约三分之二是在证明推进过程中发现的。

以 Bender–Suzuki 定理为终点向前追溯，证明网络包含 30298 个数学声明和 186187 条依赖关系，最长依赖链达到 458 层。最长的一次智能体执行持续 9.17 天，期间进行了 606 次信息压缩整理。作为文中参照，Feit–Thompson 此前的 Rocq 形式化由约 15 人耗时 6 年完成。

审查发现与当前边界

形式化过程发现并修正了多处文献问题，包括同一概念定义不一致、关键条件遗漏、整除条件位置错误以及证明下标偏差。例如，系统识别出 Peterfalvi 一条引理遗漏了群的阶为奇数这一前提，并将其明确加入形式化陈述；Huppert 定理中的错误整除条件则在找到反例后交由数学家核查。

FormaTheoria 尚未完成有限单群分类的整体形式化。项目组希望进一步形成可复用的人机协作模式：由人类确定问题并处理关键判断，人工智能承担大规模搜索与推导，形式系统则保证每个被接受步骤能够重新检验。