🎯 科技 · AI+数学

🔥 AI正从"回答问题"进化为"完成复杂任务"，数学证明领域迎来历史性突破

一、AI写代码验证数学，这不是科幻

近日，清华大学丘成桐数学科学中心宣布了一项里程碑式进展：在菲尔兹奖得主丘成桐倡导下，团队开发出的AI辅助形式化证明工具FormaTheoria，已产出超99.4万行相关联的代码化数学理论，完成了有限单群分类（CFSG）中4个关键定理的形式化证明。这一成果被学术界视为通往CFSG完整机器验证的重要里程碑。

有限单群分类是什么？如果把所有数学运算结构想象成无数复杂的"几何体"，那么有限单群就是组成"几何体"的最基础最小单元"积木"。CFSG相当于这样一张"积木清单"，几乎所有复杂代数问题都建立在这张清单之上。百余位数学家接力数十年，成果散落在数百篇论文与专著中，总篇幅接近两万页。

二、AI不只是做题，而是重建知识体系

FormaTheoria的创新之处在于，它不是面对一道已经准备好的数学题给出答案，而是直接从原始零散文献出发，自动梳理知识依赖关系、整合碎片化数学体系，最终生成可由Lean证明助手核验的形式化代码。这意味着AI要从"答题机器"进化为"知识建筑师"。

团队面临四大核心技术挑战：事先无法得知需要查阅多少文献、不同来源文献难以统一兼容、无法判断是否忠于原文、原始文献存在原生缺陷。FormaTheoria通过建立"证明地图"——把大目标拆解为辅助定理，成功结果向上汇总，失败路径记录以避免重复踩坑——实现了相互独立任务的并行运行，获得4.2倍加速效果。

三、数学与AI的交叉正在重塑科研范式

这项成果的意义远超数学本身。它证明了AI具备处理极端复杂、跨学科、长周期知识体系的能力。当AI能够自主从原始文献中重建数学基础时，它不仅在验证定理，更在重新定义人类探索知识的方式。丘成桐团队的工作表明，AI正从工具变为科研合伙人，数学这一最古老的人类智力活动，正在与最前沿的人工智能技术深度交融。

综合清华大学官网、科学网、科技日报报道 | 2026年9月5日