AI辅助数学验证新进展：FormaTheoria完成四个关键定理Lean形式化

由清华大学求真书院领军班学生及丘成桐数学科学中心、智能产业研究院和华威大学研究团队提出的FormaTheoria项目，截至2026年8月已完成四个关键定理的Lean形式化，产出超过99.4万行相互关联的代码化数学理论，成为验证有限单群分类这一庞大证明工程的重要里程碑。

有限单群分类是现代数学中规模最为庞大的证明工程之一，由上百位数学家耗时数十年接力完成，总篇幅接近两万页，远超单人乃至单个团队能够完整复核的边界。在丘成桐先生的倡导下，该项目提出数学研究人工智能辅助工作流：让AI从原始数学文献出发，自动梳理依赖关系、整合知识体系并构建形式化证明，最后交由Lean证明助手逐步核验。

2026年1月22日，FormaTheoria首次提交代码，至2026年8月2日已打通延伸至Bender–Suzuki定理的关键理论链条，依次完成了Feit–Thompson奇数阶定理、Glauberman Z*定理和Brauer–Suzuki定理的证明。这四个定理构成有限单群分类中相互衔接的重要路线。项目快照显示，其拥有超过850个代码文件，查阅15部书籍与论文、共1037页，形成包含30298个数学声明和186187条依赖关系的证明网络。

以往大规模数学形式化高度依赖人工投入，例如Feit–Thompson定理此前的Rocq形式化版本由约15人耗时六年完成，而FormaTheoria在七个月内完成了该人工项目的全部内容，并拓展至其他定理。形式化过程还发现了原始文献中的不一致定义、遗漏条件、下标误差等问题，部分问题可自动修正，证据不足的则交由数学家判断。项目距离完整验证有限单群分类仍有很长的路，但已展示AI在超长程数学工程中的推进能力。