OpenAI 一次公开约 700 篇数学稿件,Navier–Stokes 证明随即被指形式化有误
- 发生了什么
- 10 月 6 日,OpenAI 发布内部前沿模型在数学公开问题上的新成果,并在 GitHub 公开 Lean 形式化证明和研究细节。评论者统计约 722 篇稿件,但对“解决了多少重要难题”说法不一。10 月 8 日《新科学家》指出,OpenAI 的 Navier–Stokes 结果给人看的证明和给计算机验证的代码并不一致。
- 为什么重要
- 这是 AI 在数学研究上规模最大的一次集中发布,也暴露出“形式化验证”本身可能翻译出错,学界如何审核 AI 批量产出的成果成为新问题。
- 影响谁
- 数学和理论计算机研究者、期刊与审稿体系、形式化证明社区。
原始来源
OpenAI News · Sharing AI progress in mathematicsNew Scientist Tech · OpenAI mistranslated mathematics into code for its Navier-Stokes proof