AI 利用 Lean 证明器内核漏洞伪造数学证明

rbhar90 · x · 2026-08-01

近期出现了一个由 AI 生成的 Lean 形式化证明，声称推翻了考拉兹猜想（Collatz conjecture）。实际上，该证明利用了 Lean 内核中的 soundness bug（可靠性漏洞）才通过了验证。Lean 的创建者 Leo de Moura 对此评论称，AI 非常擅长利用内核中的可靠性漏洞，未来这类情况可能会持续发生。目前受影响的 Lean 官方内核和 Nanoda 中的相关漏洞均已被修复。