封面新闻记者 边雪
当地时间9月8日，OpenAI宣布，其AI模型提出了纳维–斯托克斯存在性与光滑性问题的一套解答，并公开了相关论文式证明以及Lean形式化证明。
该消息很快引发关注。纳维–斯托克斯方程是描述流体运动的基础数学方程之一，也是克雷数学研究所2000年公布的七大“千禧年大奖难题”之一。每解决一道题，可获得100万美元奖金。26年来，七道难题中只有“庞加莱猜想”被正式解决。
如果OpenAI此次给出的证明最终得到数学界认可，这将意味着AI第一次可能真正参与到顶尖数学问题的“发现”环节。但现在说“AI已经破解千禧年难题”，还为时尚早。
从“做数学题”到“寻找证明”
纳维–斯托克斯问题真正难的地方，并不是计算量有多大。它试图回答一个看似简单、却困扰数学家数十年的问题：对于描述三维流体运动的纳维–斯托克斯方程，是否始终存在光滑、合理的解？
换句话说，水流、空气等流体的运动，在数学模型中会不会在某一个时刻出现无法控制的“奇点”？这个问题与流体力学密切相关，却远没有普通物理题那么直观。过去几十年，数学家提出过大量猜想，也取得了许多局部进展，但始终没有完成能够解决整个问题的严格证明。
这也是此次OpenAI尝试特殊的地方，它并不是让AI计算一个已经有标准答案的问题，而是让AI自己寻找一条此前并不存在的证明路径。
OpenAI披露，此次系统通过大量AI智能体协同工作，对问题进行拆解、推理和验证。参与工作的AI智能体规模达到约1万个，整个过程持续约88小时。
OpenAI称系统生成了一份解析证明，并将其形式化为 Lean 证明，证明一个初始状态平滑、静止的流体，在有限时间内可以形成一个奇异性（singularity）。研究中对流体施加的是一个平滑的外力，在整个动力学过程中——从流体静止，到最终形成奇异性——其能量始终保持有限。
这一结果通过证明千禧年难题官方表述中的命题“C”以及“D”，解决了 Navier–Stokes（纳维–斯托克斯）千禧年大奖难题。
具体而言，这一解是一种涡旋：流体形成旋转的涡流，逐渐向内盘旋，同时不断沿轴向拉伸，形态类似一根越来越细长的“意大利面”。随着这一中心区域不断收缩，其旋转速度也越来越快，但与此同时，流体的总能量仍保持有限，这符合物理定律的要求。
其中真正的技术难点在于，方程中的这种“失控”必须由流体自身的运动演化产生，而不能简单地通过人为施加一个无限大的外力来制造。更严格地说，描述流体运动的纳维–斯托克斯方程中，加速度、压力梯度、动量传递和黏性等项都必须变得非常大，但又以一种精确的方式相互抵消。
正是这种精细的平衡，使得即便流体速度不断趋于无界，外部施加的力仍然保持平滑。
局部不可压缩流动的可视化。（图源：OpenAI）
这已经很难再被简单理解为“一次AI答题”，而是在尝试搭建一个由AI组成的“数学研究团队”。一个智能体寻找思路，另一些智能体尝试证明，还有智能体负责寻找漏洞。大量探索同时展开，再从其中筛选可能成立的路径。
过去，数学家面对一个重大难题，可能需要几年甚至几十年的时间不断试错，AI正在尝试改变的，是数学家的试错成本。
“AI解出来了”，为什么还不能算正式解决？
OpenAI公布的是其AI系统提出的一套解答。这与数学界正式认定问题已经解决，是两个不同的概念。
克雷数学研究所对千禧年大奖问题有明确的认定规则：相关成果需要在符合要求的学术刊物上发表，发表后至少经过两年时间，并得到数学界的普遍认可，才能进入最终评审程序。
一个证明哪怕只有一个关键步骤存在漏洞，最终结论就可能无法成立。这也是AI参与数学研究之后，一个绕不开的问题。今天的大模型已经可以完成复杂的数学推理，也能够生成看起来高度专业的证明。但“证明写得像数学”，和“证明在数学上成立”，并不是一回事。
OpenAI此次还公布了Lean形式化证明，这也意味着，可以把数学论证转换成计算机能够逐步检查的形式。如果相关证明能够被独立验证，它的可信度显然会高于一段仅供人类阅读的自然语言推理。
但即便如此，也不能跳过数学界的独立检验。因此，现阶段更准确的说法应该是：AI向一个千禧年难题提出了新的解答，而数学界需要判断，这究竟是一项真正的数学突破，还是一个看起来成立、但最终存在漏洞的证明，最终决定它能否写进数学史的，仍然是数学家。
如果OpenAI的证明最终被数学界确认，那么它带来的最大冲击将是AI可能开始从“科研工具”变成“科研参与者”。过去，人们更多把AI理解成一种效率工具，它可以帮助科学家检索论文、整理数据、运行模拟，也可以帮助数学家验证计算。
但科学研究最困难的部分，往往恰恰不是“把答案算出来”，而是找到一个此前没有人走过的路径。如果AI能够在一个数学难题上自主提出有效猜想、构建证明，并通过形式化工具完成验证，那么科研的工作方式可能因此改变。
未来的实验室里，也许会出现这样的场景：科学家提出问题，数千个AI智能体同时探索不同方向；有的负责文献检索，有的负责提出假设，有的负责计算，有的专门寻找反例；最后，人类研究人员从这些结果中筛选、理解并验证真正有价值的发现。
如果AI真的能够在几小时内探索人类数学家可能需要数年才能完成的尝试，纳维–斯托克斯问题最终能不能被AI真正攻克，还需要时间。但人类第一次开始认真面对这样一个问题：当机器不仅能够回答问题，而且开始提出新的数学答案时，科学研究的边界，会走向哪里？
热门跟贴