OpenAI 纳维-斯托克斯证明获同行认可：Lean 形式化通过编译
basedjensen · x · 2026-10-12
- 数学家 Obhishek Saha 澄清争议：据多位同行细查，OpenAI 给出的证明是正确的，可终结此前的质疑与不实信息。
- 自然语言版证明与 Lean 形式化版本并不完全相同：策略一致，但关键引理表述不同——Lean 版更弱，自然语言版更强，其中部分陈述有误或未严格证明。
- Lean 形式化证明成功编译，目前审查未发现错误或对形式系统的操纵。
- 证明包含大量真正的新想法，以复杂且非平凡的方式组合。basedjensen 感叹：之前总说 AI 无法发明新数学。
所属事件:OpenAI 纳维-斯托克斯证明经核查无误(3 条相关)→
「漫话AGI」频道最新
- 博士生两难:狂发 AI 论文还是慢工出细活? — SeaAccomplished441 · 2026-10-14
- AI 发现药物该署名吗?科研署名制度遭遇挑战 — yi111 · 2026-10-14
- 时间less决策理论会不会屈服于勒索？一场决策理论圈细节争论 — jessi_cata · 2026-10-14
- 聚合全球算力建开源超级智能,从笑谈变行业共识 — willcb · 2026-10-14
- Robert Wright《造神之约》中文版上市：呼吁 AI 治理国际合作 — wfithian · 2026-10-14
- Mike Knoop 盘点 2026 AI 颠覆:程序员不再读码、数学难题告破 — mhmazur · 2026-10-14