AI 掀桌：AI 说「已验证」的数学证明，和你以为的不是同一份
· AI Hot 编辑部
代码验过了，验的就是原来那道题吗？本文围绕 Axiom Math 发布的 Stacks 形式化工作，结合有关形式化忠实性的论文，拆开“机器检查通过”和“忠实表达原证明”的区别。这是历史事件解读，不是新的数学突破快讯。
「已验证」被偷换了。Lean 编译通过只证明形式语言里的那段逻辑自洽，不证明它忠实对应了人写的那份证明——剑桥与伦敦国王学院团队用约两周时间，在 OpenAI 的 Navier-Stokes 证明里找出英文版要求 m+4 而 Lean 版只要求 m+5 这类真实错配。OpenAI 719 篇数学手稿里只有约 42% 的顶级结果完成了形式化，其 README 明确写着未形式化的结果「可能有 issues」。
“已验证”三个字，最容易把两道验收揉成一道：代码里的证明能否通过检查，以及它是否忠实表达了原来的数学陈述。本文回看 Axiom Math 的 Stacks 形式化工作，以及有关形式化忠实性的论文。把这两件旧事放在一起，是为了看清验证的边界，不是宣布今天又发生了一次突破。
1. 桌子一：88 小时和两周之间，差的就是这一整篇
9 月 8 日 OpenAI 公布 Navier-Stokes 方程有限时间 blowup 的证明，出了两版：一份人写的论文，一份机器能验的 Lean 代码。据 New Scientist 报道，agent 花 88 小时生成了这份证明。
10 月 6 日，剑桥和伦敦国王学院三个人发 arXiv 论文，说两版对不上。他们花大约两周才找到一处真实差异——先让 ChatGPT 列疑似点，再人工核。Hansen 说：没说自然语言那份证明是错的，也没说它对的。
差在哪：Lemma 8.6，英文版要求某个量小于 m+4，Lean 版要求小于 m+5，后者更弱——就像「x 小于 4」和「x 小于 5」都能编过，说的不是一回事。
2. 桌子二：「已验证」验的不是你以为的那件事
Lean 是证明助手：代码编译通过，说明这段逻辑自洽，没有 sorry，没有偷加公理。它不负责另一件事——这段代码说的是不是英文那份证明。
那篇论文两句狠话。一句是规则：Lean 编译通过，不蕴含语义被保留。另一句是定理：要让数学英文的翻译语义忠实，得先解决文本歧义，而这问题的 SCI 是无穷大——比停机问题还高。
错配怎么来的：验收标准就是「能编译」，哪段不过就绕路改语义去过编译。原论文写得更直接——自然语言那份可能是错的而「翻译」后是对的；也可能两边都对但是完全不同的两份。
所以厂商说「已验证」，省掉的是最贵的一段：语义对齐和人工读稿。不是 Lean 的毛病，是营销偷划了一个环节。
3. 桌子三：42% 这个数字，比 719 更该看
一是形式化比例。这批手稿放上 GitHub（openai/math）时是 719 篇，README 自己写约 42% 的顶级结果完成了形式化，history.md 里 10 月 7 日那次更新写得更清楚：300/719 约等于 42%，剩下近六成没有 Lean 对照。二是透明度：TechCrunch 报道 719 篇里只有 10 篇附了思维链，我数了 reasoning_traces 目录，10 个 PDF、1 个 tex，对得上。
更要命的是 README 那句：Some of the unformalized results could have issues——没形式化的结果可能有毛病。同一份 README 还说，这些最好被当成原始研究数据。
10 月 7 日那次更新，OpenAI 自己撤了 3 篇手稿——一个符号错误让稳定化迹抵消论证失效，连带两篇一起撤，同时修了 14 篇。撤稿说明流程在跑，也说明那天还不到能直接引用。
4. 桌子四：Axiom 那一侧，也不是白捡的
11 月 4 日 Axiom Math 放出 Stacks Project 的完整 Lean 形式化，约 1600 万行，Axiom 说这是最大的整合式形式化数学库。对比扎眼：OpenAI 那 719 篇是模型现写的，Axiom 这份是把人类攒了二十年的库翻成机器能读的形式。
但翻的过程不干净。Axiom 自己写：系统暴露出 Stacks 里几十条陈述需要局部修正——缺假设、正特征下的边界情况，以及按原文的全一般性写下去根本不成立的断言。
这 1600 万行站在谁的肩膀上？Stacks 是 de Jong 2005 年发起、二十多年几百位数学人攒出来的；Axiom 说形式化也依赖 Lean 和 Mathlib 社区的库。AI 干的是平移和集成，不是发明地基。
Axiom CEO Carina Hong 那句「开头就 slop drop、后面 agent 就很难把边界撑大」——反过来读更像提醒：AI 越能往前跑，地基越是别人几十年的东西。
5. 桌子五：数学家自己写的规矩，比厂商的词靠谱
高等研究院主办的 AGMAI 顾问组，九位研究员，9 月 29 日发《负责任地发布 AI 生成的数学》，征求 600 多条回复。第一条请求就不客气：别在专有模型上测试高级数学问题。第二条要厂商在没有人类理解时负责让人类理解跟上，包括掏钱；第三条是人类理解必须由社区长出来。
剑桥的 Circelli 对 New Scientist 说得更白：形式化是想取代同行评审，但这篇论文说明 AI 自动形式化起不到同样作用。
另一边，11 月 5 日 arXiv 有篇 ProofTrace，用 8281 篇论文、五个 cohort 造了一套识别 AI 参与证明的图结构特征：AI 生成的证明引用外部结果更少、更依赖中间结论。它还有个发现——文本检测器被 AI 改写一过就崩，它这套却稳。「AI 味」可以洗白，证明结构洗不掉。
6. 普通人、builder 该怎么办
以后看到「已验证」「形式化验证」，先问三句：验的是英文那份还是代码那份？覆盖率多少？有没有一个署名负责的真人？答不上来，就当没验。
builder 迁移到代码，这毛病长得一模一样。CI 绿了不等于需求实现对了；Lean 编译过了不等于证明说的是你要的那件事。你们内部大概也有一堆「机器检查通过」但没人读过的东西。OpenAI 那次覆盖率 42%，你们那个数字是多少？
还有一条更实际的：别把厂商的「已验证」抄成自己的卖点。答不上那三问，你卖的就是被偷走的那个环节。
「已验证」是 2026 年 AI 圈最贵的词，也是最容易被省略掉的那一段。Lean 确实能把逻辑钉死，这是真本事。但从英文到 Lean 那一步、从 Lean 回到人话那一步，还得有人走。数学界这回没等厂商给标准，自己攒了 600 多条回复写成规矩——跑得快不算本事，出问题知道自己错在哪儿才算。