7个月超15数学家6年工作量，AI写下百万行代码挑战核验超大数学证明工程

AI系统FormaTheoria在7个月内完成有限单群分类（CFSG）中四个关键定理的Lean形式化，生成超99.4万行可核验代码，构建含3万余声明、144万依赖关系的证明网络，实现对散见数百篇文献的自动梳理、定义对齐、漏洞识别与机器核验，标志着AI首次系统性参与超大规模数学基础证明的重构与验证。