有限单群分类（CFSG）被视为现代数学中规模最大的证明工程之一。整个证明由上百位数学家历经数十年接力完成，成果分散在数百篇论文和专著中，总篇幅接近 2 万页，早已超出单个研究者或单个团队可以完整复核的范围。在这一背景下，借助 AI 做大规模形式化验证，成了必须尝试的路径。
在丘成桐倡导下，来自清华大学求真书院领军班、丘成桐数学科学中心、智能产业研究院和华威大学的研究团队提出了 FormaTheoria。这一工作流试图让 AI 直接从原始数学文献出发，自动梳理依赖关系、整合知识体系、构建形式化证明，再交由 Lean 证明助手逐步核验。
截至 2026 年 8 月，FormaTheoria 已完成 4 个关键定理的 Lean 形式化，累计产出超过 99.4 万行彼此关联的代码化数学理论。论文称，项目距离完整验证有限单群分类仍有很长距离，但这一步已成为通向最终目标的重要里程碑。
CFSG 为什么值得做机器核验
“有限单群分类”听上去抽象，它处理的核心问题可以理解为有限对称性的“基本零件清单”：任意复杂的有限对称结构，经过层层拆解，最终会落到一批无法继续拆分的基本单元；CFSG 的作用，就是给出这些基本单元的完整列表。
数学研究处理复杂问题时，常常先把问题拆到这些基本单元，再依据 CFSG 提供的清单逐类处理。也正因如此，CFSG 实际上成了大量后续证明可以直接调用的基础设施。若这套基础设施内部存在漏洞，建立在相关结论之上的许多成果都可能受到影响。
一些专业综述已经给出量化层面的旁证。美国数学会在 2018 年出版 Stephen D. Smith 的专著《Applying the Classification of Finite Simple Groups: A User’s Guide》，全书 231 页，共 10 章，用来梳理 GFSG 的应用场景。书中最后两章的公开目录列出 14 个带编号的应用专题，包括距离传递图、Frobenius 猜想、置换群算法、有限生成群的子群增长、域扩张、黎曼曲面覆盖、群论中的 Waring 问题、扩展图和近似群等。
国际数学界的高层级会议也给出过直接体现。2014 年国际数学家大会邀请美国数学会 2018 年 Cole 代数学奖得主 Robert Guralnick 作题为《Applications of the Classification of Finite Simple Groups》的专题报告。
这些应用里也包含影响深远的重要成果。CFSG 是限制 Burnside 问题完整证明链中的关键环节，Efim Zelmanov 因解决这一问题获得 1994 年菲尔兹奖。Smith 的专著还将有限单群上的 Waring 问题和扩展图列为 CFSG 的重要应用方向，相关代表性论文发表于《Annals of Mathematics》。
论文据此指出，CFSG 已经支撑起一批获得顶级学术奖项、发表于顶级期刊的重要工作。随着下游成果持续累积，验证这套底层系统的正确性和可复核性变得越来越关键。对 CFSG 做可追踪、可重复的机器核验，意义已不局限于群论本身。
困难同样明显。CFSG 的证明来自不同时代、不同作者和不同文献，符号、定义和默认条件并不统一，一处引用往往还会通向另一整套文献。历史上，分类证明中的一个重要缺口，直到 20 多年后才由两卷、共 1220 页的专著补齐。FormaTheoria 不只要核验单步推理，还得检查数百篇文献之间的定义、条件和引用能否无缝衔接，最终形成没有断点的证明链。
FormaTheoria 如何处理超大规模证明
许多 AI 数学系统面对的是一道已经准备好的题目，定义、条件和工具都已齐备，系统只需寻找证明。FormaTheoria 面对的情况不同。它需要先从零散文献中重建题目背后的数学基础，再完成证明本身。
论文将这项工作的难点归纳为四个方面。
资料范围并不预先确定
系统在开始时并不知道需要查阅多少资料。一条引用可能牵出另一篇论文，那篇论文又会引出更多前置工作。项目最初只有 3 个主要来源，推进过程中又发现了 12 个来源；后续补充材料占全部查阅页码的 65.6%。FormaTheoria 的做法是，一旦发现某个前置定理缺失，就暂停当前证明，先查找并形式化依赖项，再回到原任务继续推进。完成核验的结果会被存入统一知识库，供后续证明反复调用。
不同文献很难直接拼接
不同作者采用的定义、符号和默认条件并不一致。两个定义在数学意义上也许等价，但写进 Lean 代码后却可能互不兼容。FormaTheoria 需要反复对照原文与现有代码，建立必要的转换关系。同时，系统会保护已经核验过的数学陈述，并检查每一次修复是否影响后续证明。这样，多部原本相互独立的著作和论文才有机会逐步汇入同一套理论框架。
代码通过检查，不等于忠实还原原文
Lean 只负责检查逻辑是否自洽、结论能否由前提推出，但它不会判断结论是否忠实对应原始文献。AI 可能漏掉某个条件，混淆“所有”和“存在”，也可能把结论改错。为此，FormaTheoria 设置了一道独立审查环节：先由翻译组件写出 Lean 陈述，再由审查组件逐项对照原文核验。在论文分析的 14 个文献小节中，有 11 个小节的首轮翻译被退回修改。这一独立审查机制成了机器核验之外的第二道保险。
原始文献本身也可能有问题
旧文献可能出现排版错误、条件缺失或表述含混。FormaTheoria 会保留原始页面，等到后续证明出现矛盾时再回溯排查。如果文献足以支持修正，系统就补充条件或建立兼容关系；证据不足时，则记录问题并交给数学专业人员判断。
除这四点外，项目还要解决超长周期任务管理。一次对话不可能容纳完整任务，因此 FormaTheoria 用一张持续更新的“证明地图”管理进度：把困难目标拆解成较小的辅助定理，成功结果逐层汇回主定理，失败路线也会记录在案，避免系统反复进入同一条死胡同。
并行策略也经过专门设计。相互独立的任务可以同时推进；多个任务如果依赖同一个前置结果，系统只完成一次，再允许其他任务复用。那些可能牵动大量后续内容的公共数学部分，则按顺序逐个修改，以减少冲突。论文中的对照实验显示，这种依赖感知的并行方式在测试任务上实现了 4.2 倍加速。
从文献检索、依赖补齐、原文翻译、证明构造，到机器核验、独立审查、冲突协调，再到把无法确定的问题交给数学专业人员，FormaTheoria 形成了一条完整工作链。论文将这种设计视为对超大规模证明工程真实难题的直接回应，其目标是把分散的数学文献逐步连接成可检查、可追踪、可持续扩展的理论体系。
7 个月完成 4 个关键定理形式化
根据论文记录，FormaTheoria 于 2026 年 1 月 22 日首次提交代码，到 2026 年 8 月 2 日，已经打通一条延伸至 Bender–Suzuki 定理的关键理论链。在这条路径上，项目依次完成了 Feit–Thompson 奇数阶定理、Glauberman Z* 定理、Brauer–Suzuki 定理和 Bender–Suzuki 定理的证明。
这 4 个定理并非彼此孤立，而是有限单群分类中一条相互衔接的重要路线。后一个定理的证明，往往建立在前面定理所沉淀的大量数学基础之上。
论文给出的项目快照包括：
- 超过 99.4 万行 Lean 代码；
- 超过 850 个代码文件；
- 系统共查阅 15 部书籍与论文、共 1037 页，其中约三分之二是在证明推进过程中逐步发现的。
代码行数只能说明工程体量的一部分。若以 Bender–Suzuki 定理为终点向前回溯，项目已经形成一张包含 30298 个数学声明、186187 条依赖关系的证明网络，最长依赖链达到 458 层。若把 Lean 基础库中的相关内容一并计入，这张网络会扩展到 74922 个声明和超过 144 万条依赖关系。
论文据此认为，近百万行代码背后并非简单堆积，而是一张结构复杂、联系紧密的证明网络。研究也显示，在机器核验与分层审查配合下，AI 智能体已经能够持续推进大型、超长程的数学工程。
项目的实际运行过程同样呈现超长程特征。论文记录的一次最长智能体执行持续了 9.17 天，期间系统对累积信息进行了 606 次压缩整理，同时始终保留当前证明目标、已完成结果和待解决问题。论文借此说明，项目管理的是一张不断演化的长程证明网络，单次生成或一次对话都不足以覆盖完整过程。
与既有人工形式化项目相比，时间差异也很明显。论文给出的历史参照是，Feit–Thompson 定理此前的 Rocq 形式化版本由大约 15 人耗时 6 年完成；而 FormaTheoria 在 7 个月内完成了该人工项目的全部内容，并把形式化工作继续推进到其他关键定理。对一次 AI 智能体任务而言，7 个月依然很长，但与传统人工形式化相比，AI 的介入明显缩短了项目时间尺度。
形式化过程让文献中的问题暴露出来
数学文献通常写给熟悉该领域的研究者。作者会省略前文已出现的条件，也默认读者能够识别不同定义之间的等价关系。排版或符号层面的细小错误，在人工阅读中也常被自然忽略或自行纠正。FormaTheoria 的做法不同。它把文献逐条翻译为 Lean 代码，要求每个定义、每个条件和每一步推理都写得明确无歧义。也正因为要逐行核验，原始文献中原本不易察觉的问题会直接暴露出来。
论文详细记录了项目发现的多种问题，包括不同资料对同一概念给出不一致定义、定理陈述遗漏必要条件、整除条件位置写错，以及证明中的下标误差。部分问题可以依据上下文自动修正，证据不足的则交由数学家判断。
“类型 I 极大子群”定义差异
一个典型案例来自两部关于奇数阶定理的资料。两部资料都定义了“类型 I 极大子群”，但其中一部要求某个性质对“每一个补结构”成立，另一部只要求“存在一个补结构”满足该性质。形式上，前者比后者更强，因此两套定义无法直接对接。FormaTheoria 在形式化过程中识别出这一区别，随后借助 Schur–Zassenhaus 定理，证明两种定义在这里实际等价，从而把两部文献连接起来。
Peterfalvi 引理遗漏前提条件
另一个案例来自 Peterfalvi 的一条引理。该引理的正式陈述漏掉了“某个群的阶为奇数”这一前提条件，而后续证明又确实依赖该条件。尽管在后文应用这条引理时，前文已经保证了这一条件，整体论证没有中断，但 Lean 不会自动补足这层背景。FormaTheoria 在追踪引理的证明路径和使用位置后，把遗漏条件明确加入定理陈述，使整条形式化链更完整。
更直接的文献错误
项目还发现了更直接的错误。一处定义把本应出现的对象 H 写成了 M，两部参考资料都保留了同样的错误。Huppert 的一条定理则把因子 d 放进了错误的整除条件里；系统在找到反例后终止证明，并把问题交由数学家核查，人工随后确认了正确条件。Higman 的一段证明又把一组基向量的编号写成从 u₀ 到 uₘ，正确范围应到 uₘ₋₁，这一下标问题由系统在证明过程中自动识别并修正。
论文认为，这些案例说明，机器核验在大型数学工程中的价值不只是“把证明写成代码”。FormaTheoria 在构造形式化证明时，也同步对原始文献做细粒度审查：问题出现在哪里、后续证明需要什么条件、修正依据来自哪些文献、修正是否影响其他结果，都被逐一记录下来。对于由数百份资料相互勾连构成的 CFSG，这种可追踪机制把过去依赖读者经验补全的细节，转化成可以明确检查的数学依据。
项目状态与后续方向
FormaTheoria 目前尚未完成有限单群分类的整体形式化，距离最终目标仍有很长路要走。论文称，项目仍在加速推进，继续朝完整形式化这一现代数学中最庞大的证明工程之一迈进。
现有结果显示，AI 已经能够在数月时间里维护并扩展大规模数学环境，跨越多部文献追踪复杂依赖关系，并在严格核验下构建彼此连通、体量可观的理论体系。论文据此将 AI 的能力边界描述为：从求解孤立数学问题，逐步扩展到参与系统性的数学知识建构。
这项工作也在沉淀一套可持续扩展、可重复使用的数学基础设施。传统文献通常只能告诉读者“证明写在哪里”；形式化代码则进一步记录“每个结论依赖什么”“不同来源如何衔接”“哪些问题经过修正”，并把已核验的定义、引理和证明整理为可直接复用的知识模块。
论文还提到，若未来加入解释、搜索和可视化工具，这张知识网络可能帮助研究者更快理解 CFSG 的整体结构、复用现有成果，也可能为数学家探索新的联系和发现新的定理提供支持。
FormaTheoria 项目组希望探索一种面向 AI 时代的人机协作模式：人类负责确定值得研究的问题并作出关键判断，AI 负责大规模搜索与推导，形式系统则保证每一个被接受的步骤都可以重新检验。当一项证明庞大到任何个人都难以从头复核时，论文认为，这三者结合可能成为管理超大规模数学知识的一条新路径。
文中项目状态和定量结果，均来自论文所述的 2026 年 8 月完成时快照。