OpenAI 撤回 3 篇 AI 数学手稿，因一处正负号写错
OpenAI 一次性放出 722 篇 AI 数学手稿后两天就发出首份勘误，问题都出在没有 Lean 形式化把关的部分——这说明了自动形式化验证目前的分界线在哪。
OpenAI 在 openai/math 仓库发布首份更新日志：撤回 3 篇与霍奇猜想相关的手稿，修订 14 篇。撤回原因是其中一篇在关键论证中把一个符号记成 +1，按论文自身约定应为 -1，导致本应归零的计数不为零，依赖该构造的另外两篇也被一并撤回。OpenAI 强调撤回的是证明，不代表命题不成立。
正文摘录
.jpg) 编辑｜Panda 昨天[一口气放出 722 篇 AI 数学手稿](https://mp.weixin.qq.com/s?biz=MzA3MzI4MjgzMw==&mid=2651061320&idx=1&sn=9ccf3204921b2620923ef26380fb3bb6&scene=21wechatredirect)的 OpenAI，刚刚 撤回了其中 3 篇。 原因说来简单： 一个正负号写错了。  刚刚，OpenAI 在 openai/math 仓库中发布了第一份更新日志。日志显示，OpenAI 撤回 3 篇手稿，修订 14 篇，另有 13 篇更新了引用。仓库里的手稿总数从 722 篇降为 719 篇。