# 数学家指出 OpenAI 的 Navier-Stokes 证明在转为 Lean 代码时存在误译

> 原标题：OpenAI mistranslated mathematics into code for its Navier-Stokes proof

- 来源：Hacker News 首页
- 发布时间：2026-10-09T21:25:09.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/gaesbgtqofpn620arukf9k0wj
- 原文：https://www.newscientist.com/article/2592824-openai-mistranslated-mathematics-into-code-for-its-navier-stokes-proof/

## 摘要

数学家团队指出，OpenAI 的 Navier-Stokes 自然语言证明与 Lean 形式化版本存在差异，但这不代表任一版本无效。Lemma 8.6 中，自然语言版本要求某个值小于 m + 4，Lean 版本却要求小于 m + 5，条件更弱；团队借助 ChatGPT 排查并人工核验，约用两周找到这一差异。