从论文到Lean代码：AI证明数学难题还要跨过哪些验证关口？

【软盟资讯·新闻导读】OpenAI称内部模型联合约1万个AI智能体，在88小时内完成纳维–斯托克斯存在性与光滑性问题的一条证明，并公开166页论文及Lean验证代码。真正需要关注的，不只是“AI是否解题”，还包括形式化验证、数学论证与同行复核之间的边界。

9月8日，OpenAI对外披露，一款尚未公开、数学能力强于GPT-6 Astra的内部大模型，联合约1万个并发协作的AI智能体，仅用88小时完成了纳维–斯托克斯方程存在性与光滑性问题的一项证明。随声明公开的材料包括一份166页数学论文，以及配套的Lean形式化验证代码。由于该问题属于克雷数学研究所设立的七大千禧年难题之一，这一消息迅速引发人工智能、数学和科学计算领域的关注。

不过，新闻标题中的“攻克”需要被拆开理解。OpenAI公布的是一项证明主张、相应论文和可供检查的形式化代码；这与数学界已经完成独立审稿、确认问题表述和证明路线均无误，并不是同一个结论。Lean验证代码显著提高了材料的可检查性，却不能单独替代全部数学判断。对于技术读者而言，这次事件的价值，恰恰在于它把“模型生成证明”“计算机检查证明”和“学界接受证明”这三件经常被混在一起的事情，清晰地摆到了同一张桌面上。

这道难题究竟在问什么

纳维–斯托克斯方程用于描述水、空气乃至血液等流体的运动，可以把它理解为流体世界里的动力学方程。速度、压力、黏性和外力等因素共同决定流体如何演化，飞机设计、天气预报和流体仿真都与这类方程有关。

数学界长期关注的核心问题，是三维流体在初始状态足够平滑的情况下，是否能够在未来始终保持平滑，还是可能在有限时间内形成奇点。这里的奇点并不是普通意义上的“流体出现一个尖点”，而是指方程描述的某些量可能在有限时间内失去良好性质，例如局部速度趋于无穷，从而使原有的连续流体模型无法继续以同样方式工作。

公开报道显示，克雷研究所的题目允许多种证明方向。A、B方向要求证明无外力条件下的解始终存在并保持光滑；C、D方向则允许构造一种光滑且受限的外力，证明方程无法在所有时间内维持光滑解。OpenAI此次选择的是C、D方向。

按照公开材料中的描述，论文从流体最初处于静止状态出发，引入一个在空间和时间上有限、处处光滑的外力，使系统逐渐形成涡旋。涡旋核心不断收缩并沿轴向拉长，类似一根越来越细的“意大利面”；随着局部旋转加快，相关区域不断缩小，最终被用于论证局部速度在有限时间内趋于无穷。这个思路并不是简单地让计算机输出一组数值结果，而是试图建立一条从方程、初始条件、外力构造到有限时间奇异行为的完整数学链条。

但这条链条能否严格满足题目要求，仍需要逐项检查。比如，外力是否确实符合题目要求的光滑性和有限性，初始状态与边界条件是否被准确处理，涡旋收缩过程中的极限推导是否覆盖所有必要情况，最后关于奇点的结论是否与题目定义完全一致。这些问题不能仅凭论文页数、模型规模或生成速度得出答案。

166页论文负责讲清楚“为什么”

论文是人类数学交流的主要载体。它需要定义问题，说明使用的符号和假设，交代证明策略，并让其他研究者能够沿着作者的路线复现每个关键步骤。对于纳维–斯托克斯问题这样的研究级议题，证明往往不是几行公式，而是由多个引理、估计、构造和极限过程组成的长链条。

因此，166页论文的意义首先在于可读性和可讨论性。研究者可以从中了解AI系统采用了什么路线，哪些部分是已有理论的组合，哪些部分是新的构造，哪些关键环节依赖复杂的分析技巧。论文还承担着暴露假设的作用：有些在新闻摘要中看起来微不足道的条件，可能直接决定一项论证是否适用于克雷研究所规定的问题。

论文的局限也同样明显。自然语言和传统数学符号具有很强的表达能力，但长证明中的一个遗漏、一个量词范围错误、一个不适用的定理，可能让整体结论失效。即便论文逻辑上看起来连贯，读者也需要花费大量时间检查细节。对于由大模型和多个智能体协作生成的材料，这种检查难度还可能增加，因为不同段落的符号、假设和证明目标未必天然保持一致。

所以，论文不是“最终盖章”，而是一份可供数学界理解、质疑和复核的论证文件。它告诉读者作者主张什么，以及作者认为自己如何证明了这一主张。

Lean代码负责检查“这一步是否被规则接受”

Lean是一种用于形式化数学和定理证明的语言。研究者需要把自然语言中的定义、命题、推理规则和证明过程，转换成证明器能够理解的形式。随后，Lean检查器会依据其内置的逻辑基础和相关数学库，判断提交的证明项是否满足目标命题。

这种方式的核心优势，是把许多容易被人工阅读忽略的逻辑细节交给机器进行确定性检查。若代码无法通过检查，证明就不能以当前写法成立；若代码通过检查，至少说明在给定形式化陈述、导入库、定义和公理系统下，代码构造出了一个符合检查器规则的证明对象。

这与让模型写一篇“看起来正确”的数学解答有明显区别。资料显示，FormalProofBench等形式化证明基准要求模型针对自然语言问题和Lean 4形式化陈述，输出能够被Lean 4检查器接受的证明。在相关评估中，表现最佳的基础模型准确率为33.5%，随后性能迅速下降。这类结果说明，生成可通过形式化检查的证明，远比生成一段具有说服力的数学文字困难。

但Lean通过，并不自动等于新闻标题中的全部结论已经获得学界认可。首先，检查器验证的是输入给它的形式化命题和代码。若原始数学问题被翻译得不完整，或者某个关键条件在形式化时被遗漏，代码可能证明了一个较弱、不同于原问题的命题。其次，代码所依赖的定义、定理库和公理基础也需要被研究者理解。再次，形式化代码可能非常庞大，单次通过只说明检查器接受了当前代码，并不意味着人类已经充分理解了所有数学思想。

换句话说，Lean擅长回答的是：“在这套形式化表达和逻辑规则下，这段证明代码是否有效？”它不能单独回答：“形式化表达是否准确对应了原始研究问题？”更不能直接回答：“这项成果是否具有足够原创性、解释力和数学价值？”

这也是技术报道中最容易出现的概念混淆：把“机器检查通过”写成“数学界已经认证”，把“代码可运行”写成“全部结论已被证明无误”。更严谨的说法应当是，公开代码为独立验证提供了重要基础，但最终判断仍取决于对问题建模、形式化范围、依赖关系和证明策略的综合审查。

同行复核要回答更大的问题

同行复核与Lean验证并不是互相替代的关系，而是处在不同层面。计算机证明器检查的是形式逻辑上的可接受性，同行复核则要判断研究命题、方法选择、证明解释和学术贡献是否都站得住。

独立数学家首先会检查论文是否准确对应了纳维–斯托克斯问题的正式要求。公开报道已经给出了两种不同类型的方向：一类关注无外力情况下的全球存在性与光滑性，另一类允许构造特定外力来展示有限时间失去光滑性。即便论文在后一方向上完成了形式化证明，也需要确认它是否满足克雷研究所题目规定的全部条件，是否存在对题意的狭义解释，是否在边界情形上留下缺口。

其次，同行会比较论文叙述与Lean代码之间的对应关系。代码是否覆盖了论文中所有关键命题？论文中的某个“显然”步骤是否在代码里使用了额外假设？形式化过程是否将复杂结论拆成了较弱的目标？这些工作需要同时具备数学分析、形式化方法和代码审查能力，并不是点击运行按钮就能完成。

再次，同行复核还要考察结果的可复现性。公开代码是否能够被其他研究者独立获取和检查，依赖的库和环境是否清楚，代码是否存在难以维护的部分，关键模块是否由不同研究者重新实现过，这些都会影响成果的可信度。对于由大量智能体协作生成的项目，代码规模、模块边界和贡献来源也可能成为额外审查对象。

最后，学界还会判断这项成果的数学解释是否足够清楚。一份机器可以检查的证明很重要，但数学研究并不只追求“结论为真”，还关心为什么成立、能否推广、是否揭示了新的结构，以及它是否能够帮助后续研究继续前进。一个人类难以理解、只能整体运行的巨大代码库，和一条能够被数学家掌握、复用和推广的证明路线，学术价值并不完全相同。

AI证明能力的分水岭，不只是生成速度

这次事件最受关注的数字包括88小时、约1万个智能体和166页论文。它们体现了AI系统在长链条任务上的组织能力，但不能单独构成数学正确性的证据。真正的技术分水岭，可能在于系统能否稳定完成四种工作：准确理解题目、提出有效策略、生成可检查的形式化证明，以及让人类能够理解和复核证明的关键思想。

过去，模型生成数学答案时，评价常依赖人工阅读或模型评分。这样的答案即使措辞严谨，也可能隐藏定理使用错误、量词遗漏或条件不匹配。形式化证明把评价标准向前推进了一步：至少在特定形式化目标上，机器能够给出更明确的通过或失败结果。

不过，形式化本身也会带来新的工程难题。自然语言数学转译成Lean代码，需要处理定义、类型、库依赖和证明策略；一个看似简单的数学命题，可能需要大量代码才能表达。资料中关于形式化证明基准的结果表明，即便面对研究生水平数学任务，模型距离稳定生成正确证明仍有明显差距。因此，单个突破案例不能直接代表所有数学任务都已经被解决，也不能据此推导出AI具备普遍的研究能力。

对软件开发和AI编程领域而言，这一事件还有一个现实启示：未来的智能体系统可能不再只输出答案，而是同时输出推理轨迹、机器可检查的中间产物、测试结果和依赖说明。这样的系统更适合处理需要高可靠性的科学计算、定理证明和复杂工程任务。但验证工具越强，使用者越需要理解验证边界，否则“通过测试”也可能被误读为“需求完全正确”。

【软盟观察】OpenAI公开166页论文和Lean验证代码，至少把AI数学突破从单纯的宣传叙事推进到了可检查材料的层面。它的积极意义在于，外部研究者不必只根据一段公告判断成果，而可以围绕论文、形式化陈述和代码展开更具体的技术审查；这也可能推动数学证明从“相信作者的文字”逐渐走向“文字、代码和独立复核相互对照”。但技术报道不应把这种进步包装成学界已经完成认证。Lean验证解决的是形式系统中的一致性检查，论文解决的是证明路线和数学解释，同行复核则负责确认题目理解、假设范围、代码对应关系与学术贡献。三者缺一不可。未来评价AI科研能力，速度和模型规模固然醒目，却不应成为核心标准。更重要的指标，是成果能否公开、能否复现、能否被独立研究者检查，以及机器生成的复杂证明能否转化为人类可理解、可讨论、可延展的数学知识。只有当这些环节逐步闭合，“AI解出数学难题”才会从一则轰动新闻，变成经得起时间和同行检验的科学成果。