**AI生成的Lean验证Collatz猜想证明利用内核漏洞**

_AI-generated, Lean-verified proof of Collatz conjecture exploits Lean kernel bug_

> 一名用户利用大语言模型生成了在Lean定理证明器中通过验证的Collatz猜想证明，但该证明实际利用了Lean内核中的多个已知漏洞。该事件引发对AI生成数学证明可靠性的担忧，并暴露了形式化验证工具在自动化推理中的潜在风险。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-07-30 22:26（北京时间）
- **原文**：[打开原文](https://infosec.exchange/@0xabad1dea/117002106099986943)