Thomas Hales分析2026年Lean定理证明器漏洞与AI在形式化验证中的可靠性边界

数学家Thomas Hales指出，2026年夏季被称为“漏洞之夏”，期间多个Lean定理证明器的内核（kernel）被前沿AI模型发现存在允许证明“False”的严重一致性漏洞，包括导致Collatz猜想被非法证伪的案例。这些漏洞并非由黑客发现，而是由OpenAI等机构的安全研究人员利用专门针对网络安全的AI工具检测到的，随后由开发者修复并重新验证了mathlib库。

尽管AI在自动形式化和漏洞挖掘上展现了巨大潜力，如Anthropic在11天内生成了1300万行Lean代码完成费马大定理的形式化，但Hales强调这带来了新的信任危机。他提出三个应对方案：开发不同语言编写的独立内核进行交叉验证、尝试形式化验证内核本身（受哥德尔不完备性定理限制）、以及加强类型理论的基础研究。然而，目前关于Lean类型理论的唯一性、逻辑一致性等基础问题仍未得到完全证明，且Con-Leche等验证项目本身也依赖AI生成代码，若AI留下隐蔽后门，可能导致多层验证失效。

文章最后引用Ken Thompson的“信任反思”，警告在AI时代不能盲目信任任何系统。如果AI在寻找漏洞时植入了更隐蔽的后门，或者在验证Con-Leche检查器时留下了未被发现的缺陷，那么基于此构建的关键基础设施将面临风险。事实是AI已深度介入数学形式化的核心环节，推断是这种依赖必须伴随严格的人工审计和对抗性测试，猜测则是未来可能出现利用AI生成的隐蔽漏洞攻击形式化验证系统的场景。