百万美元悬赏没领,但「谣言一出、算力压平」已成数学前沿的新现实。
事实
- OpenAI 称内部系统对 Navier–Stokes 存在与光滑性问题给出解:光滑三维不可压流体动力学可在有限时间发展出奇点(陈述 C/D)。
- 证明经 Lean 形式化;代理约万级并发,约 88 小时得到解、再约 17 小时用 GPT-6 Astra 做 Lean;文中称另有内部模型「显著强于 GPT-6 Astra」。
- Concurrent Work:曾听说 Alpöge/Buckmaster 进展,后知对方是强迫 Euler 等;OpenAI 称证明不同,并写「不能排除其使用我方产品的去标识化数据帮助了模型」。
- 不申请 Clay 千禧年奖;讨论里 Tao 谈「有人在做的传闻」即可触发大规模 AI 压平。
解读
- 数学产品叙事若同时甩「更强内部模型」与「不能排除用户数据」,信任会立刻变成主议题。
- 形式化(Lean)把「AI 解了」从公关句变成可复核工件——这是科研发布的正确产品形态。
- 对研究工具平台:用户会话里的洞察是否进训练,要写成可审计默认,而不是事后一句免责。
讨论
- 正方有人视作 AI 已站在数学发现前沿;Lean 让主张可核验。
- 反方大量讨论指向 Buckmaster 声明:是否 scoop、是否用了 Codex/用户洞察。
- 共识必须与同日 Tristan Buckmaster PDF 帖对照读,不能只看 OpenAI 通稿。