nanoda：为什么 Lean 还需要另一个 kernel
· 阅读需 14 分钟
Lean 已经有 kernel，为什么还要再写一个？
答案不是“官方 kernel 不可信，所以换成 nanoda”。nanoda 也有过 soundness bug，而且本系列的主事件正是旧版 nanoda 接受了一个它本应拒绝的 artifact。它的价值来自另一件事：用另一种语言、另一套代码和另一条 proof replay 路径，减少 official Lean kernel 成为唯一故障点。
nanoda 是一个 Rust 编写的 Lean 4 external type checker。
它读取 lean4export 产生的 proof environment，重新检查 declarations、theorem bodies、inductive types、recursors、projections、axioms 和 definitional equality。它不运行 tactic，也不需要相信原项目的 elaborator 输出过程；它关心的是最终导出的 kernel-level 对象能否在自己的实现中成立。