「解决了千禧难题」这个说法要减掉一项
传播里最容易丢失的是那个外力项。这次证明的对象，是一个从静止开始、全程被施加一个光滑外力的流体，结论是它会在有限时间内形成奇点。经典的千禧问题问的不是这个——它问的是无外力（或者说在标准设定下）的三维纳维–斯托克斯方程，解是否永远光滑地存在下去。 OpenAI 自己把话说得比多数转述更克制：它称这确立了官方表述里的陈述 C 和 D，并且明确表示不申领奖金。这个自我设限比结果本身更值得记——一家有强烈动机把成果说大的公司，主动划了边界。 克雷数学研究所的规则也决定了这件事没法快：奖金要在经同行评审发表、并经过两年社区验证之后才可能授出，历史上只授过一次（庞加莱猜想）。所以即便争议全部解决，时间表也是以年计的。
88 小时、1 万个 agent、1300 亿 token
方法侧的数字是这条新闻里最实的部分：近 1 万个 agent 并行推进，首批启动后约 88 小时得到结果，其间 270 万条消息、约 1300 亿输出 token；之后 GPT-6 Astra 又花 17 小时把证明写成 Lean 并通过验证。 值得注意的是这和上周 Anthropic 的费马大定理形式化不是一回事。那一次是把已有的人类证明翻译成机器可验证的形式——新的是验证。这一次声称的是新结果，Lean 只是最后的把关环节。两件事放在一起，大致划出了当下 AI 在数学上的两条战线：把旧结论变得可机器检查，和在有明确目标的问题上并行搜索新证明。
优先权争议没有定论
Buckmaster（NYU 数学教授）称 OpenAI 是在得知他与 Levent Alpöge（Anthropic 员工）正用某一特定方法攻关相关问题之后才启动的，并对私有的 Codex 使用材料是否起过作用提出疑问。 OpenAI 的说法是：9 月 1 日因听到一则传闻而开始，9 月 6 日完成证明与 Lean 验证后主动联系对方，提出同步发布并承认其优先权；研究员和 agent 在公开之前都没有看到对方的工作，也没有访问特定用户数据，但它不能排除来自产品使用的去标识化数据曾帮助改进模型；并称两份证明差别显著，在欧拉方程的情形下证的是不同结果（有外力与无外力之别）。Buckmaster 方面则称他们在 8 月 22 日已经有了欧拉方程的 Lean 验证证明。 还有观察者指出这项工作对 Córdoba 与 Martínez-Zoroa 早前研究存在明显的智识继承。这些分歧目前都没有第三方结论，写的时候只能把两边的说法并列。 同一周还有一件相关的事：在 771 位数学家联署公开信之后，OpenAI 退出了对 Caltech Mathathon 的赞助——联署者反对让本科生用 200 万美元的 AI 额度去攻公开问题，担心产生大量未经验证的「劣质数学」，并把核验成本转嫁给数学界。把这两件事放在一起，数学社区眼下要处理的不只是「AI 能不能证」，还有「谁来验、验的代价谁付」。
via: OpenAI《On the Navier–Stokes Millennium Prize Problem》、Quanta Magazine 报道、Scientific American 报道、The Next Web 关于公开证明与不申领奖金的报道