OpenAI数学证明与Lean形式化被指出存在差异

10月10日，Hacker News 首页报道，数学家团队指出，OpenAI 的 Navier-Stokes 自然语言证明与其 Lean 形式化版本存在差异。具体而言，Lemma 8.6 的自然语言版本要求某个值小于 m + 4，而 Lean 版本要求小于 m + 5，后者条件更弱。团队借助 ChatGPT 排查，并通过人工核验，约用两周找到这一差异。报道强调，两个版本存在差异并不代表任一版本无效；目前披露的问题是自然语言证明转为 Lean 代码时的条件不一致。

AI 根据报道生成 · 48 分钟前更新

还没有足够的连续观测数据，暂不绘制趋势。