AI 一年写掉几千万行形式化证明之后，Lean 社区开始盯「检查器本身可不可信」

形式化证明在今年变成了工业量级：据 Thomas Hales 十月初的公开长文，Math Inc. 在 2026 年 3 月给出 24 维球堆积的 autoformalization（约 50 万行源码，golfing 后压到约 20 万行），Meta/FAIR 的 ATLAS 项目把 26 本数学教材的大部分形式化，Anthropic 九月四日宣布的费马大定理形式化在 11 天里产出 1300 万行 Lean，OpenAI 九月八日的 Navier-Stokes 结果也配了 Lean 版本。量一上来，问题就从「能不能自动形式化」转成「能不能信这个检查器」。今年夏天 Lean 官方内核接连爆出 soundness 缺陷：7 月底的 #14576 让内核有可能接受 False 的证明（只能经元编程触达，前端会拦住）。Lean 维护者 Leonardo de Moura 的复盘还提到，OpenAI 的 Daniel Selsam 用内部模型找出了若干同类缺陷，全部已被 nanoda 这个独立检查器捕获，也都已修复。Hales 文章里最实操的一条提醒是：光过内核不够，还要防「证的东西不是你想证的那个」，并该用 comparator 与外部检查器复检。