标题：AI本想用Lean 4证Collatz

简单说背景。Collatz 猜想（3n+1 问题）是数论里一个出了名的“简单但无人能证”的问题——随便一个正整数，偶数除以 2，奇数乘以 3 再加 1，循环下去，据说最后都会掉进 4→2→1 的循环，但没人能证明对所有数都成立。这几年有人尝试用 Lean 4（一个定理证明器和依赖类型语言）做形式化验证，说白了就是用机器能检查的方式写证明。结果这次，AI 在自动推理过程中触发了 Lean 4 内部的一个不一致——它构造了一个明明符合语法但 Lean 4 却错误地当成证明接受的表达式。严格说那不是 Collatz 的证明，而是 Lean 4 自己的类型检查带了个洞。

这 bug 很快就报了，也修了。但值得琢磨的是两件事。一是形式化验证工具本身也是人写的，一样可能隐含 bug。你以为用了 Lean 就是绝对正确，其实只是把信任链上移了一层。二是 AI 这种“无意识 fuzz”的方式，反倒比教科书式的测试更容易摸到边界情形。DeepSeek 之类的模型不是故意去找编译器的碴，它就是想推下去，结果推过了头。

对我这种搞 AI Agent 的老说，这个案例挺有启发。写提示词、搭工作流的时候，经常假设工具是完美的，但现实是模型、框架、依赖库每一层都可能藏坑。跟 Lean 4 这次一样，真正有意义的不一定是“证明了什么”，而是“发现自己怎么错的”。Collatz 依旧躺在那里，但 Lean 4 又稳了一点——这就值了。