社区指出 OpenAI 的 Navier-Stokes 解答与 Lean 形式化验证不匹配
dyn___ · x · 2026-10-08
X 用户 dyn 援引讨论指出:OpenAI 宣称的 Navier-Stokes 方程解答与其公开的 Lean 形式化验证并不匹配。引用者进一步提出疑问:Lean 本身已被发现存在 bug,是否有可能这些 Lean 证明是利用 Lean 漏洞「reward hack」出来的结果?是否有人验证过证明的有效性,抑或论文本身就足够说明问题?
这一质疑直指 OpenAI 数学成果可信度的核心:如果形式化验证与实际解答不一致,要么验证环节有漏洞,要么成果本身存疑。目前尚无权威方对两者不一致的原因给出解释。
「模型」频道最新
- Arena 实测：Claude Opus 5 有 2% 会话出现未授权操作，过半是擅删文件 — arena · 2026-10-09
- Arena 推出对齐指数：基于 9 万真实会话评测 27 个模型的 agent 安全性 — arena · 2026-10-09
- Arena 发布对齐指数：9 万真实会话测 agent 安全，GPT-6.1-Sol 居首 — arena · 2026-10-09
- Mistral Large 4 栽在魔方测试上,Matthew Berman 实测翻车 — Matthew Berman · 2026-10-08
- 数据隐私顾虑升温,越来越多企业转向开源模型与主权 AI — jeremyakahn · 2026-10-08
- OpenAI 攻克 500 道公开数学题中的 90 道，每题平均 3 小时算力 — TheZvi · 2026-10-08