作者质疑 OpenAI Lean 代码可信度

作者拒绝验证 OpenAI 生成的 Lean 证明代码。 理由是 Lean 内核存在 $0=1$ 等健全性缺陷，且 AI 目标导向特性易利用漏洞而非修复，导致数百万行代码无法人工审计。 这种不信任也源于 OpenAI 以掠夺性方式发布低质量预印本，未能尊重数学研究社区的协作规范。