定理证明器 Lean 4 内核现高危漏洞，可无公理证明 0=1

jedisct1 · x · 2026-08-12

安全研究人员发现 Lean 4 定理证明器内核存在类型混淆漏洞（CWE-843）。通过在嵌套归纳类型的投影验证中绕过检查，攻击者可利用精心构造的哈希碰撞，最终让系统接受 False 的证明，从而得出 0 = 1 的荒谬结论。

该漏洞被标记为 CVSS 7.1 高危级别，影响 Lean 4 v4.31.0 及更早版本。官方已在最新的 nightly 构建中修复此问题，并提供了无需额外公理即可复现该漏洞的概念验证（PoC）代码。