Lean 内核出现可构造 False 的健全性缺陷并已修复 RSS

依赖形式化证明的系统把「内核拒绝非法项」当作信任根。Lean 官方复盘称，一份 AI 辅助生成、没有 sorry 的反 Collatz 证明利用了嵌套归纳类型参数缺检查的实现缺陷，因而能构造出 False。问题在报告后约一小时修复并发布补丁，只能经元编程直接向内核提交构造来触发。值得注意的是旧版独立检查器 nanoda 另有缺陷，说明多一个检查器并不等于可以不升级，关键证明应在两端重新校验。

发布于 2026-09-10T10:59:47.32849Z · Lean FRO · Leonardo de Moura 博客

Lean 可信根 形式化验证

依赖形式化证明的系统把「内核拒绝非法项」当作信任根。Lean 官方复盘称，一份 AI 辅助生成、没有 sorry 的反 Collatz 证明利用了嵌套归纳类型参数缺检查的实现缺陷，因而能构造出 False。问题在报告后约一小时修复并发布补丁，只能经元编程直接向内核提交构造来触发。值得注意的是旧版独立检查器 nanoda 另有缺陷，说明多一个检查器并不等于可以不升级，关键证明应在两端重新校验。

依赖形式化证明的系统把「内核拒绝非法项」当作信任根。Lean 官方复盘称，一份 AI 辅助生成、没有 sorry 的反 Collatz 证明利用了嵌套归纳类型参数缺检查的实现缺陷，因而能构造出 False。问题在报告后约一小时修复并发布补丁，只能经元编程直接向内核提交构造来触发。值得注意的是旧版独立检查器 nanoda 另有缺陷，说明多一个检查器并不等于可以不升级，关键证明应在两端重新校验。

原始来源 ↗

来源记录

• center.info_item · f5ae1e46f8ec3adf · 2026-10-03T04:08:35.169032Z
• pgweb.info_item · f5ae1e46f8ec3adf · 2026-10-03T04:08:55.967155Z