Lean 通过的证明也可能证错题：OpenAI 流体奇点结果待数学界核验
MasterWitcher69 · reddit · 2026-09-19
围绕 OpenAI 关于 Navier-Stokes 问题的结果，作者梳理了「Lean 形式化验证通过 ≠ 问题被解决」的关键区别。
OpenAI 声称其系统构造了一个从静止出发、施加光滑外力、并在有限时间内发展出奇点的光滑三维流体，并发布了经 Lean 检查的形式化证明。但 Lean 只验证结论从编码后的定义和假设中逻辑推出——仍需有人确认这些定义准确对应 Clay 数学研究所的原始问题。
作者用工具 Apodex 把 OpenAI 的报告、Clay 官方问题陈述与解释逐条对照，检查初始条件、外力、能量界和奇点声明是否对得上。结论是双向都要谨慎：
- 「Lean 检查过所以正式解决」说过了头
- 「用了外力所以不算」可能也错，因为官方表述在指定条件下允许光滑外力
Clay 奖的规则要求结果在合格刊物发表、发表后至少两年、且获得数学界普遍接受后才可评审。作者最后提出核心问题：做形式化证明的人如何核对 Lean 中编码的定理就是人类想证的那个定理？
「漫话AGI」频道最新
- 观点:AI 代理将成为商店本身,购物不再需要打开浏览器 — armand_ruiz · 2026-09-19
- 「post economic」成旧金山约会圈新词,折射AGI财富预期文化 — signulll · 2026-09-19
- 安全研究者不满同行押注两年内ASI「foom」,忽视渐进式对齐方案 — tszzl · 2026-09-19
- 500 个 LLM 智能体在模拟 X 上零人类干预跑通完整宣传攻势 — ziv_ravid · 2026-09-19
- Chalmers 与 Robert Long 同框 ConCon,AI 意识研究大牛齐聚 — RosieCampbell · 2026-09-19
- 《心灵捕手》恶搞版：LessWrong 论坛青年的「拯救人类」 — csuwildcat · 2026-09-19