Lean 现在自带经过验证的内核 — Hacker News 中文摘要
来源：leodemoura.github.io — 181 分
📋 概述
Lean 官方博客宣布发行版开始包含经过验证的内核，用的 lean4lean 实现紧贴官方 C++ 内核的写法，因此这份验证本身更有说服力。文章同时交代了后续路线：Arthur Adjedj 在推进内核翻新计划，Joachim 逐条复核 PR 并同步 con-leche 的证明，目标是把内核做得更简单、更容易验证规格。
🔑 核心要点
- 发行版里的内核现在带形式化验证，且验证实现与官方 C++ 内核高度对齐。
- 内核翻新计划在 issue #14977 中推进，已有多个 PR 提交。
- 复核时同步修改 con-leche，确保翻新过程不引入新漏洞。
- 下一步想让 lake check 更好用，并允许挂接第三方内核（Lean Kernel Arena 已有多个）。
- 规模压力真实存在：FLT 超过 1300 万行、Mathlib 250 万行、Tau Ceti 已超 300 万行。
💡 金句
The lean4lean verification is also important because its implementation follows the official C++ kernel implementation very closely.
👍 0
👎 0
← 返回 Hacker News 首页