OpenAI宣布已经证明千禧年七大难题之一。《量子杂志》（Quanta Magazine）速度真快，已经发表了一篇报道文章《AI攻克了价值100万美元的数学界“千禧年大奖难题”之一》。#OpenAI宣布攻克千禧年难题#
下面是全文翻译：
9月8日星期二上午，OpenAI的数学家们宣布，在他们的指导下，一组由10,000个自主AI智能体组成的团队（运行在一个未向公众开放的高级模型上）在三维纳维-斯托克斯（Navier-Stokes）方程中发现了一个“奇点”——从而解决了克雷数学研究所于2000年提出的六个尚未解决的千禧年大奖难题之一，每个难题的奖金为100万美元。他们的结果已经使用编程语言Lean进行了形式化验证，这让数学家们确信其确实是正确的。
如果这一结果能够经受住进一步的审查，它将毫无悬念地成为迄今为止由人工智能模型得出的最重要的数学证明，甚至可能标志着数学家解决难题方式的一个根本性转折点。
这个特定的难题涉及微分方程，这类方程表达了变化量之间的关系。可以说，它们是解释我们周围世界最重要的一种数学工具。通常来说，微分方程写出来容易，解起来却很难。
纳维-斯托克斯方程是利用牛顿第二运动定律来描述流体（从洋流到气流）行为的微分方程。它们最早在19世纪中叶被写下，从那时起就一直是流体力学研究的核心。但关于这些方程的一个基本问题一直存在：它们的解总是“表现良好”的吗？或者，它们的解是否会随着时间演化，使得流体中极小的一部分开始以无限快的速度流动，从而产生所谓的“奇点”？
在OpenAI宣布找到这个寻找已久的奇点的12小时前，纽约大学的特里斯坦·巴克马斯特（Tristan Buckmaster）刚刚宣布，他与Anthropic的勒文特·阿尔珀热（Levent Alpöge）在各种AI模型（包括OpenAI的模型）的帮助下，解决了几道密切相关的问题。
这两支使用AI的团队都严重依赖马德里数学科学研究所的迭戈·科尔多瓦（Diego Córdoba）和CUNEF大学的路易斯·马丁内斯-佐罗亚（Luis Martínez-Zoroa）的研究成果。这两位研究人员开发了一种攻克该问题的策略，这与大多数数学家正在使用的方法截然不同。
“得知这个问题被解决，我感到非常激动，”普林斯顿大学的查尔斯·费弗曼（Charles Fefferman）说，他曾撰写了克雷数学研究所纳维-斯托克斯问题的官方描述。他说，这个故事的英雄是科尔多瓦和马丁内斯-佐罗亚。正如巴克马斯特在宣布其成果的声明中所写的那样：“让我在公开场合重申我私下对同事们说过的话：鉴于这项工作，我认为路易斯·马丁内斯-佐罗亚理应获得菲尔兹奖。”
【非凡的“奇点”】
纳维-斯托克斯方程依赖于一个假设：你可以不断放大流体，考量其无限小的部分。现实世界并非如此：流体最终是由分子和原子组成的，它们并非绝对平滑。这意味着有关奇点形成的数学结果并不具有任何直接的现实影响。然而，这些结果很重要，因为即使在理想化的意义上这种奇点是可能存在的，这也足以令人惊讶。它告诉我们，尽管牛顿第二运动定律看起来很直观，但它应用于流体时的结果却极其反直觉。换句话说：湍流比它看起来还要诡异。
纳维-斯托克斯方程考虑了流体具有粘性或摩擦力的事实。（粘性较大的流体，如蜂蜜，流动缓慢；而粘性较小的流体，如水，流动较快。）一组更为简单且相关的方程被称为欧拉方程，它描述了粘度为零、流动时没有摩擦的流体。这两组方程密切相关——研究人员经常并行研究两者。但哪怕只是引入极小的一点摩擦力，也会导致流体的行为发生深刻的变化。
（注：原文配图显示OpenAI的解是一个漩涡，其中黄色代表较快的旋转速度，蓝色代表较慢的旋转速度。）
“十年前，没人相信纳维-斯托克斯方程存在奇点，”科尔多瓦说——尽管许多人相信欧拉方程确实允许奇点的存在。这种看法在2013年开始转变，当时加州理工学院的侯一钊（Thomas Hou）和现任教于香港恒生大学的罗果（Guo Luo）得出了一个突破性的结果，表明如果将圆柱体的上下两半设置为反向旋转，欧拉方程可以在圆柱体中“爆破”——这是数学家们惯用的说法。“那是第一个真正严肃的奇点声明，”科尔多瓦回忆道。在接下来的几年里，一系列成果（包括一篇2019年的论文）让数学家们开始思考：不仅欧拉方程可能存在奇点，纳维-斯托克斯方程也可能存在。
从那时到今天，还需要跨越几个学术上的台阶。首先是边界问题。千禧年大奖版本的难题，问的是在向各个方向无限延伸的三维空间中会发生什么。早期的结果（如2013年的圆柱体研究）都假设了某种边界的存在。费弗曼表示，这些都是有用的中间发现，但没有边界的情况在数学上更有趣，因为在带有边界的模型中，找到奇点“只能说明流体由于与边界的相互作用而形成了奇点——但在没有边界的情况下，则是流体自身在做疯狂的事情。”
下一个主要步骤涉及对引起流体运动的力进行建模。这些力可能是像重力将流体向下拉扯这样自然的力量，也可能是像螺旋桨这样的人为干预。数学家使用一种称为“强迫”的技术来对这些力进行建模。他们有时会尝试引入笨拙、难以处理的强迫函数，以使流体表现出奇怪的行为。但千禧年大奖版本的难题，问的是当强迫函数在数学上表现良好或“平滑”时，会发生什么。
在他们2013年的圆柱体研究中，侯一钊和罗果使用计算机模型模拟了一种可能导致欧拉方程爆破的场景。随后，他们通过计算排除了所有潜在误差，证明了爆破确实会发生。自那以后的几年里，类似的技术成为了攻克欧拉和纳维-斯托克斯问题的主流方式。
但是在其2021年的博士论文中，马丁内斯-佐罗亚首创了完全不依赖计算机的分析技术。这让他和他的博士导师科尔多瓦成了该领域的“异类”。到了2023年，两人已经证明了带有复杂强迫函数的一个版本的欧拉方程存在奇点。
科尔多瓦喜欢开玩笑说：“我不用AI：我有路易斯。”马丁内斯-佐罗亚补充说，这并不是说他们俩反对AI，而是“直到最近，当我试图将它用于自己的工作时，它与我的工作流程不是很匹配。显然，我得去适应它。”
概括来说，这两人的技术依赖于创建一个无限的“层”序列，其中每一层都是他们正在研究的方程的非奇点解。（他们已将类似的技术应用于欧拉方程、纳维-斯托克斯方程以及其他相关系统。）然后，他们将这些解通过马丁内斯-佐罗亚所称的“无限级联”结合起来，生成一个新的解。
他们证明，这个新解包含了所期望的奇点。然而，尽管每一层单独来看都依赖于平滑的强迫函数，但将它们结合在一起可能会导致强迫函数产生不合需要的数学特性。这就是为什么他们的解没能满足千禧年大奖标准的原因。剩下的障碍是弄清楚如何创建一个类似的无限级联，使其不仅能产生奇点，还能保持平滑的强迫函数。
这正是这两个相互竞争的AI团队似乎取得成功的关键步骤。
【激动人心的结合】
就在科尔多瓦和马丁内斯-佐罗亚致力于完善其技术的同时，基于AI的数学研究正处于一种“狂飙”状态。自初夏以来，大型语言模型（主要来自OpenAI和Anthropic）已被用于获取许多数学领域的证明结果。通常，这些结果都伴随着形式化证明，它们依赖编程语言Lean来以无懈可击的确定性证明某个陈述必须为真。（仍然必须由人类完成的关键验证步骤是：确保在Lean中被证明为真的陈述，在逻辑上等同于数学家最初想要证明的内容。）
在整个夏天的大部分时间里，这种竞争就算称不上友好，至少也没有公开的火药味。但在过去的24小时里，情况发生了改变。
9月7日星期一午夜前夕，巴克马斯特发布了一份声明，宣布了他与阿尔珀热的合作成果。“在过去一年的大部分时间里，进展都很缓慢，”巴克马斯特在声明中说。但到了8月22日，他们已经获得了一个经过Lean验证的欧拉方程证明：“我可以这样说，勒文特发给我的第一个由LLM生成的证明，是我读过的最糟糕的东西，”巴克马斯特写道。
两人本计划继续打磨，写出一份更优雅的报告，但在他们的进展风声走漏给OpenAI之后，他们觉得必须提前发布的时间表。巴克马斯特感叹道，他与阿尔珀热发布的这三篇论文中，有一篇“只能被描述为AI生成的垃圾。我对此感到抱歉。”
OpenAI承认，他们对纳维-斯托克斯方程的研究是受到了“阿尔珀热和巴克马斯特已经解决了一个千禧年大奖难题”这一传闻的启发。（事实上他们并没有完全解决，尽管他们表示，对于一个稍微简单版本的纳维-斯托克斯方程，他们有一个尚未验证的爆破证明。）使用了一个新的内部模型，OpenAI部署了不同规模的自主AI智能体群来攻克欧拉和纳维-斯托克斯问题的变体。该公司在一份新闻稿中写道：“近100个智能体协同工作了大约50个小时，得出了我们对欧拉正则性的反证。”随后，他们部署了一个规模更大的智能体群——大约10,000个——来攻克纳维-斯托克斯问题。88小时后，运行在内部模型上的智能体得出了纳维-斯托克斯方程存在奇点的证明，再经过17个小时，另一个AI模型将该结果形式化。总的来说，这些智能体之间发送了近500万条消息。OpenAI的塞巴斯蒂安·布贝克（Sébastien Bubeck）估计，计算成本高达数百万美元。
在本文发稿时，巴克马斯特、阿尔珀热和OpenAI之间互动的细节仍扑朔迷离——对话的各方对此给出了不同的说法。OpenAI将3D欧拉方程结果的优先权让给了巴克马斯特和阿尔珀热，但声称自己拥有纳维-斯托克斯结果的优先权。在巴克马斯特的声明中，他似乎暗示OpenAI的研究人员或他们的AI智能体，可能获取了（并从中受益）他与阿尔珀热使用OpenAI模型所做的工作数据。
厘清谁在什么时候做了什么的时间线，以及理解新AI证明的数学意义（即使它们已经被形式化验证），还需要一些时间。但无论如何，这项工作在学术上对科尔多瓦和马丁内斯-佐罗亚的借鉴是显而易见的。“我为特里斯坦感到非常高兴，”马丁内斯-佐罗亚说。“如果能由我们自己完成这件事那真是再好不过了，但我依然为他感到非常高兴。”
