前DeepMind工程总监David Budden高调宣称用AI证明纳维-斯托克斯等三大千年难题并下注数万美元，引发AI幻觉还是数学革命的激烈争论。
前谷歌DeepMind工程总监放话：我证明了纳维-斯托克斯千年难题，还赌上1万美元！
就在今天，整个数学圈和AI圈炸锅了！前DeepMind工程总监David Budden突然在X（原Twitter）上公开宣称，他已经完整证明了千禧年七大数学难题之一的“纳维-斯托克斯存在性与光滑性问题”，并承诺将在当晚发布端到端的Lean 4形式化证明。
更夸张的是，他当场下注1万美元，押自己是对的！这还没完——他还顺带放出消息说，霍奇猜想的证明也已搞定，计划明年一月正式发表。
甚至，有传言称他接下来还要挑战BSD猜想，赌注金额已累计高达4.5万美元！
这消息一出，Reddit的r/singularity板块直接爆贴，566个赞、219个踩，评论区彻底分裂：有人高呼“AGI已来”，也有人直接嘲讽“AI精神病发作”。更有网友扒出他最近推文语气极度膨胀，甚至开始自比“当代牛顿”，种种迹象让人不得不怀疑：这到底是数学史上的重大突破，还是一场精心策划的AI幻觉式营销闹剧？
纳维-斯托克斯问题到底在问什么？用“五岁小孩”都能听懂的话解释
先别急着膜拜或嘲笑，咱得搞清楚这个问题到底多难。简单说：纳维-斯托克斯方程是描述流体（比如水、空气）如何流动的基本物理方程。工程师用它设计飞机、气象学家靠它预测台风、F1车队拿它优化尾翼。但问题来了——这些方程在数学上有一个致命漏洞：我们不知道它们是否“永远稳定”。
更具体地说，千禧年难题问的是：如果你给流体一个“合理”的初始状态（比如平静的湖面突然扔进一块石头），这些方程能不能永远给出“光滑、有限”的解？还是说，在某种极端条件下，流速或压力会突然“炸开”成无穷大（数学上叫“奇点”或“blow-up”）？如果真的会“炸”，那就意味着这套用了150多年的流体力学基础理论，在某些情况下会失效——哪怕现实中流体由原子组成，根本不会真的出现无穷大，但数学模型本身的崩溃，足以动摇整个连续介质力学的根基。
正如Reddit用户svideo精准总结：“这不是关于真实世界的流体，而是关于数学本身的命运。它在问：这套方程会不会‘发疯’？”
David Budden是谁？从DeepMind高管到“千年难题破解者”的离奇转身
这位David Budden可不是无名之辈。他曾是DeepMind的工程总监，主导过多个前沿AI系统架构，属于谷歌AI帝国的核心技术骨干之一。但就在最近，他突然离职，创办了自己的AI初创公司，并把全部精力押注在“用AI解决数学难题”上。据他在推文透露，他并未接受过系统的数学专业训练——没有数学本科，更别提博士。他的背景是计算机工程和机器学习。
这就让整件事更显诡异：纳维-斯托克斯问题是20世纪最艰深的偏微分方程难题之一，连菲尔兹奖得主陶哲轩都曾坦言“我们几乎一无所知”。霍奇猜想更是代数几何中的珠穆朗玛峰，需要用到层论、上同调、霍奇结构等极高深的抽象工具。一个非数学出身的工程师，一个月内连破两大千年难题？这概率比中彩票还低，除非……他手握某种超越人类认知的AI武器。
Lean 4形式化证明：是“真证明”还是“AI糊弄学”？
Budden强调，他的成果不仅有手写证明，还有完整的Lean 4形式化代码，号称“端到端可验证”。这立刻引发了Lean社区的激烈争论。要知道，Lean是一种交互式定理证明器，要求每一步推理都严格符合逻辑规则，不能有半点模糊。千禧年难题的形式化本身已是巨大工程——GitHub上有个开源项目LeanMillenniumPrizeProblems，花了9个月才勉强完成纳维-斯托克斯问题的“陈述框架”（见下文），但核心定义仍大量使用sorry（即“此处留空，日后补证”）。
而Budden声称自己一夜之间就写出了“完整证明”。但很快有专家扒出他发布的代码片段，发现其中大量依赖native_decide这类“黑箱”战术——相当于告诉Lean：“相信我，这段是对的，别问为什么”。这在学术界等同于“用Wolfram Alpha算2+2=4，然后交卷”。真正的数学证明必须展示完整推导链。正如Reddit用户ferminriii讽刺：“老师要你展示解题过程，你却交了张截图说‘计算器说对了’”。
更关键的是，有AI（如Gemini 3）分析后指出：Budden的代码只是构建了一个“归约框架”——即“如果以下五个公理成立，那么纳维-斯托克斯解就不会爆”。但问题恰恰在于，这五个公理本身就是原难题的等价表述！等于说，他把原问题换了个壳，再声称已解决。这在数学界属于经典的文字游戏。
三大千年难题连破？还是AI幻觉的完美风暴？
除了纳维-斯托克斯，Budden还宣称已证明霍奇猜想和BSD猜想。这就更离谱了。霍奇猜想横跨代数几何与拓扑，BSD涉及椭圆曲线与L函数——三个问题分属数学中几乎不相交的领域，各自需要数十年专业积累。历史上从未有人能同时精通这三个方向，更别说一次性破解。
大量评论直接指向“AI幻觉”：Budden很可能用Claude、Gemini等大模型生成“看似专业”的证明草稿，再因自身数学素养不足，无法识别其中逻辑漏洞。正如用户BaudrillardsMirror所言：“几乎可以肯定，是LLM幻觉出一个证明，而他没能力看出错在哪。”
更有阴谋论者猜测这是一场病毒式营销：用1万美元赌注博眼球，为自家AI初创公司造势。毕竟，如果最后证明是假的，三个月后没人记得；但如果万一蒙对了……那直接封神，100万美元奖金+无限流量，回报率爆表。
千年难题的Lean形式化现状：GitHub开源项目揭示真实难度
回到那个GitHub仓库（https://github.com/lean-dojo/LeanMillenniumPrizeProblems），我们能看到真正形式化的艰辛。该项目明确标注：
- 黎曼猜想：⭐⭐⭐⭐⭐（完整）
- 庞加莱猜想：⭐⭐⭐⭐⭐（完整，因已证）
- 纳维-斯托克斯：⭐⭐⭐⭐☆（近完整，但定义依赖sorry）
- P vs NP：⭐⭐⭐⭐☆
- BSD猜想：⭐⭐⭐☆☆
- 霍奇猜想：⭐⭐☆☆☆（部分）
- 杨-米尔斯存在性与质量间隙：⭐⭐☆☆☆（部分）
特别值得注意的是，纳维-斯托克斯的形式化虽标注“近完成”，但仍依赖大量未证明的底层定义。作者坦言：“我非数学家，形式化可能有误，请指正。”而霍奇与杨-米尔斯因涉及高深数学，完成度最低。这恰恰说明：Budden声称的“端到端证明”远超当前社区能力，除非他拥有某种内部黑科技。
如果是真的？数学界将地震，AI将封神
当然，我们不能完全排除奇迹发生的可能。如果Budden真的成功了，意义远超100万美元奖金：
首先，这是人类首次用AI（或人机协作）解决千禧年难题，直接证明AI具备前沿数学发现能力，AGI进程将大幅加速。
其次，纳维-斯托克斯的证明可能揭示流体“奇点”是否可能，为湍流理论提供全新视角——尽管未必直接提升天气预报精度，但可能催生新的数值模拟范式。
第三，霍奇猜想一旦解决，代数几何、数论甚至弦理论都将迎来革命。BSD的证明则能彻底改变密码学与椭圆曲线加密的基础。
正如Reddit用户Interesting_Phenom所说：“如果他用AI做到这点，那比任何AI基准测试都更能证明AI的进步。”
但更可能的结局：一场AI时代的“LK99式”闹剧
回看2023年的LK99室温超导闹剧——也是由非主流团队高调宣布，全球实验室疯狂复现，最终证伪。Budden事件正在重演这一剧本：高调宣告 → 社群沸腾 → 代码漏洞曝光 → 舆论反转。
目前已有多个迹象表明事态不妙：
- 他发布的Lean代码被指“只是框架，非真证明”；
- 推特账号行为异常，疑似情绪亢奋（manic episode）；
- 数学界几乎无人背书，反而集体质疑；
- 他本人后续改口称“只是归约框架，非端到端”。
若十天后（他承诺的arXiv论文截止日）无实质内容，这场闹剧将迅速退潮。但其警示意义深远：AI让“伪科学”生产门槛急剧降低。以前民科写篇论文要数月，现在LLM几小时就能生成“貌似严谨”的数学证明。如何区分真突破与AI幻觉，将成为AI时代的新挑战。
尾声：我们为何如此渴望“奇迹”？
其实，Budden事件之所以引爆舆论，深层原因是人类对“智能奇点”的集体焦虑与期待。在AI日新月异的今天，我们既恐惧被取代，又渴望见证历史性突破。当一个前DeepMind高管宣称用AI破解千年难题，无论真假，它都成了我们内心希望的投射。
但数学终究是铁律的领域。千年难题不会因流量或赌注而低头。真正的证明，需要经得起全球顶尖数学家长达数年的 scrutiny。无论Budden是疯子、骗子还是天才，时间会给出答案。而在这之前，请记住陶哲轩的忠告：“如果你认为自己解决了纳维-斯托克斯问题，先别急着发推，去找一个懂PDE的专家聊聊。”