OpenAI 撤回三项数学成果
OpenAI withdraws three mathematical results
Dan Roberts 在 Twitter 上宣布，团队更新了 GitHub 上的数学仓库，新增了 6 个 Lean 形式化证明，修改了 19 处内容，并正式撤回了 3 项数学成果。目前该仓库中约 42% 的核心结果已完成形式化。被撤回的三项研究包括分裂阿贝尔八维流形上的 Weil 类代数性、K3 曲面的 Kuga–Satake 对应代数性，以及 K3 曲面乘积空间的有理 Hodge 猜想。此次公开撤回行为在学术界较为罕见，体现了对形式化验证严谨性的坚持。
我们已更新 GitHub 数学仓库，新增 6 个 Lean 形式化证明，修改 19 处内容，并撤回 3 项成果。
HN 评论区
86- renyicircle
这就是软件工程实践撞上数学时的样子。"openai/math 1.3.42 版本发布：撤回论文 139 和 140，修复了论文 47 中的符号错误，恢复了此前撤回的论文 85，重构了论文 101 的论证过程"。
我很好奇，这次撤回是因为有真正的数学家审阅了这些论文并发现了错误，还是因为他们运行了模型来进行校对？如果是后者，这恐怕也不是第一次了，毕竟他们在发表前肯定做过这件事。无论哪种情况，都很有意思。
- rich_sasha
我有点困惑——我以为他们的证明都是基于 Lean 证明的吗？难道不是这样？所以即使某些指标下工作质量不高，证明要么通过测试，要么不通过……？无论哪种情况，都没有改变主意的余地。
- autuni
这不完全相关于那条推文，而是关于这个话题本身，这促使我再次去检查他们的仓库，看到了这段内容：
> 绝大多数结果都是通过相同的流程，使用一个未发布的 OpenAI 内部模型获得的。平均而言，每个结果使用了该模型三小时的 ChatGPT Pro 思考算力。在评估过程中，该模型共被提出了约 4000 个问题。将输出聚合为结果族和手稿，并要求达到适当的显著性水平，最终形成了上述目录。
看到完整的问题列表将是整个情况中最有趣的部分。这或许能提供一些洞见，揭示哪些类型的问题属性会导致问题，或者对 LLM 来说容易解决。
（编辑：他们发布了约 700 个问题的结果，共 4000 个）
- theanonymousone
我很惊讶，关于他们的矩阵乘法界限（Matrix Multiplication bound）的讨论竟然不多：https://news.ycombinator.com/item?id=50001740
这有实际应用价值吗，还是目前仅仅是一个证明？
- ekjhgkejhgk
就在前几天我还在想，如果无监督数学最终会演变成“哎呀，我们在某段代码里发现了个 bug，数学的 XYZ 分支不再成立”的局面，那会怎样。