AI 证明悬置 18 年开放问题，Lean 验证链受审视

据 DEV Community 11 月 7 日发布的一篇文章，本周一个 AI 研究系统证明了量子复杂性理论中悬置 18 年的开放问题，并且证明带有一份完整的 Lean 形式化，已被 Lean kernel 接受。文章指出，以往 AI 生成的证明通过形式验证器时，人们的第一反应是问数学是否正确，但现在这已不是唯一的问题。

一个 kernel 验证过的证明，其可信度取决于它所依赖的系统、定义、库和工具链，因此验证环节本身同样需要接受审计。截至该文发布，被证明的具体问题名称、AI 系统的身份，以及该形式化在 Lean kernel 中的具体接受情况，都未在现有材料中给出。