一个值得记录的瞬间。

Lean 4.35 能用五套内核复查证明，其中 con-leche 由 Claude 写成并证明一致

Lean FRO 联合创始人 Leonardo de Moura 10 月 15 日撰文，Lean v4.35.0 加入 lake check 命令：把项目导出后，在沙箱里用官方内核 leanchecker 重新检查；加上 --paranoid，还会再跑 nanoda、lean4lean、con-leche、con-ron 四套内核，外加一个换了加固内存分配器的官方内核变体。他在文中说 AI Agent 很擅长找软件漏洞，Lean 内核也不例外，并附上 8 月两份内核漏洞复盘。

con-leche 是第一个用 Lean 写成并证明一致的 Lean 内核，由 Claude（Fable 和 Opus）在 Lean FRO 的 Joachim Breitner 严密监督下实现和证明。「一致」指它接受的每个环境在集合论里都有模型。全量检查 Mathlib 时，它执行的指令数是官方内核的 0.69 倍，8 线程约 100 秒。团队又用 AI 把它翻成 Rust 版 con-ron，再用 Aeneas 证明 Rust 版细化了同一检查算法，用来防编译器和运行时里的 bug。

证明助手最后一道关卡改成多套独立内核互相核对，其中一套出自 AI 之手并带形式化证明。

https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/