Lean 通过的证明也可能证错题：OpenAI 流体奇点结果待数学界核验
MasterWitcher69 · reddit · 2026-09-19
围绕 OpenAI 关于 Navier-Stokes 问题的结果，作者梳理了「Lean 形式化验证通过 ≠ 问题被解决」的关键区别。
OpenAI 声称其系统构造了一个从静止出发、施加光滑外力、并在有限时间内发展出奇点的光滑三维流体，并发布了经 Lean 检查的形式化证明。但 Lean 只验证结论从编码后的定义和假设中逻辑推出——仍需有人确认这些定义准确对应 Clay 数学研究所的原始问题。
作者用工具 Apodex 把 OpenAI 的报告、Clay 官方问题陈述与解释逐条对照，检查初始条件、外力、能量界和奇点声明是否对得上。结论是双向都要谨慎：
- 「Lean 检查过所以正式解决」说过了头
- 「用了外力所以不算」可能也错，因为官方表述在指定条件下允许光滑外力
Clay 奖的规则要求结果在合格刊物发表、发表后至少两年、且获得数学界普遍接受后才可评审。作者最后提出核心问题：做形式化证明的人如何核对 Lean 中编码的定理就是人类想证的那个定理？
「漫话AGI」频道最新
- Chollet 提问:单细胞如何仅靠基因组信息把自己连成大脑 — CatAstro_Piyush · 2026-11-04
- 美国多数情侣如今相识于数据中心，线上已远超办公室 — menhguin · 2026-11-04
- Sam Altman:我们离科学发现里程碑比预期更近 — ChrisGPT · 2026-11-04
- 独立研究者开源 10 年数学成果：14.6 万文件，AI 加速三年成型 — HamOnWhy · 2026-11-04
- RLHF 标量奖励藏着 2450 年前的老问题:有用与无害是对抗的两股力 — vasilisvj · 2026-11-04
- Gary Marcus 称 AI 幻想收割变难，美股期货与亚洲半导体股已下跌 — GaryMarcus · 2026-11-04