Claude把千禧年难题做出来了？陶哲轩：我可没这么说

机器之心编辑部 过去一天，一条关于 Claude 的数学传闻在社交媒体上迅速扩散。 昨天，博主 Andrew Curran 发帖「预测」，Anthropic 已经解决了一个千禧年大奖难题，即纳维-斯托克斯方程相关的存在性与光滑性问题，目前成果正在接受专家评审，并可能在 Anthropic IPO 前对外公布。 这条帖子很快获得超过 250 万次浏览，也被越来越多账号转发。 截至目前，公开渠道中还看不到对应论文、证明文本或专家评审材料，Clay 数学研究所仍将纳维-斯托克斯存在性与光滑性问题列在未解决的千禧年大奖难题中。 不过，这条传闻并非空穴来风。它的一个重要背景，来自数学家陶哲轩两天前发布的一组帖子。 一篇关于 AI 的假想 9 月 3 日，陶哲轩以纳维-斯托克斯方程为例，讨论 AI 解决重大开放数学问题之后，可能给数学研究带来的影响。 https://mathstodon.xyz/@tao 纳维-斯托克斯方程描述水、空气等流体如何运动。数学家真正悬而未决的问题，是三维不可压缩情况下，从光滑初始状态出发，解能否始终保持光滑，还是会在有限时间内形成奇点。这个问题已经被 Clay 数学研究所列为千禧年大奖难题，奖金为 100 万美元。 陶哲轩在帖子里设想了一种未来可能出现的研究流程：自主 AI 系统拥有大量计算资源，可以持续尝试不同的数学构造，分析失败原因、调整方案、验证结果，最终形成一个极其复杂的候选证明，并用 Lean 等形式化证明系统完成机器验证。 他的重点是这个过程中产生的数学知识如何保存下来。 在传统数学研究中，一个困难问题往往会在多年探索中产生大量副产品：新的引理、新的工具、新的研究方向，以及之后值得继续研究的问题。陶哲轩担心，如果 AI 在封闭环境中完成整套探索，人类最终拿到一份已经验证完成的结果，很多有价值的中间路径可能很难进入数学共同体。 帖子中的场景写得相当具体：AI 搜索候选结构、进行数值检验、形成庞大的 Lean 证明文件，最后解决纳维-斯托克斯正则性问题。 于是，互联网熟悉的剧情出现了。 一些人开始猜测，陶哲轩是否掌握了尚未公开的信息。社交平台上很快出现「陶哲轩是不是在暗示 Claude 已经解决了纳维-斯托克斯」的讨论，随后 Curran 又给出了更加明确的预测：「Claude 已经解决了纳维-斯托克斯。」这一说法由此迅速传播。 随着猜测扩大，陶哲轩随后专门作出澄清。 他的态度很谨慎：目前他并不了解纳维-斯托克斯问题出现任何重大新进展，此前的讨论属于一个假设性的 AI 研究场景。同时，以现在 AI 技术发展的速度来看，这种场景已经具有一定现实可能性。 他随后谈到了「机会成本」。 像纳维-斯托克斯这样的开放问题，几十年来一直在推动新方法、新问题和新研究者的产生。如果 AI 可以迅速得到最终答案，数学界接下来还需要考虑，怎样把机器探索中的过程、方法和失败路线重新沉淀成可供人类理解和继承的数学知识。 这已经逐渐成为 AI 数学研究中的一个现实议题。 AI 正在改变数学里的「稀缺资源」 这条传闻为什么会如此火爆？ 最近几个月，AI 在数学领域确实接连越过了几个过去很难想象的门槛。 昨天，Anthropic 公布了 Claude 对费马大定理的形式化工作。 https://www.anthropic.com/research/formalizing-fermats-last-theorem 费马大定理早在 1990 年代已经由安德鲁·怀尔斯等数学家证明。几十年来，数学界一直希望把这套极其复杂的证明完整翻译成 Lean 等形式化语言，让计算机能够逐步核查其中每一步。 Anthropic 称，Claude 在 11 天里基本自主完成了端到端的 Lean 形式化，最终代码规模达到约 1300 万行，过程中生成了约 3.03 万个可机器验证的定理，其中约 2.95 万个进入最终证明。参与长期费马大定理形式化项目的数学家 Kevin Buzzard 也对这项结果给予了积极评价。 时间再往前一个月。 8 月 10 日，Anthropic 宣布，一个尚未公开的 Claude 研究模型在尝试黎曼猜想时，对一个相关问题取得了进展：把已知满足黎曼猜想条件的 ζ 函数零点比例下界，从 41.6% 提高到 67.2%。黎曼猜想与素数分布密切相关，也是千禧年大奖难题之一。 https://www.anthropic.com/research/riemann-zeta 今年 5 月，OpenAI 也公布了一项离散几何结果。一个通用推理模型构造出新的单位距离点集，推翻了一个围绕 Erdős 平面单位距离问题长期存在的猜想。相关证明随后由外部数学家检查。这个结果解决的是该问题中的一个重要猜想，整个单位距离问题仍有进一步空间。 https://openai.com/zh-Hans-CN/index/model-disproves-discrete-geometry-conjecture/ 到 8 月，OpenAI 又集中公布了十项数学和理论计算机科学结果，其中包括对多个长期开放问题的解决或实质性推进。 https://openai.com/zh-Hans-CN/index/ten-advances-in-mathematics/ 几年前，大模型在数学领域最醒目的成绩还是奥数题。现在，研究对象已经开始进入开放问题、论文级结果和大规模形式化证明。 AI 对数学界的影响，也开始从能解多少题转向数学家以后主要负责什么。 一个变化是验证的重要性正在上升。 语言模型可以快速生成数量庞大的数学推导，同时也可能产生非常隐蔽的错误。Lean 这类证明助手能够把证明拆成机器逐步检查的形式。随着 AI 生成证明的速度提升，形式化验证正在成为越来越重要的基础设施。陶哲轩此前就多次强调，未来数学研究中的瓶颈可能逐渐转向检查、整理和理解。 https://academy.openai.com/public/blogs/terence-tao-ai-is-ready-for-primetime-in-math-and-theoretical-physics-2026-03-06 第二个变化发生在数学家的工作分工上。 如果常规推导、文献搜索、计算实验乃至部分证明可以交给 AI，人类研究者投入更多精力的地方，可能会转向选题、提出合适的猜想、设计研究路线，以及把机器生成的结果提炼成能够解释的新理论。 陶哲轩把这种未来称为一种「大数学」模式：复杂问题被拆成许多模块，人类、AI 和形式化证明系统共同参与，再通过机器验证把结果重新组合起来。 https://spectrum.ieee.org/ai-in-mathematics 当答案越来越「便宜」，什么才算数学研究真正稀缺的部分？ 过去，一个重要开放问题可以养活一个研究方向几十年。数学家围绕它走过的弯路，本身可能孕育出新的理论。AI 如果大幅压缩这个过程，最终答案会来得更快，同时也要求数学界重新设计一套保存研究过程、分配贡献和培养下一代研究者的方法。 陶哲轩这次拿纳维-斯托克斯举例，讨论的正是这一变化。 至于 Claude 是否真的已经攻克这道千禧年难题，目前仍然停留在社交媒体传闻阶段。 但这场