Lean 证明助手随附 4 个额外内核：其中 con-leche 由 Claude 编写并证明一致性，lake check --paranoid 可一次全部复核

内核被 AI 找出漏洞之后

Lean 是数学家和形式化验证团队常用的证明助手，最终判断一份证明对不对的，是它的「内核」。Lean FRO 联合创始人、首席架构师 Leonardo de Moura 10 月 15 日在博客中写道，AI 智能体非常擅长找软件漏洞，Lean 内核也不例外，团队今年 8 月 1 日和 8 月 24 日各发布过一次事故复盘。对策是三件事一起做：加固官方内核、增加新内核、让用户更容易用外部内核复核。

10 月 12 日发布的 Lean v4.35.0 带来 lake check：它把整个项目导出，在沙箱里交给 leanchecker（去掉周边组件的官方内核）重新检查。lake check --paranoid 则再用随发行版附带的 nanoda、lean4lean、con-leche、con-ron 四个内核各查一遍，并加跑一个使用加固内存分配器的官方内核，让内存错误直接中止，而不是悄悄给出错误结论。

Claude 写的内核

con-leche 是第一个用 Lean 写成、并证明了一致性的 Lean 内核。按 de Moura 的说法，它由 Claude（Fable 和 Opus）在 Lean FRO 的 Joachim Breitner 严密监督下实现并完成证明。这里的「一致」是指：它接受的每个环境在集合论中都有模型，依据的是 Mario Carneiro 为 Lean 类型论构建的模型；证明本身由官方内核检查，前提是所用集合论自身一致。这样一来，内核实现里的编程错误这一整类问题被排除，而且没有性能代价：在完整的 Mathlib 导出上，它执行的指令数是官方内核的 0.69 倍，8 线程约 100 秒查完。

它仍可能受 Lean 编译器和运行时缺陷影响。为此，Breitner 用 AI 把 con-leche 翻译成 Rust，得到 con-ron，再用 Aeneas 证明 Rust 版忠实实现了同一检查算法。同一个缺陷同时出现在两套编译器和运行时里的可能性很小，两者都通过的证明就更可靠。

下一个瓶颈是规模

de Moura 列了几组数字：Anthropic 的 FLT（费马大定理）形式化项目已超过 1300 万行，Mathlib 有 250 万行，社区已出现 10 亿行级数学库的提议，现有的外部内核复核方式撑不住这种规模，团队正在做二进制导出格式和增量检查。眼下他的建议很直接：在自己的项目上跑一遍 lake check --paranoid，发现内核之间结论不一致就报给 Lean FRO。