OpenAI 撤回了三个数学结果

原文 ↗ Hacker News 讨论 ↗

OpenAI 大规模发布 AI 生成的数学论文——随后又因错误悄然撤回了三个结果——引发了一场关于 AI 研究炒作与传统数学严谨标准之间的冲突。评论者争论：部分经过 Lean 形式化的证明和难以阅读的 AI 写作手稿，究竟应不应该为了社区审查而尽早公开，还是应该等到彻底验证后再发布，因为这会给人类专家带来沉重负担。在此之下，许多人担心这对数学生态系统本身的长期影响：从资助和职业发展，到是否会用难以验证的“slop”淹没这个领域，从而减缓而非加速真正的进步。

发布与撤回

  • OpenAI 发布了约 700 个数学结果（来自约 4,000 个问题）的 GitHub “预印本”转储；随后在发现错误（例如一个符号错误）后撤回了三篇手稿，并新增了若干 Lean 形式化。
  • 有些人认为，数百个结果中撤回 3 个是正常的科学修正过程；也有人认为这严重削弱了标题中的主张。

Lean 形式化与验证

  • 约 40–42% 的“核心”结果现在已有 Lean 形式化证明；其中一些是在发布后补上的。
  • 许多人强调，Lean 只保证内部逻辑成立，并不保证形式化与预期定理一致。错误可能出现在：
    • 在 Lean 中把问题陈述错了。
    • 使用了缺失或细微地错误的定义。
    • 少见但真实的内核 bug，以及证明助手的“奖励黑客”行为。
  • 有几位指出，许多陈述（例如标准猜想）原本就已经在数学库中；新的是机器生成的证明。

质量、可读性与“slop”

  • 多位读者把这些论文描述为难读、组织混乱、引用繁多；“AI 精神病”和“slop”是反复出现的主题。
  • 人们担心，规模巨大、晦涩难懂的证明实际上对人类来说无法验证，即使它们在数字上“通过检查”。

责任、宣传与激励

  • 批评者说 OpenAI 为了炒作/IPO 观感而仓促行事，发布了未经验证的工作，并把验证工作外包给社区。
  • 辩护者回应说，这类似于 arXiv 上的人类预印本，而且一些数学家明确要求尽早发布以保持透明。
  • 讨论还包括：OpenAI 是否应把完全经过 Lean 验证的结果与推测性结果分开，以及是否应支付外部验证者报酬。

对数学界的影响

  • 人们担心炒作可能会：
    • 削弱学术数学的资助和职业发展。
    • 让数学家成为企业模型的无偿证明检查员。
    • 侵蚀理解和扩展结果所需的“繁荣社区”。
  • 也有人认为，如果 AI 能自动化数学的大部分工作，那只是经济现实的反映；也有人欢迎 AI 作为强大的新工具。

与软件及其他领域的类比

  • 许多人把这与 LLM 生成代码相比：生产力大幅提升，但验证和维护会成为瓶颈；“agent wranglers”取代传统的初级工程师。
  • 更广泛的担忧是，AI 生成的“slop”会淹没研究（数学、软件、实验科学），把稀缺的人类注意力从创造转向分流审查与清理。