OpenAI 用 Lean 证明受迫 Navier-Stokes 流可承载通用计算
anderssandberg · x · 2026-10-16
Anders Sandberg 推荐 OpenAI 数学堆里他最喜欢的成果：论文《Universal computation in forced Navier–Stokes flows》及配套 Lean 形式化（openai/math 仓库第 376 号文档）。
- 核心思想：给定通用图灵机和程序，可在三维环面上构造随时间变化的力场驱动流体，让流体粒子按计算结果被输运到表示 "0" 或 "1" 的盒子，从而用流体检测任意有限机器的停机。
- 形式化范围：在每个正的可计算粘度下，从静止、零压力出发给出光滑不可压缩解，力场无散、空间均值为零且时间一周期，并对所有混合导数给出有效界；粒子停机探测器与固体盒子上的互易映射不在该形式化范围内。
- Sandberg 评价：结果并不太令人意外（此前早有猜想），但把这件事向前推进了一步。
所属事件:OpenAI 证明受迫 Navier-Stokes 流可承载通用计算(5 条相关)→
「漫话AGI」频道最新
- 恶意软件作者驳「AI 蠕虫」报道:这是武器化虚假信息 — dyn___ · 2026-10-17
- 热论：机械可解释性并非对齐的真正瓶颈 — ShahabBakht · 2026-10-17
- 牛津学者迎新演讲：AI 时代学数学与哲学从未如此紧迫与诱人 — raphaelmilliere · 2026-10-17
- Aura 创始人：债券市场显然已相信奇点将至 — tszzl · 2026-10-17
- MIRI 遭抨击:批评者称 Yudkowsky 是「低水平知识分子开皮包慈善」 — inductionheads · 2026-10-17
- 有 AI 反而更累:工程师自述 vibe coding 加剧职业倦怠 — kmeanskaran · 2026-10-17