关于纳维-斯托克斯千禧年奖难题

计算、成本与方法论

• 评论者估计，按 Astra 的公开价格，约 3000 亿输出 token 的成本大约是 1500 万美元；有人指出 OpenAI 的内部成本更低，但仍然非常高。
• 该系统使用了约 1 万个并发代理，持续了约 88 小时。有人将其视为“数据中心里的天才国家”；也有人认为这只是蛮力加大量人工引导，而不是干净利落的“一次性” AGI。
• 不少人指出，提示链、工具使用和人工指导都相当复杂，而博客文章淡化了人为参与。

优先权争议与剽窃担忧

• 另一支团队大约花了一年时间，使用 Codex/LLM 在高度相关的 Euler/NS 工作上推进；他们的公开声明指控：
  • OpenAI 是在听到有关千禧年奖难题解法的传闻后才开始他们的工作。
  • 他们的 Codex 会话里包含草稿和关键想法。
  • 关于这些聊天是否被用于训练的问题并没有得到明确回答。
  • OpenAI 曾提出联合发布，但以放弃 Anthropic 关联合著者为条件，并据称使用了威胁职业发展的措辞。
• OpenAI 的回应（在帖子和社交媒体上）声称：
  • 他们从未访问过任何特定的私密聊天。
  • 该模型的证明，甚至精确的 Euler 结果，都不同。
  • 用户数据可能以“去标识化”的形式贡献了训练信号；他们“不能排除”这种可能。
• 讨论分裂为两派：
  • 一方认为这很可能是知识产权泄露/“抢跑”客户使用其自身数据。
  • 另一方坚持没有具体的不当行为证据，相关指控需要证明。

数据使用、隐私与信任

• 讨论重点集中在训练开关（“为所有人改进模型”）以及退出是否真的能阻止原始数据或“去标识化”数据被使用。
• 有人认为 OpenAI 可以也应该判断特定聊天是否进入训练；也有人说，规模和去标识化使这在实践上不可行，或者会侵犯隐私。
• 许多人得出的结论是，研究人员应避免在未发表工作上使用专有 LLM（或要求严格的零数据保留）。

对数学与研究文化的影响

• 反应不一：既有对千禧年难题被攻克的惊叹，也有对其实现方式的失望。
• 有人担心，关于进展的传闻如今会触发大规模 AI 努力，在人类项目成熟之前就“抹平”开放问题，把数学推向保密（“认知黑暗森林”）。
• 有人认为这展示了 AI 前沿推理能力并预示 AGI；也有人将其类比为 Deep Blue 或国际象棋引擎：在狭窄且可充分验证的领域里超越人类。

Lean 形式化与正确性

• 许多人强调 Lean 证明是正确性的强证据，甚至可能比传统同行评审更强。
• 也有人指出：
  • Lean 命题必须与 Clay 问题完全一致，这仍需要人工检查。
  • 证明助手过去出现过 bug，因此仍需要一定的人类审查。

更广泛的社会与就业影响

• 讨论聚焦于这是否会加速一场威胁知识工作岗位的“智能爆炸”，还是只是把人类推向更高层次的任务。
• 不少人认为这是一个分水岭时刻；也有人警告，不应把单一的高知名度数学结果过度解读为通用 AGI。