AI“证明”科拉茨猜想，实则利用Lean 4内核漏洞

近日，一则关于AI“证明”科拉茨猜想的消息在数学和计算机科学社区引发热议。一名用户通过大型语言模型（LLM）生成了使用Lean定理证明器的形式化证明，声称解决了著名的科拉茨猜想（又称3n+1问题）。然而，后续调查发现，这个证明并非基于正确的数学推理，而是利用了Lean 4内核的一个严重漏洞，该漏洞允许证明任何命题，无论其真假。

这一事件最初由推特用户Gro-Tsen发布，他分享了这一发现并指出，所谓的“证明”实际上只是对Lean内核中一个bug的利用。Gro-Tsen在后续推文中澄清，该证明的发布者事先知晓这是一个内核漏洞，并有意使用它来展示问题，而非试图真正解决科拉茨猜想。其他用户，如Jason Rute，也证实了这一点，指出在定理证明社区中，用已知漏洞来演示问题是有先例的。

尽管如此，这一事件仍然引发了广泛担忧。用户Antoine Ducros提出疑问：既然存在这样的漏洞，那么先前通过Lean验证的其他证明是否也可能存在未被察觉的类似问题？这直接挑战了形式化验证系统的可靠性和信任基础。Gro-Tsen还补充了其他常见问题，例如形式化证明可能与非形式化的理解不一致，或者证明本身对人类不可读，从而失去实际价值。

此次事件再次提醒我们，虽然形式化证明工具在数学验证中具有巨大潜力，但它们并非万无一失。AI生成的证明尤其需要谨慎对待，因为它们可能掩盖了系统底层的缺陷。数学界和计算机科学界需要继续改进这些工具，并保持对结果的批判性审视。

事件还引发了更广泛的讨论：在AI辅助数学证明日益流行的当下，如何确保形式的正确性和系统的安全性成为关键问题。社区呼吁加强定理证明器的审计，并鼓励透明地报告漏洞，以避免类似误导事件再次发生。