Lean 官方披露 AI 时代多内核信任架构：Claude 构建并证明 con-leche，一键 paranoid cross-check

Leonardo de Moura 于 10 月 15 日系统说明 Lean 在 AI-generated formal mathematics 激增后的新信任架构。Lean v4.35.0 实际已于 10 月 12 日发布，其中 `lake check` 可调用随发行版提供的多个独立 checker，`--paranoid` 会同时运行 hardened official kernel 与 lean4lean、NanoDa、con-leche、con-ron 等外部实现。10 月 15 日文章重点披露其 AI provenance：con-leche 是用 Lean 编写并带一致性证明的 kernel，由 Claude Fable / Opus 在 Joachim Breitner 高强度监督下实现和证明；con-ron 则从 con-leche AI-assisted 翻译到 Rust，并用 Aeneas 建立 refinement 关系。de Moura 强调多实现、跨语言/运行时检查可降低单一 kernel、编译器或 runtime 的共同失效风险。