7月25日，Ramana Kumar在GitHub上放出一个仓库：一份由AI辅助生成、不含sorry的Collatz猜想“反证明”。三天后，Kiran Gopinathan把它精简成几行代码，直接构造出一个False的证明，提交了issue #14576。Lean核心团队一小时内就把补丁推了出去（PR #14577），经审查合并，新补丁版本随即发布。
这本该是个“漏洞发现—修复”的常规故事。但往下多看一层，会发现真正有意思的不是这个漏洞本身，而是它顺带牵出的另一个漏洞——那个漏洞不在Lean里，而在一个专门用来检查Lean的独立系统里，且早在Lean漏洞被报告前一周就已经修好了。
漏洞出在哪：一个只有元编程能碰到的角落
Lean的内核在处理嵌套归纳类型时，如果构造子的某个参数是“幻影参数”——也就是这个参数根本没出现在构造子的字段里——它会在内核生成的辅助类型中悄悄消失，逃过类型检查。塞一个类型不对的参数进去，内核就有可能把一个False的命题当成真命题接受。
关键限制是：这条路只能靠元编程直接向内核发送归纳声明才能走通。正常写证明时，前端elaborator会先检查参数类型，把不合法的项拦下来。也就是说，普通用户写出这个漏洞的概率几乎为零，能触发它的只有故意绕开前端、直接跟内核对话的代码。
巧合还是嗅觉：两把锁同时松动
真正让这次事件变得不寻常的，是那份Collatz假证明当初还通过了一个一周前版本的nanoda——这是Chris Bailey用Rust独立实现的另一个Lean检查器，本该和官方内核完全无关。它其实也检查了那个位置，只是没验证投影节点里的类型名，这个bug由Jeremy Chen报告，在Lean漏洞被发现前一周已经修复。
也就是说，这份假证明恰好踩中了两个互不相关实现里两个互不相关的漏洞，而且是在其中一个已经修好、另一个还没被发现的窄窗口里完成的。Ramana Kumar认为这是巧合，但也承认无法排除模型此前接触过nanoda修复记录的可能。Joachim Breitner给出另一种解释：不是信息泄露，而是当下的强模型本身已经具备发现这类隐蔽实现漏洞的能力。两种说法目前都没有定论。
内核没被攻破，是因为攻破的门槛从来不是一把锁。
这恰恰是多内核交叉验证的设计初衷：单独一个实现出问题不可怕，可怕的是所有独立实现在同一时刻同一位置都出问题。这次两个漏洞确实同时存在过，但它们互相独立、修复节奏也不同步，攻击者要拼出一份能同时骗过两套系统的证明，门槛比骗过一套高得多。这次事件更像是压力测试意外通过了，而不是防线被突破了。
“砍掉元编程”是个方向性错误
事件讨论里有人提议：既然攻击路径要靠元编程直接给内核喂归纳声明，不如限制或移除元编程能力，从源头堵死这条路。作者明确反对。
理由不复杂：Lean的elaborator（前端）本来就是不可信组件，安全性从设计上就不能指望它主动拒绝写坏证明。想提交恶意证明的攻击者，完全可以绕开elaborator，直接手写.olean文件或者篡改内存——这些路径元编程限制统统管不到。内核必须能在自己的进程里独立拒绝一切不合法的声明，这才是可信计算基该有的样子。这次的问题不是元编程给了攻击面，是内核本身在这一处没做完整的类型检查。
- 结论.内核必须自己验真，不能指望前端替它把关，这也是证明项统一走内核校验这套架构的核心优势。
这个原则不只对Lean成立。任何基于“小内核+大前端”结构的证明助手——Coq、Isabelle都是同一套逻辑——如果哪天有人建议靠削弱功能来堵漏洞，多半是没分清楚可信边界画在哪。
修复之外，还剩下什么没补上
Mario Carneiro的lean4lean项目在做一件更根本的事：用Lean本身去形式化Lean的类型论，并证明内核实现符合这套理论。但这项工作目前还没覆盖归纳类型，而这次的漏洞恰好长在归纳类型这一块。也就是说，即便lean4lean的一致性证明当时已经完成，也未必能在漏洞被利用之前自动拦下它——它只是本该在补完这部分验证时被发现。
- 风险.被形式化验证的内核，目前还没验证到归纳类型这一步，这个空白点会在多久内补上还不确定。
团队随后做的加固包括：往Kernel Arena里加了这次的漏洞回归测试和Arthur Adjedj提出的一个相关非统一参数场景；PR #14582让内核真正检查嵌套出现处的参数是否表现得像参数，而不只是重新做类型检查；OpenAI的Daniel Selsam用一个专门做安全审计的AI帮忙又找出几个内核编程失误，全部修复，而且全部被nanoda提前捕获，同样只能通过元编程触发。comparator.live现在默认跑nanoda，日常追踪版本是否同步。
这条线索其实比漏洞本身更值得记住：一份意外的AI生成假证明，客观上完成了一轮谁都没安排的红队测试，而团队后续引入的AI安全审计，又在没有实战诱因的情况下主动挖出了同类问题。形式化验证社区过去更担心AI会不会“生成出看起来对但实际错的证明”，这次事件提醒的是另一半——AI也可能顺手把系统自身的漏洞给带出来，无论是不是故意的。孟子说“生于忧患，死于安乐”，一套系统能不能扛住冲击，往往不是看它有没有漏洞，而是看漏洞出现时，防线是单薄还是有纵深。这次答案是后者，但lean4lean那块空白提醒人，这份从容还没到能完全放心的地步。