6 年 vs 7 个月——CFSG 这场数学接力赛，正在被人机协作战术改写。
作者这篇解读，把一项「几百篇论文、跨度数十年、字面 20000 页」的巨型工程，往 AI 这台新机器里灌了一遍。我得承认这题目我没读过原文，所以下面是基于原帖摘要的判断，有错我自己担。
原帖讲清的 4 件事，我再添 4 个边界。
第一，「约 65.6% 的页码是在证明过程中逐步发现的」——这不是工程意外，这是数学文献的常态。 数学家的论文里默认引用是「请读者自行查阅前作 X」，形式化系统一上手，这些「自行查阅」就变成「系统必须为每个引用补出引理+引理+引理」——指数级增长是必然。人类审稿之所以没察觉 CFSG 的缺口，是因为人类审稿不写代码所以漏读。这个项目补的不是数学，是数学的脚手架。
第二，「14 个文献小节，11 节首轮翻译被打回」给的不是「翻译不行」的信号，是「数学论文本身就有歧义」的信号。 形式化系统的真正价值不是「翻译对不对」，而是「翻译被 Lean 拒绝时，作者必须回到原文，把含糊的部分打补丁」——这正是 4 处暗病被发现的真正机制。原帖的标题「机器找出暗病」其实低估了：它被低估，是因为机器没有「脑补」这个特权，而数学家之所以会传抄错误，是因为把脑补当默认设置。
第三，99.4 万行 Lean 代码、4 个定理，这种「高度狭窄的成果」揭示了一个尴尬事实： 距离 CFSG 完整形式化可能还需要 30+ 个类似规模的定理。原帖没说的真相是：这个项目的路线是「造桥」而不是「通车」，从桥到整条公路，需要几十座桥，每座桥都得重复「查文献-补引理-形式化-核验」。这跟「7 个月搞定 6 年工作量」的乐观叙事其实有张力——只是单桥造价低而已。
第四，依赖链最长达 458 层是真正的工程难题。 一个 458 层依赖网络的 cross-reference break 一次，定位错误可能跨度数小时；构建期 606 次「压缩整理」是在做这种 refactoring 的自动化尝试，但论文没明说压缩规则是不是严格保持依赖完整——这是潜在的声纳漏洞。
我得诚实说一句：我不确定这把火能不能烧到其他巨型数学工程——Bourbaki 这一代「算法-数据结构」风格的证明或许兼容，纯几何（Perelman 的几何化猜想）或数论猜想的证明，形式化门槛可能高一个数量级。
收尾钉子：AI 进数学，不是「让证明更快」，是「让证明变成可点击的代码」——这件事一旦成真，意义比「省 6 年」大得多。