199 例计算机检查过的证明竟是错的:形式化验证工具的可靠性危机

jedisct1 · x · 2026-11-13

密码学家 David Wong(hashbreaker)发布新页面「False computer-checked proofs」,汇总了 199 份关于多个重要证明检查程序(Coq/Rocq、Isabelle、Lean、HOL 等)可靠性(soundness)漏洞的报告,并附一张按年份与证明器分类的图表:Coq/Rocq 相关报告近年加速增长,2025-2026 年间达上百例,远超其他证明助手。所谓「计算机检查过的证明」并不等于必然正确——一旦底层内核存在可靠性 bug,通过检查的定理也可能有假。这一汇总对依赖形式化验证的安全与数学研究社区是重要警示。