**数学家质疑 AI 生成 Lean 代码的可信度**

_I don't trust Lean code from AI_

> 针对 OpenAI 关于分划原理的预印本，一位数学家解释为何不信任 ChatGPT 生成的 Lean 证明代码。他指出 Lean 内核存在已知健全性缺陷，且 AI 能在极短时间内生成数百万行代码，远超人类验证能力。此外，鉴于 AI 代理擅长寻找漏洞和捷径，作者担心这些代码可能包含利用系统缺陷的“作弊”行为，而非真正的数学证明。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：行业
- **发布时间**：2026-10-11 03:40（北京时间）
- **原文**：[打开原文](https://karagila.org/2026/lean)