OpenAI 数学仓库因符号错误撤回 3 篇霍奇猜想论文

OpenAI 在公开 openai/math 仓库仅两天后发布首份更新日志：撤回 3 篇手稿、修订 14 篇、更新 13 篇引用，手稿总数从 722 降至 719。撤稿原因是一处符号错误使一个稳定性-迹相消（stability-trace cancellation）论证失效，另两篇依赖该论证的论文随之撤回；据机器之心转述，三篇均与霍奇猜想相关，涉及 Weil 类代数性与 K3 曲面等内容。

已确认

• OpenAI 于 10 月 7 日前后撤回 3 篇论文，并修订其余 14 份手稿。
• 仓库新增 6 个 Lean 形式化、19 处修改。
• 在 719 项核心（顶线）结果中，约 300 项、即约 42% 已完成 Lean 形式化，团队表示将持续更新。

为什么重要

• 事件显示形式化验证正在成为 AI 生成数学成果的可信度把关机制：错误由 Lean 形式化流程暴露并促成及时撤稿。
• 42% 的形式化覆盖率意味着多数结果尚未经机器验证，该仓库的可信度仍有待后续形式化工作逐步确认。

2026-10-08 ~ 2026-10-09 · 5 条相关

事件全程(共 3 集)→

• 第 1 集:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(2026-10-08,14 条)
• 第 2 集:OpenAI 数学仓库因符号错误撤回 3 篇霍奇猜想论文(2026-10-08,5 条)
• 第 3 集:研究者用 Lean 验证并改进 OpenAI 数学证明(2026-10-08,2 条)

• 【源头】OpenAI 数学仓库更新：约 42% 顶线结果已 Lean 形式化，3 篇撤稿 — danintheory · 2026-10-08
• 【源头】一个正负号写错，OpenAI 数学仓库两篇霍奇猜想论文遭撤回 — 机器之心 · 2026-10-08
• AI 数学仓库更新：约 42% 顶线结果完成 Lean 形式化，撤稿 3 篇 — iskander · 2026-10-08
• 【源头】OpenAI 撤回 3 篇数学论文,719 项结果仅 42% 完成形式化 — petrusenko_max · 2026-10-08

另有 1 条近重复转述:petrusenko_max