OpenAI 纳维-斯托克斯证明争议拆解：Lean 版可自动验证，人读版被挑出漏洞
qi2peng2 · x · 2026-10-10
作者自学梳理了 OpenAI 数学证明风波的技术背景：
- 问题是什么：纳维-斯托克斯方程是流体动力学的数学模型，一个悬而未决的公开问题是它在特定技术条件下（如三维不可压缩、密度恒定的流体）是否会发展出奇点——这里的奇点是数学/物理意义上的无穷小或无穷快，与 AI 无关
- OpenAI 做了什么：展示了两种形式的数学证明，一个用 Lean 编程语言写成（可自动机检证明正确性），一个是人类可读版本，针对该问题的一个特殊情形；证明结论是该特殊情形下奇点存在
- 争议所在：约一个月后，数学家们声称在 OpenAI 发布的人读版证明中发现了问题——这也正凸显了 Lean 形式化验证版本的价值：机器可检验，不受人读版的歧义和疏漏影响
这条线索对理解 "形式化验证 vs 人读证明" 在前沿 AI 数学成果中的角色很有参考价值。
「漫话AGI」频道最新
- 神经网络的末代Clippy:未对齐AI自我重构却毁掉继任者 — repligate · 2026-10-10
- Friedberg 称 OpenAI 数学成果未发密码学证明,或预示重大突破引发加密货币安全担忧 — firstadopter · 2026-10-10
- AI 能做一切时，做个人还有什么意义？ — understated_quokka · 2026-10-10
- AI 研究员的人类智能上限，可能严重制约 AI 进展 — fkasummer · 2026-10-10
- Reddit 热议:UBI 的数学账根本算不通,钱从哪来? — Amphibious333 · 2026-10-10
- 对话式 AI 或 1-2 年内过时,Agent 蜂群将推高流量千倍 — dumpshoot · 2026-10-10