8月1日，OpenAI 公布了下一代模型 Astra，同时丢出10道数学与理论计算机科学难题的"答案"，这批问题此前至少十年、部分近三十年没有实质性进展。微博每个答案都附 Lean 4 形式化证明证书，开源在 GitHub 上，机器可以逐行核验。知乎
OpenAI 还补了一句：把功劳归于人类会歪曲事实。知乎但这个"登月时刻"仅仅维持了五天，多位活跃在科研一线的顶尖数学家联合发文，直指两项核心成果的核心论证来自已有论文、没有恰当引用。知乎更微妙的是，同一时期 Lean 自己也刚修掉一个会"判错案"的内核漏洞——负责盖绿色对勾的机器，在另一个地方盖错了章。那么问题就变得很具体：这个绿色对勾到底能保什么，又保不了什么？
绿色对勾是什么
一句话：Lean 检查证明，靠的是类型检查。你不需要信任整个 Lean，只需要信任它的内核。知乎这个内核只有约5000行代码，小到有人用 Lean 本身重写了一个叫 Lean4Lean 的内核，还证明了它的正确性。它盖出的绿色对勾，意思是"在当前规则下，证明的每一步都能从上一步推出"，而不是"这段文字读起来很严谨"。知乎
这套东西不只是数学玩具。今年的 PLDI 大会上，Gimlet Labs 展示了对 AI 编写的 GPU 内核做形式化验证的案例：AI 生成的优化版本将注意力计算悄悄移除了中间裁剪操作。知乎而人类参考实现的运算链清清楚楚：Q 和 K 先做 MatMul，再 scale，再 Softmax，再 MatMul，最后由 clamp 把数值限制在安全区间内输出。
删掉 clamp 的 AI 版本，在随机测试里和原实现输出一模一样，可一旦输入越界，就可能引发数值不稳定。验证器的办法是：把两份代码翻译成同一种中间表示，拆成基本数学运算，再标量化之后交给 Z3 求解器判定——找到反例就拒绝，证明所有情况等价就放行，算不出来就退回测试。随机测试可能永远抓不住的 bug，它0.01秒就揪了出来。
这就是绿色对勾的完整含义：它保的是推理过程本身，不是"结论看起来可信"。
但绿色对勾只保这一件事
第一层保不了的，是"证的是不是那道题"。Lean 可以完美地证明 P，但人类可能以为 P 对应的就是自然语言里的那个猜想，只要命题还停留在自然语言层面，机器就无法核验两者是否等价。微博
这次 OpenAI 对 Connes 刚性猜想的反例就遇到了这种挑战：一篇反驳文章声称，OpenAI 构造的群不满足猜想的前提条件，但将反驳文章与公开的 Lean 源码逐条对照后，可以发现其关键质疑是错误的。微博即便如此，陈源等人也把话说得很清楚：形式化命题是否忠实表达了原猜想，仍需算子代数专家与 Lean 专家共同确认，这一步完成之前，谈不上"验证完毕"。
第二层保不了的，是检查器自己。检查器也是软件，是软件就可能有漏洞。就在8月初，Lean 刚修复了一个与嵌套归纳类型有关的内核漏洞：此前有 AI 交出一份考拉兹猜想的"反证"，一路查下去发现它只是钻进了验证器的缺口，所谓反证最后被缩减成了一份 False 的证明。知乎官方一小时内推送了修复并补上回归测试，连独立检查器 nanoda 都被查出另一个问题。这不说明 Lean 不可靠——愿意公开事故、快速修复、留下测试，恰恰是可靠工程该有的样子。但从此看到"Lean 已验证"，最好顺手多问一句：哪个版本？
第三层保不了的，是"想法是谁的"。Lean 能验证证明是对的，验证不了这个想法是谁的。知乎高维球堆积一题的核心论证，早在2016年就出现在 Miller 与合作者的论文里，最初版本没有提及；非 sofic 群结果的地基，则分别来自 Gábor Kun 2016年关于膨胀图性质的研究，以及 Andreas Thom 2019年关于 Kazhdan 性质（T）的论文。知乎OpenAI 连夜修改了论文措辞，表示会对结果正确性负责并做"小幅更新"，但数学界的信任一时收不回来。
一个容易混淆的反面例子
就在前不久的知乎上，还有一次"假绿勾"的现场演示。7月底，有题主宣称在 lean4 里形式化了广义黎曼假设，请网友找漏洞，收到的回复是：除了还剩下24个 unsolved goals、24个语法错误、8个类型异常和3个把定理当定义的问题之外，“你几乎已经完成了 GRH 的证明”。知乎更耐人寻味的是，题主声称这份代码通过了多个 AI 的一致性逻辑检查，评论区网友直接回怼：该通过的难道不是 lean 的类型检查吗？知乎这个例子值得当镜子照。分辨"真绿勾"和"看起来绿"，只需要三个问题：检查器是不是真的通过了全部目标，还是留着未解决项？Lean 里形式化的命题，和自然语言说的是不是同一件事？有没有私设公理或 sorry 占位符混进去？任何一条存疑，对勾都不成立。
话虽如此，这事真值得上手
如果你被勾起了兴趣，现在其实是入场的好时机。入门路径已经被游戏化：Natural Number Game 里一关一关证自然数的加法和归纳，数学里所有"显然易得"“同理可证"的模糊跳步，在这里完全不存在。小红书Lean Game Server 里的自然数和集合论关卡，已经有人一路打通，评价是"有点上头”，关卡设计得让人停不下来。小红书
第一道门槛其实是装环境。有小红书网友说很想尝尝 Lean4 的咸淡，自己估计大概率从第一步安装开始就会卡壳。小红书绕开这一步的办法不少：live.lean-lang.org 可以直接在浏览器里写；B站有逐关 walkthrough；UC Berkeley 2026春季课的 Lean 课程资料也挂了出来。国内这边，浙大 Lean4 暑校甚至开出了"麻将的数学形式化"分组，入门氛围比想象中热闹。
值得继续盯的信号
最后给几条值得持续跟进的线索：
十项成果能否通过深度同行评议，重点不在"Lean 验过了"，而在领域专家确认"形式化命题就是那个命题"。
独立验证的进展。这次 Lean 内核和独立检查器 nanoda 都暴露过问题，以后看任何绿色对勾，可能都得先问一句它出自哪个版本、哪个检查器。
能力的边界。Lean 作者 de Moura 的判断是：AI 可以找到已有问题的新证明路径、可以反驳猜想，但还没有证据表明它能提出新的数学概念。知乎
成本曲线的下降。当"附一份机器证书"的代价开始像云账单一样可计算，这样的新闻只会越来越多。
成本信号其实已经在显现。今年5月 Erdős 单位距离猜想的形式化挑战发布后，包含全部依赖库约100万行代码的证明，从发布到完成只用了大约两周。知乎
写在最后
真正的分水岭不是"信不信 AI 证明"，而是会不会读验收单。绿色对勾只保一件事：在当前规则下，推理过程没有错误。它不保证问对了题，不保证功劳归属，也不保证检查器永远正确。知道这条边界，这项技术才值得认真关注。
