在一场10月2日的 World Science Festival 访谈中，数学家 Tristan Buckmaster 介绍了一项由 AI 生成的结果；他认为结果正确，但其他数学家很难读懂。他的讲述将近期 Navier–Stokes 声明引出的疑问说得更具体：当易读的解释还需要进一步工作时，研究共同体如何检查一个形式化论证？
Buckmaster 谈到他与 Levent Alpöge 关于带光滑外力的三维 Euler 方程的工作。他们的结果不同于OpenAI 9月8日提出的声明，后者涉及带光滑外力的 Navier–Stokes 方程。Navier–Stokes 方程包含黏性，Euler 方程则没有。OpenAI 发布了一篇论文和 Lean 形式化文件，支持其关于有限时间内发生奇异的主张。负责管理 Millennium Prize 的机构尚未宣布颁奖。
重大变化
- 变化之处：Buckmaster 首次亲自讲述了如何使用 AI 生成的论证和 Lean 建立另一项受迫 Euler 结果，以及向数学家解释此类证明仍需开展哪些工作。
- 这为何重要：形式化检查可以确认编码后的论证是否由指定的定义和依赖关系推出。数学家还需要理解定理的含义、其思想如何运作，以及它借鉴了谁的先前工作。
- 后续观察：Clay 对 OpenAI 的 Navier–Stokes 声明进行评估、出现易读的证明说明，以及关于作者身份和访问权的公开讨论，都将显示这一结果如何被评价。Buckmaster 对结果的信心是专家观点，并非颁奖决定。
经过检查的论证仍需要解释
在这场访谈中，Buckmaster表示，人工智能为他的Euler结果生成的第一份证明中，既有有用的思路，也夹杂着无关计算和难以阅读的表述。他的团队先借助其他智能体逐步检查论证，随后将其转写为Lean以进行形式化验证。他说，尽管呈现方式不佳，最终证明仍然正确。这段讲述针对的是他的 Euler 工作；不应将其理解为他独立核验了 OpenAI 另一篇 Navier–Stokes 论文的每个部分。
这种区别有实际意义。Lean 会在指定的证明环境中检查精确定义的命题，但它本身不会让长篇论证变得易读，也无法自动帮助研究者复用其中的方法。Buckmaster 告诉 Brian Greene，其他 AI 系统能够解析一些他几乎读不懂的段落；请 AI 将其改写成普通数学语言也成为工作的一部分。他还说，尽管已发表的 PDF 很难读，他仍能理解 Navier–Stokes 论证中的思想。这些是他的评估，并非 BIG CHANGE 对证明的审计；我们没有运行 Lean 文件，也没有评审任一条定理。
NYU Courant 的9月14日报道将 Buckmaster 和 Alpöge 的成就描述为：带光滑外力和有限能量初始数据的受迫三维 Euler 方程在有限时间内失去正则性。报道说，合作团队的三篇论文均以 Lean 形式化，并将结果置于 Diego Córdoba 和 Luis Martínez-Zoroa 开创的研究路径中。准确分配贡献时，这些细节很重要：模型生成的证明可以延展现有数学路径，同时不抹去奠定该路径的人。
快速发展的一系列事件中的两个结果
OpenAI 表示，其内部智能体系统最初产生了一个关于无外力 Euler 方程的结果，随后将这一研究方向用于其另一项 Navier–Stokes 构造。其公告承认 Buckmaster 和 Alpöge 在受迫 Euler结果上的优先贡献，同时称自己的证明是独立开发的。Buckmaster 在访谈中表示，这些数学机制彼此相关，并称 OpenAI 增加了一个关于涡旋塌缩的想法来处理黏性。双方叙述都认为这些主张涉及不同方程和证明步骤，但并未解决所有关于时间先后或智力贡献的问题。
欧洲数学 学会欢迎了这项公告，同时强调此前的工作，并呼吁关注作者身份、贡献归属以及对内部模型的访问权。Clay 在9月11日的回应称 Navier–Stokes 问题似乎已经解决，但对成果的评估和贡献归属将谨慎进行，不会仓促决定。Buckmaster 告诉 Greene，他相信 OpenAI 已有解决方案。读者可以同时接受两种说法：专家的正面判断，以及机构仍在进行评估。
最近OpenAI 另外三篇数学手稿撤回是另一件独立事件。他们报告的符号错误说明应逐一检查各项主张；但这并不证明 Navier–Stokes 证明也有同样错误。BIG CHANGE 的仓库检查指南说明了如何查找手稿版本和证明材料；我们的评审能力观点则认为，解释和检查需要专门支持。先前的 Navier–Stokes 报道记录了这一系列事件的起点。这次访谈补充了一位在职数学家的讲述：AI 系统提出论证之后会发生什么。
对于如此重大的主张，接下来有用的出版物包括精确易读的说明、可检查的形式化材料，以及独立的数学回应。它们各有作用。生成候选证明的速度让这些工作更加紧迫，而 Clay 声明的流程也为谨慎处理留出了空间。
来源与延伸阅读
- World Science Festival 10月2日的节目确认了访谈日期和参与者；访谈视频是 Buckmaster 本人讲述的来源。他的评估均归于本人。
- NYU Courant 9月14日的报道说明了 Buckmaster 和 Alpöge 的受迫 Euler 结果、此前的数学工作以及 Lean 形式化。
- OpenAI 9月8日发布、9月10日更新的公告,介绍了其声称的受迫 Navier–Stokes 构造、公开论文和 Lean 形式化，以及对同期工作的说法。这是提出结果一方的叙述，并非独立认可。
- Clay 9月11日的声明阐明了其谨慎的公开立场和评估流程。European Mathematical Society 9月10日的声明讨论贡献归属、来源脉络和访问权。
- BIG CHANGE 关于最初 Navier–Stokes 报道、仓库检查、评审能力观点以及另外三篇手稿撤回报告的报道，提供了这条发展中故事的背景。
