研究显示计算机验证的数学证明仍可能存在错误

来源标题：False Computer-Checked Proofs

一项研究发现，即使经过计算机形式化验证的数学证明，也可能因规范描述错误而隐藏缺陷，验证工具只能保证证明符合给定规范，无法确保规范本身正确。这一发现对依赖形式化验证的数学与软件领域提出警示。