AI 的 10 个数学证明，24 小时被驳回一个：「Lean 已验证」到底能保什么

8 月 1 日，OpenAI 一次性放出 10 个数学与理论计算机问题的结果，覆盖群论、算子代数、算术电路等八个领域。这次真正让圈内震动的不是结论本身，而是交付方式：每个结果都附带一份 Lean 4 形式化证明，社区管它叫「Lean 证书」。知乎

第二天，堪萨斯大学的 J. L. Nielsen 把其中 Connes 刚性猜想那份 37000 行 Lean 代码从头追到尾，给出两条互相独立的失败路径——AI 构造的「反例」里，有一个群根本不满足猜想题设的前提条件。证明的每一步都通过了机器验证，但它证的那个东西，不是原猜想。量子位

同一周还发生了两件事。Lean 官方刚复盘完一个内核可靠性漏洞，有 AI 在尝试推翻考拉兹猜想时，发现验证器一度能证明出 False。知乎8 月 16 日，OpenAI 又宣布新模型 Sol Ultra 在不到一小时内证明了图论的循环双覆盖猜想，并开放了 Lean 形式化仓库。知乎

20 天里，「Lean」这个名字在 AI 数学新闻里出现的密度，超过它诞生以来的任何一段时间。关注这个兴趣的你，大概率攒了一堆问号：Lean 到底是什么？「Lean 已验证」等于绝对正确吗？被驳回的那一个，是 Lean 的失败还是胜利？现在入坑学 Lean 4，值不值？

这段时间我把知乎、B站和几家科技媒体上的信号捋了一遍，替你拆开看。

先花一分钟搞懂 Lean 4 在链路里干什么

Lean 4 既是一门编程语言，也是一个证明助手。你写进去的数学证明本质上是一段程序，Lean 的内核像编译器一样逐行检查：编译通过 = 证明在逻辑上成立，没有「读起来像对」的模糊地带。

关键在两个设计。一是内核极小：真正负责判定的内核大约只有 5000 行代码，目标是「小到任何人都能从零重写一个」。Lean 本体庞大且功能不断增加，但判定环节被压缩到可以被人眼和独立实现交叉审计的尺寸——已经有人用 Lean 本身写了独立内核 Lean4Lean，也有人用 Rust 等语言实现。二是证明检查就是类型检查：证明写错，就是类型对不上，编译器当场拒绝。

这就是 OpenAI 要给每个结果配 Lean 证书的原因。AI 写证明最大的风险，是「看似合理的推导链条里悄悄跳了一步，谁都看不出来」，而 Lean 不接受任何语气上的笃定，少一步就是少一步。这次 10 个证明被放进 GitHub 仓库 openai/ten-proofs，Apache 2.0 协议，任何人两条命令就能全部编译，几分钟出结果，不必等几个月的人工审读。知乎

知乎上一位搞形式化方法的学生说得挺准：在《数学原理》出版 113 年后、Automath 出现 59 年后、Lean 诞生仅仅 13 年后，定理证明器似乎真的在实现它最初的夙愿。知乎

这 20 天到底发生了什么

「Lean 已验证」只守一层，拆给你看

把 Connes 事件掰开，会发现它其实是整个验收体系按设计工作的一次演示——只是结果和大众预期相反。

Nielsen 指出的问题不在推理链：Connes 猜想要求反例中的群满足两个附加条件（ICC 和 Kazhdan 性质 T），而 AI 构造的两个「不同构但代数结构相同」的群里，有一个两条都不满足。Lean 内核完美地验证了「关于这个对象的所有证明」，但这个对象压根不是题目要求的那个对象。量子位

陶哲轩对此有个被反复引用的说法：验证证明的是形式陈述本身，而不是这个陈述与意图相符。量子位形式化圈子里还有一句更狠的警句：最危险的不是一个失败的证明，而是一个对错误陈述的成功证明。一份针对五个常用 Lean 基准的审计曾给出 4833 条发现，包括空洞定理和不可靠公理——它们全部通过了机器验证，直到人类构造出反例，才被发现被证的那句话本身是错的。

所以「Lean 已验证」的信任链其实是四层，Lean 只负责其中一层：

1. 模型生成：AI 提出的数学想法对不对——Lean 管不了；

2. 形式化翻译：把自然语言猜想翻译成 Lean 命题时，前提、定义有没有丢失或走样——Connes 这次栽在这一层，Lean 也管不了；

3. 内核验证：证明的每一步是否合乎规则——这是 Lean 的辖区，这次它没失职；

4. 环境与版本：用哪个版本、有没有依赖元编程扩展、能否独立复现——同一周的内核漏洞事件提醒的正是这层。

顺带说下那个漏洞：有 AI 在尝试「推翻」考拉兹猜想时，发现了一条通过嵌套归纳类型和元编程触发的路径，可以在系统里证明出 False——在逻辑系统里，这意味着一切皆可证，是最高级别的事故。但后续处理是教科书级的：公开复盘、一小时内推送修复、补回归测试，连社区常用的独立检查器 nanoda 都被顺带查出另一个问题并提示升级。知乎可靠从来不是「永不出错」，而是出错后你能立刻知道哪一节链条掉了。这也是为什么，以后看到「Lean 已验证」四个字，值得顺手多问三句：哪个版本？形式化陈述和原题对得上吗？有没有被独立复验过？

硬币另一面：验证的成本结构真的塌了

如果只看到「被驳回」，会低估这 20 天。同一周，Lean 和 Z3 的创造者 Leonardo de Moura（现任 AWS 高级首席应用科学家、Lean 背后非营利组织 Lean FRO 的首席架构师）的访谈流出，里面几个数字值得记住：

• seL4：AI 出现之前的形式化验证标杆，一个约 8700 行的 C 语言微内核，验证花了约 20 人年，折合每行代码约 350 美元。知乎这就是 AWS 过去十年只敢把形式化用在最关键安全组件上的原因。

• lean-zip：de Moura 的同事 Kim Morrison 用 AI 把 C 语言压缩库 zlib 翻译成 Lean，并证明了「压缩再解压必还原原始数据」这条对压缩引擎最重要的性质——1100 多条定理、约 32000 行证明代码、没有任何未完成占位符，全程约一周。

• IMO：2024 年 DeepMind 的 AlphaProof 用 Lean 拿国际数学奥林匹克银牌时，社区觉得已是了不起的成就；到 2025 年，Harmonic 的 Aristotle 和字节跳动的 Seed-Prover 已经做到金牌水平。de Moura 说，金牌「现在被当成简单问题的基准」。

de Moura 自己的总结最直接：他已经不再写测试了，他写性质，然后 AI 替他证明。知乎

过去形式化验证最痛苦的不是初始投入（写程序花 x 时间，验证大约 10x），而是维护：代码一改，证明跟着崩，修证明比修测试难得多，因为你很可能已经不记得某条证明背后的逻辑。AI 恰好把「写证明」和「修证明」这两件最痛苦的事都接了过去。这解释了一个看起来矛盾的现象：AI 一边在生产需要被审查的结果，一边在把审查工具变得人人可用。

值不值：三种人，三个答案

最后落到「值不值得你花时间」，这是这篇想替你做的判断。

如果你是程序员，对形式化验证或高可靠软件有兴趣——现在的入场窗口是真实存在的。 过去劝退新人的三座大山（证明难写、难维护、学了没处用）正在被 AI 逐条拆掉：证明的脏活累活 AI 干，人负责写规格说明，也就是「这个程序应该满足什么性质」。de Moura 给想学 Lean 的人的建议很务实：直接跟 AI 对话学，屏幕分三块——Lean 代码、右侧实时反馈的 info view、底部一个 AI 智能体。路径也清楚：先玩 Natural Number Game（自然数游戏），完全免费，打开浏览器就能开始。知乎再读 lean-lang.org 上的免费入门书（函数式编程、定理证明、数学三个方向），中文材料可以看 B 站「手把手教你学 lean4」这类连载教程。预期管理要提前做好：从入门到能借助 mathlib 写小定理，是按周到月计的投入，不是速成班。

如果你是数学或 AI 进展的围观者——值得花一小时搞懂上面的「四层信任链」，但不必下场学。 接下来你会不断看到「XX 猜想在 Lean 中完成形式化」的新闻，能不能分清「形式化通过」和「猜想被解决」的区别，就是看懂门道和看热闹的区别。Connes 这个案例值得收藏，它是目前最好的样本。

如果你想要立竿见影的生产力回报——先别入。 Lean 目前不是通用开发语言，就业面窄（工业端规模最大的实践在 AWS 内部，一个约 50 万行 Lean 代码的 AI 加速器编译器项目），短期内它给你的回报主要是思维训练和前沿参与感，不是涨薪。

接下来值得盯的三个信号

1. ten-proofs 的另外九项：Nielsen 只驳回了 Connes 一项，其余九项（包括回答了 Gromov 1999 年提问的非 sofic 群存在性）还在等数学界逐条深究，单项被撤的可能性仍然存在。知乎

2. Astra 会不会开放：目前这批结果的可信度建立在「OpenAI 背书 + 机器检查」上，模型和工作流都不对外，无法独立复现；后续是否开放，含金量的成色会完全不同。

3. Lean 生态自身：内核漏洞的复盘质量、数学库 Mathlib 补齐研究级数学定义的速度、以及更多独立内核实现的出现，都会继续影响「Lean 已验证」这四个字的分量。

一句话收尾：这 20 天既不是「AI 证明不可信」，也不是「机器验证万能」，而是第一次把完整的验收链条暴露在所有人面前——模型负责猜，Lean 负责守逻辑，人类负责追问「你证的是不是我要的那道题」。能看懂这条链的人，才算真的看懂了这场热闹。