1 篇博文 含有标签「theorem-proving」

2026 年 7 月 28 日，Lean Zulip 的 lean4 stream 出现了一个很难忽略的 topic：Counterexample to the Lean Conjecture (Soundness Bug)。

帖子里的三个事实放在一起，几乎像一道故意设计的判断题：

1. 一个不到 500 行的 Lean 仓库声称“反证”了 Collatz 猜想。
2. 它没有 sorry，#print axioms 没暴露隐藏公理，当时的 comparator.live 和旧版 nanoda 都接受了它。
3. 它没有解决 Collatz。它真正构造出来的是一个利用 kernel soundness bug 的无公理 False。

这不是“形式化验证忽然失效”的故事，也不是一个模型真的完成了世纪数学突破。它更具体，也更值得研究：一份 proof artifact 把 Lean 官方 kernel 的漏检 与 旧版 nanoda 的另一处漏检 拼在一起，恰好穿过了两套原本彼此独立的检查。