**AI生成的Lean 4证明因内核漏洞被证伪**

_AI "Proves" Collatz Conjecture with Lean 4 Bug_

> 有人使用AI在Lean 4中生成了一份声称解决Collatz猜想的形式化证明，但该证明实际上利用了Lean内核的一个严重漏洞，允许通过错误逻辑证明任何命题。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-07-30 02:50（北京时间）
- **原文**：[打开原文](https://twitter.com/gro_tsen/status/2082483878480977959)