科技日报记者 都芃
有限单群分类（CFSG）是现代数学中规模最为庞大的证明工程之一。其相当于有限对称结构的“基本零件清单”，大量重要数学结论建立在该理论之上。围绕该理论，上百位数学家历时数十年接力完成证明，但成果散落在数百篇论文、专著中，总篇幅接近两万页，仅靠人工难以实现完整核验。
日前，在丘成桐倡导下，来自清华大学求真书院领军班的聂天骄、张傲、汤瑀森，清华大学丘成桐数学科学中心副教授周源、清华大学智能产业研究院副研究员李鹏以及华威大学副教授Damiano Testa组成团队，提出了AI辅助形式化证明构造工作流——FormaTheoria。
该系统直接从原始数学文献出发，自动梳理知识依赖关系、整合数学体系，生成可由Lean证明助手核验的形式化证明，有效推进有限单群分类的机器核验工作。截至2026年8月，FormaTheoria已完成四个关键定理的Lean形式化，产出超过99.4万行互相关联的代码化数学理论，成为通往CFSG完整机器验证的重要里程碑。
不同于多数AI数学系统“题目、定义工具预先就绪，AI仅负责寻找证明”的工作机制，FormaTheoria需要从零散文献中重建数学基础，面临分布式依赖、跨源定义错位、语义保真、原始文献自身缺陷四大技术难点。
针对超长工程周期，FormaTheoria可维护持续更新的证明地图，把大目标拆解为辅助定理，成功结果向上汇总，记录失败路径避免重复“踩坑”；采用依赖感知并行策略，独立任务并行运行；公共前置结果只需计算一次即可供多任务复用，会产生全局影响的公共数学内容串行修改，规避冲突。
对照实验表明，该策略较以往方法实现了4.2倍效率提升。项目快照显示，其已产出99.4万余行Lean代码、850余个代码文件，累计研读15部书籍论文，合计1037页文献。
虽然当前进度离有限单群分类完整形式化这一目标仍有较远距离，但该项目证实了AI智能体可以在数月的时间尺度上维护百万行级别形式化数学体系，跨大量文献追踪复杂依赖，构建连通的大型数学理论，能从求解孤立数学题目，拓展到系统性数学知识建构。
目前，该工作已产出一套可迭代复用的数学基础设施：形式化代码记录每条结论的依赖、文献衔接方式、勘误记录。未来搭配检索、可视化工具，可帮助研究者理解CFSG整体架构，复用已有成果，辅助数学家发现新联系、新定理。
FormaTheoria项目组希望借此探索一种面向AI时代的人机协作模式，即人类负责确定值得研究的问题并作出关键判断，AI承担大规模搜索与推导，形式系统则确保每一个被接受的步骤都可以被重新检验。当一项证明庞大到任何个人都难以从头复核时，这三者结合的方式，或许将成为人类管理超大规模数学知识的一条全新路径。
网友评论
