2 篇博文 含有标签「security」

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 的另一处漏检 拼在一起，恰好穿过了两套原本彼此独立的检查。

一份不可信的 Lean 项目能够 lake build，不等于它证明了你以为的 theorem。

它可能重新定义了 statement 里的 identifier，用 macro 或 notation 改变表面语法的含义，用不同 typeclass instance 让同一个类型别名展开成另一项，也可能在 build 阶段运行 meta code、写文件，最后再把 sorry warning 藏起来。Lean 很灵活，这种灵活性对正常开发是能力，对 adversarial proof 则是攻击面。

Comparator 的工作，是在一个 reviewer 控制的 theorem statement 与 untrusted proof project 之间建立边界。它不只问“这份代码能否编译”，而是问：它是否证明了 trusted Challenge 中那个精确的 statement，只用了允许的 axioms，并且能被指定的 kernel 接受？