1. 引言一场关于“让AI去证明NS爆破”的讨论暴露了什么问题上个月在一个AI for Math主题的闭门研讨会上有位做AI infra的工程师放了一页幻灯片PPT上是一个大模型自动生成的泛函分析草稿标题写的是“NS方程有限时间爆破问题的AI证明思路”。底下不少人交头接耳有人问是不是以后我们只要把open problem丢给大模型第二天就能收到一份满是公式的“解”也有人摇头说这种输出只能当梗图发朋友圈当真就输了。当时现场有个做非线性PDE的同行低声说了一句陶哲轩对这种“AI自说自话式”的方案态度一直很微妙。他不是说AI没用而是对“纯AI解决方案”这个说法本身非常警惕。这句话戳中了我。过去一两年AI圈对数学的想象越来越膨胀铺天盖地的热词里“AI agent”“AI编程”“AI大模型”像浪一样涌过来好像任何学科问题只要挂上AI就能顺理成章地变成“自动化求解”。但真正在数学研究一线的人尤其是像陶哲轩这样既深度参与数字化数学、又亲手推动过形式化证明的人看到的完全是另一幅图景。这篇文章想借着“Tao’s reservations on future AI-only solutions to NS finite-time blowup problem”这个话题展开聊聊。我会先把NS有限时间爆破为什么难到足以成为千禧年难题讲清楚再梳理陶哲轩这些年对AI辅助数学的真实立场然后分析一个假设的“纯AI证明”如果直接丢到数学共同体面前会撞上哪些实际障碍最后聊聊在保留意见之下未来的AI到底还能以什么姿势参与这场长达几十年的攻坚。我自己的背景是AI工程实践加一点数学基础既做过模型部署也啃过几本偏分析的教材。所以这篇文章不会写成那种“AI万能论”或者“数学家守旧论”的二极管文章而会尽量还原一个朴素的真相数学信任机制、形式化验证成本和问题本身的内在难度决定了“纯AI-only”在短期内很难真正落地NS爆破这个问题但AI作为深度辅助工具的潜力又比很多人以为的更大。2. 纳维-斯托克斯有限时间爆破短暂时光几十年悬而无解2.1 我到底在说什么从NS方程到“爆破”先给不熟悉这问题的人补一段背景。纳维-斯托克斯方程描述的是粘性不可压缩流体的运动在三维情形下写成∂u/∂t u·∇u -∇p νΔu∇·u 0。其中u是速度场p是压力ν是运动粘性系数。数学上已经知道只要初始条件足够光滑解在局部时间区间内一定存在同时弱解也就是所谓的Leray-Hopf弱解在全局时间上都能构造出来。问题是解会不会在某个有限时刻失去光滑性某个物理范数直接炸到无穷大这就是“有限时间爆破”。想象一根被快速拉伸的涡丝速度场在某个局部区域越来越陡。如果拉伸效应不断把能量送到小尺度而粘性耗散来不及压制速度场梯度就可能在一个有限时刻内趋于无穷。这不是科幻片里的“爆炸”而是数学意义上的解的奇异性形成。如果三维NS方程确实存在这样的初值那千禧年问题中“光滑解全局存在性”就得到否定答案反过来说如果所有光滑初值都能延拓到无穷时间那就要证明一个普遍的正则性结论。两种结果谁都拿不出来这就是问题悬置至今的核心困难。2.2 致命点标度不变性与临界空间为什么这个问题难到几十年没人能彻底攻克一个核心原因是标度不变性。NS方程在时空缩放下有自相似性如果u(x,t)是解那么λu(λx,λ²t)也是解。基于这个缩放关系定义出一系列“临界空间”比如三维情形的L³、L∞、H^{1/2}。在这些空间里解的范数在缩放变换下保持不变或准不变。这意味着什么拿能量估计来说L²范数在二维里可以给出全局控制到三维就不够了。三维NS方程的能量估计只给出弱解层面的全局性而弱解的正则性、唯一性全都在临界下面挣扎。现有的大部分工具比如各种插值不等式和能量方法只能处理“稍微次临界”的情况。想证明爆破就需要在临界空间层面找到一个自相似或近自相似的奇异结构想证明全局光滑又需要在临界空间层面排除这种结构。两边都卡在同一根尺子上。很多初学的人以为NS问题只要算力够强就能数值逼近实际上数值模拟只能告诉你在有限网格尺度下解有没有变大的迹象根本无法判定有限时刻是否真正发生奇点。网格细化、数值误差、边界效应每一个环节都可能在结果里埋雷。2.3 陶哲轩自己的“几乎有限时间爆破”给出了什么线索陶哲轩对这个问题的态度不是围观吃瓜他亲自下场做过一种“几乎有限时间爆破”的约化模型研究。简单说他在一个受NS方程启发的简化系统里构造出在有限时刻爆破的机制但这里的爆破发生在有力的近似和截断修改下不完全等同于原始NS方程。这个结果给数学界传递了两个信号一是提醒大家在靠近爆破临界状态的地方NS家族的动态可以极其丰富二是说明用“找到一个完整自相似机制”的思路去证明真问题还差非常远的距离。我对这个工作的理解是陶哲轩在亲手示范一种正确的研究方式。他没有让程序去自动生成一个几千页的“证明”而是先用人的数学直觉构造出一个约化模型计算实验确认机制再回过头来写严格的分析。这种人脑先设计、计算做验证、最后再形式化的流程才是他认可的工作模式。后面聊AI辅助方案时这条线会一直贯穿。3. 陶哲轩对AI的真实态度支持人类科学家的局限性3.1 一个长期的“数字数学”践行者而不是保守派如果只看“reservations”这个标题容易把陶哲轩误解成AI怀疑论者。事实恰恰相反。陶哲轩可能是当代顶级数学家里最积极地拥抱数字化工具的那个人。他长期维护自己的博客把大量研究笔记公开支持开源数学软件自己也亲身参与了Lean定理证明器社区的相关工作。近些年他和合作者尝试用Lean将一些复杂证明形式化把“人可读的论文证明”变成“机器可验证的代码”。也就是说他对AI-only方案的保留不是来自技术恐惧而是来自他对数学知识生产细节的熟悉。他知道一个证明尤其是一个牵扯到几百条引理、几十个抽象空间嵌入关系的现代分析证明要在机器层面验证到底有多麻烦。纯粹问“AI能不能给一个结论”和大模型能不能把一个完整数学分支形式化完全是两码事。3.2 问题不在AI有没有智能而在“验证”和“信任”陶哲轩在多处公开表达里其实更支持“AI作为辅助助手”的路线AI帮忙做文献归纳、生成形式化草稿、把某个论证段落翻译成机器可检查的代码但最后仍要数学家来设定目标、设计整体结构、审查关键步骤。他关心的核心问题不是大模型够不够聪明而是一个结论要获得数学共同体的接受必须经过“可验证”“可理解”“可复用”三个阶段。这让我想到很多AI工程里的实际经验。你让大模型生成一段部署代码它能跑起来是一回事但你要把它放进生产环境就必须有监控、有日志、有回滚机制。数学证明也是一样甚至更严格。自然语言写成的证明哪怕看起来再合理也要经过同行逐步复核形式化证明则要过编译器这一关。纯AI方案最尴尬的地方在于它既可能产出一个自然语言上的“合理假象”又很难在短期内把所有环节翻译成机器可验证的逻辑链。这不是看不起AI而是工程落地层面的客观约束。3.3 数学共同体如何“接受”一个证明社会学视角陶哲轩作为一位高产数学家对数学知识的社会生成机制理解得很透。一个证明被接受不只是逻辑链条正确还需要被写进教科书、被其他研究者引用、被推广到更一般的情形形成一种“社区记忆”。如果一个AI生成的证明只是冷冰冰的几千页形式化代码哪怕逻辑上无懈可击没有哪个研究组能消化它更谈不上复用和拓展。这个“社会学”层面的隐含阻力是讨论AI-only方案时被忽略最多的一环。我自己参与过一个小型数学实验项目试着用大模型辅助证明一个不太难的PDE引理。它给出的自然语言推导很有“数学味”但中间一步用了一个根本不成立的嵌入关系。如果不是我去人工复核这个错误会悄悄溜进结果。那一次经验让我直观理解了陶哲轩为什么会反复强调“human-in-the-loop”。大模型生成的论证如果不在每个关键节点打上形式化的补丁它对数学共同体来说就像一段没有测试覆盖的生产代码看着能跑却没人敢承接。4. 如果“纯AI证明”真的砸过来会撞上哪四堵墙4.1 第一堵墙高置信度的幻觉比做不出来更危险假设我们真的训练一个AI让它针对NS爆破输出一个五千页的证明然后它也确实“顺利”地生成了。第一个现实问题就是幻觉。大模型的语言流畅性会让它在不确定的地方自动补齐逻辑链条而这些补丁往往是近似合理但严格欠妥的。比如它会假设某个嵌入定理在临界空间也成立或者在交换极限和积分时漏掉一致收敛条件。这类错误在数学验证里非常致命因为它们隐藏在一堆正确的内容中间人力审查成本极高。NS爆破是全称或存在性命题牵涉到无穷维函数空间任何一步松掉条件后面的结论都可能失效。业界一直有人说“AI幻觉会随着模型变大而消失”但数学证明恰恰是最不会容忍这种“近似正确”的领域。你写程序编译器能帮你抓类型错误你写证明除非这一步能被某个定理证明器检查否则人和模型都无法在根源上确认无误。陶哲轩的保留意见里最务实的一条恐怕就是我们还没有一个能够对大段数学证明做完全自动验证的基础设施所以纯AI方案的输出大多数情况下只是“高置信度的臆断”。4.2 第二堵墙形式化定义与知识库的工程量就算我们把目标降低不让AI独立生成最终证明只想让它把论文中的自然语言论证翻译成Lean里的可验证代码也会撞上第二个障碍现有形式化数学知识库的覆盖范围太小。要处理NS爆破至少需要调和分析、插值不等式、算子半群、几何测度论、湍流理论等一大堆子领域的基础结果。每一个子领域要形式化都需要成百上千小时的人力投入。陶哲轩自己参与的形式化项目已经验证了不少前沿结果但离“把泛函分析前沿全面形式化”还有很远的距离。这就像你想让AI当翻译把一篇中文小说翻成一种几乎没人用的小语种但如果这本字典都还没编全翻译得再好也是无米之炊。纯AI证明的难点不只在于“想不出新思路”更在于它没有一个可以展开推理的、覆盖广度和深度都足够的形式化环境。打一个比方大模型可以写出自然语言层面的流畅证明但要进入机器可验证世界需要先有一条长长的高速公路而这条路不是AI能一夜之间铺好的。4.3 第三堵墙可模仿的正例太少反例警告太多数学研究很依赖类比与扩展。AI在大数据模式匹配上的确很强但对NS爆破这种几十年无人攻克的开放问题来说文献里几乎没有“成功证明爆破”的正例可供参考。相反有大量“差一点就成功”的局部结果和反例警告。陶哲轩的约化模型“几乎爆破”实验就是一个典型反例它在修改后的模型里确实爆破但这反而说明原始方程的爆破需要更严格、更巧妙的构造。这种“不能从现有成功路径直接归纳”的局面正好打在AI最擅长的事情之外。我并不是说AI没有归纳能力也不是说它不能从这类反例里学到“什么不该做”。只是当你面对一个反例众多、成功路径为零的问题时生成式的搜索空间几乎是无边无际的。AI在海量组合里找到正确方向的概率并不比一个训练有素的数学家直接看穿关键构造高多少。而且AI没有数学品味它不知道哪些构造更“自然”哪些路径不值得投入。陶哲轩这类数学家最大的优势恰恰在这里他们对数学结构有一种深刻的直觉能在无穷多的组合里先用“审美”筛掉一大批不可能路径。4.4 第四堵墙社会接受与知识传承最后一堵墙也是被严重低估的即使AI真的产出一个严格证明数学界也不一定敢用。这不是说数学家守旧而是因为现代数学高度依赖“可理解的启发式结构”。一个证明如果只是某个AI系统的输出没有人能给出高层直觉那后人在引用它时甚至连该引用哪个部分都不知道。这就像你拿到一份没有注释、没有README、没有测试的代码仓库功能上也许正确但没人敢合并到主干。数学共同体需要的是可教学、可解释、可推广的证明。一个纯AI证明如果不能被“翻译”成一系列有启发性的想法它就成了一个孤岛无法融入学科脉络。陶哲轩谈数学社会学时说得很清楚一个结果要被接受必须在共同体里建立信用而这个信用需要基于人类可理解的推导过程。纯AI方案的逻辑正确性只是必要条件远非充分条件。从整个学术生态来看这个问题比技术问题更棘手也更难用算力堆出来。5. 更可能先出现的是“AI陷阱”陶氏约化模型的启示5.1 约化模型到底做了什么陶哲轩的“几乎有限时间爆破”模型从技术上看是把NS方程里比较复杂的高频相互作用压缩到一组有限维模式把不可压缩条件和涡拉伸机制保留下来舍弃掉一部分Fourier约束。在这个修改后的系统里能量不断被输送到越来越小的尺度粘性耗散跟不上最终在有限时刻产生奇异性。这个结果很惊艳但也很微妙它不能直接外推到原始NS方程。我之前跟人聊这个工作有人问“这难道不是NS爆破的雏形吗为什么不能直接补几个细节就完成证明”答案在于约化模型去掉的那些约束恰恰是原始方程里最难处理的几何结构。原始NS方程中速度和压力之间通过不可压缩条件存在非局部耦合这个耦合会在某些时刻抑制或改变涡拉伸路径。约化模型把它简化成局部的相互作用于是容易爆破。反过来说真实NS能不能爆破就在于这个非局部抑制到底有多强。这个分寸极难拿捏。5.2 AI更可能先“找到”一个假爆破正是因为这个原因我认为未来几年如果真有人用AI硬刚NS爆破最可能先出现的不是证明而是一个“AI陷阱”。大模型会基于文献里关于涡拉伸和能量级联的常见描述生成一个看似合理的自相似爆破构造。它会在数值模拟里表现得很漂亮能量谱也符合某种级联规律但关键的正则性估计在某个尺度上偷换了常量初值可能也不在允许的解析函数类里。这些错误不是随便编故事。你在一个复杂的形式化论证里只要漏掉一项临界范数的控制后面的递推就会垮掉。而大模型在生成过程里没有内建的“数学自检”能力它只会顺着语言模式把故事讲圆。真把这份东西投到arXiv会被同行花很长时间审校因为错误藏得很深。陶哲轩主动构造“约化模型”这个动作其实也是在给这类AI方案打预防针你想证明真问题得先承认约化模型与原问题之间的巨大鸿沟而不是拿一个处处受限的机制当成完整炮弹。5.3 数学家的“蓝图”角色没有消失反而更重要从陶哲轩的实践来看他在约化模型设计里做的事情本质上不是“用程序证明定理”而是“用数学家的方式设计一个机制再让计算去验证它”。这种模式里AI可以承担大量繁琐的中间推导和文献检索但“要构造什么样的模型”“应该在哪个尺度上调整非线性项”这些问题仍然依赖人的直觉。这给AI辅助数学提供了一个很好的参照。你可以让AI帮你搜索“是否存在某种高频模式在NS框架内保持增长”并让它在几百万个候选结构里筛选但你得先知道要去搜这个方向。AI-only方案跳过“前人知道该往哪里看”这个环节直接从混沌里摸大象效率其实很低。陶哲轩对纯AI的保留本质上也是在说在这个问题上有方向的探索和无方向的暴力搜索难度根本不在一个量级。6. 保留意见没有让道路封闭AI辅助NS爆破的落地路径6.1 先搭形式化地基再谈“让AI给出最终答案”如果真想用AI帮助解决NS爆破目前最靠谱的第一步不是训练一个“定理生成器”而是把NS方程相关的基础分析结论一点一点放进Lean这类形式化证明环境。弱解的存在性、局部强解的构造、尺度不变正则性、各种插值不等式都要先变成机器可验证的定义和定理。这工作量很大但它是地基。没有这个地基AI生成的所有“证明”都只能停留在自然语言的黑箱里无法进入严格验证通道。陶哲轩在这件事上是先锋但他也从没说“这几个月就能完成”。他自己参与形式化项目时一个中等难度的结论就需要花费大量精力去处理细节。对普通研究团队来说更现实的做法是选择一个子问题比如“证明某个简化模型存在爆破”先把它整套形式化验证一遍把工具链跑通。等这个流程成熟了再往原始NS方向推进。6.2 “人机双检”工作流人给蓝图AI做执行与验证我比较看好的AI辅助探索模式是“人机双检”。具体来说数学家负责提出一个可能的爆破机制或全局正则性障碍把大方向和策略描述给AIAI负责把这套策略展开成具体的推导并尝试翻译成形式化片段再用另一个独立的验证工具逐段检查。研究者再检查高层的“假设”是否符合物理与数学直觉并把有问题的策略调整掉。这套流程里AI的价值在于快速生成大量候选推导并帮助穷举一些情况下成立的级数估计人的价值在于定义标准、判断方向、处理那些AI完全无法把握的“模式之外”的构造。这不像是“人去监督一台自动售货机”更像是“有一位极其勤奋但容易出错的研究生你作为导师给他布置任务再逐项审查”。陶哲轩的保留意见落到实践层面就是鼓励这种“带着缰绳的AI跑”而不是把方向盘直接交给AI。6.3 AI真正能贡献的几个非神话任务比起“让AI证明NS爆破”这种宏大惊悚标题我更愿意列几个短中期可行、又能逼近大问题的实际任务。找到合适的突破口比空喊AGI好得多。任务核心难点为什么AI参与值得尝试引理库推荐巨量文献中哪个引理适合当前场景大模型在语义检索上有天然优势能给出候选范围不等式常数搜索多次插值后的临界常数是否统一数值实验可以帮助快速缩小可行区间给证明者提示反例模式识别构造一个让某类估计失效的几乎反例AI可以组合已知“陷阱模式”生成试探性结构形式化翻译把论文里的手写推导转成Lean可检查代码大模型擅长语法转换再由人复核逻辑细节这四个任务没有一个是“全自动产生一个震撼证明”但它们组合起来能在真实意义上推进NS爆破研究。陶哲轩自己也在系统里做过类似事情用形式化工具检查推导、用AI辅助翻译、用计算实验观察趋势。所有这些都在“纯AI-only”和“完全不用AI”之间画出了一条中间路线。6.4 我的实际体会AI是探照灯不是预言家我试着做过一个很小的实验让大模型帮忙查找某个与Sobolev嵌入有关的反例它确实给出了一个我很陌生的构造方向。去查文献后发现那个方向确实有相关例子只是表述方式不同。那一刻我意识到AI在“扩大搜索半径”这件事上非常有价值。它帮你照亮那些你本该看到但忽略了的角落而不是凭空告诉你终点的样子。NS爆破问题也是一样。AI真正的用武之地不是直接生成定理而是在浩如烟海的文献和想法里帮数学家标记出那些“值得深挖的线索”。陶哲轩对未来纯AI方案的保留不是要把AI关在数学门外而是提醒我们一个证明只有经过人的理解、审查和传承才能成为数学的一部分。AI可以是极其出色的探照灯但真正的登山者仍然要是能看懂地形的人。