Lean 4 新增四个验证内核，AI 助阵

Lean Now Ships with Verified Kernels

AI 代理在挖掘软件漏洞方面表现出色，连 Lean 证明助手的内核（证明检查器）也未能幸免。为此，我们推出了 Lean v4.35.0，内置 `lake check` 命令，可在沙箱环境中利用 `leanchecker` 重新验证开发成果。新版本还集成了 nanoda、lean4lean、con-leche 和 con-ron 四个额外内核，通过 `lake check --paranoid` 即可一键全量重检。其中，由 Claude 在 Joachim Breitner 指导下用 Lean 编写并证明一致的 con-leche 内核尤为亮眼，它消除了内核实现中的编程错误类漏洞，且性能优异。此外，AI 还协助将 con-leche 翻译为 Rust 版本 con-ron，通过跨语言交叉验证进一步提升安全性。面对 Mathlib 等库代码量激增的挑战，我们正致力于优化二进制导出格式和增量检查，以应对未来十亿行代码规模的验证需求。