2026年9月8日，OpenAI（OpenAI）宣布其生成了纳维-斯托克斯存在性与光滑性问题的AI解法，该问题是七个千禧年大奖难题之一。这一公告引发了关于荣誉分配以及人类与机器在此成果中各自贡献的辩论，也加剧了将此次突破与此前AI在象征人类智力优势领域取得胜利的比较。参与该难题的数学家之一特里斯坦·巴克斯特（Tristan Buckmaster）在近期声明中称这是深蓝-卡斯帕罗夫（Deep Blue–Kasparov）时刻。

2026年9月8日，OpenAI宣布用AI生成了纳维-斯托克斯存在性与光滑性问题的解，这是七大千禧年大奖难题之一。该声明引发关于功劳归属及人机贡献的争论，也加剧了将此事与早先AI在看似人类智力典范领域取得胜利的比较。参与此事的数学家特里斯坦·巴克斯特在近期声明中写道：“这是深蓝对阵卡斯帕罗夫的时刻。”

自然浮现数学的生存问题：若AI已能解答数学最前沿问题，这门学科是否如许多人所言象棋围棋那样濒临被“解决”？数学家是否该像棋手一样“继续下棋”并调整实践？

“继续玩”的回应有些道理。哲学家C. Thi Nguyen（2019）一直强调，玩游戏目的不止于获胜；重点不仅是结果更是过程。派对游戏如Twister比象棋更明显：玩它肯定不为赢。但类似逻辑也适用于围棋等深度智力游戏，下好一局即便输了也是成就。

但在数学实践语境中，这像是不必要的退让。我们可做更强反击：拒斥将数学视为游戏这种设定，正是它让退让显得必要。问题不仅是AI能答最难问题后数学还剩什么，更在于我们做数学究竟追求什么。

AI“解决”数学的叙述基于两个诱人却错误的假设： 1. AI真解决了数学问题。 2. 数学只关乎解题。

第一点错在：真解决数学问题，仅给答案（即便形式验证）不够，缺的是人类可理解并用以推进数学的可理解证明。即便AI给了可理解证明，故事也未结束，因第二点错。数学显然是比解题更广的事业：数学家致力发展新概念理论、提出回答问题、统一领域、教育维持社群、产出以美和深度受珍视的工作。因此我们该拒斥AI击败人类数学的叙述，认真思考数学真正是什么、我们想它是什么。

并非所有答案都是解

OpenAI对纳维-斯托克斯能否产生奇点给了答案：能。《银河系漫游指南》中Deep Thought给了生命宇宙一切的答案：42。两者都不尽如人意。

当然OpenAI给的不止“是”。它产出两件多人称证明的物件：一是Lean形式化验证，附带着似乎是相应非形式证明的手稿。为何仍不满意？关乎证明的概念本身。

证明有两种：逻辑的证明与可理解的证明。现代逻辑按演绎有效性刻画证明，可由不需理解论证的机械程序检查。Lean形式化恰满足，因此是确保确定性的真正贡献。但数学家还想要理解（Thurston 1994）：他们想知道命题为何真，这种知识关乎可把握、可交流、可联已知、可推进的观念。这是可理解证明。目前不清楚OpenAI结果是否给了此类价值。

真正证明同时是逻辑与可理解的。历史上两概念常合一，因无人能产出极复杂逻辑证明而不先把握使定理真的观念；逻辑证明主要用于验证可理解证明（Burgess and De Toffoli 2022）。但AI让两概念可能分离，我们或得到脱离可理解证明的形式证明。

这不是对形式证明的批评。反问题同样严重：可理解论证能传达宏大观念却未确立结果真。Jaffe和Quinn（1993）以Thurston几何化定理为例：重大洞察伴不完整证明成“路障而非启发”。Hales的Flyspeck形式化项目动机之一正是验证Kepler猜想可理解（但难查）证明是真证明（Hales等 2009）。

因此，缺逻辑或可理解都制造路障，真正数学解需两者。七大千禧问题被选是因数学家要丰硕解而非仅答案；克莱数学研究所解释纳维-斯托克斯为何证明重要：“因为证明不仅给确定性，也给理解。”

OpenAI给的是答案，但不清楚是否给丰硕解。或许将来发现是，但此刻远未明。真正解将提供相信结果的理由，也使结果成为数学家理解实践之数学一部分。然而，若OpenAI仅给答案，也不足以消除数学面临的生存威胁，因未来AI可能产出既形式验证又完全可理解的真正证明。当前担忧数学被AI“解决”不能仅靠强调真正解而非答案来消解。

要“解决数学”仅靠解还不够

若未来AI产出如“大师”数学家般的真正证明（逻辑正确且可理解），仍不能认为数学被“解决”如象棋围棋。象棋围棋中我们接受人机不对等竞争，因他们“玩同一游戏”。但数学不是（或仅）游戏：首先无赢家，它非有确定胜利条件的对抗游戏。数学家确为名声奖职竞争，棋手也如此，但棋手还赢棋，数学无对应条件，无数学将死。

数学中更自然视AI为助手而非竞争者。Jeremy Avigad（2026）说：“谨记AI无非技术，设计服我等目的。视数学家与AI竞争是误导；开车不是比谁快，用电话不是比谁大声。”

但竞争框架有更深问题：它要求接受解题是衡量数学成功的活动的假设。真正解题确是主要目的之一，非唯一。数学是被社群参与解释消化的知识体系，非抽象结果登记处，这甚至催生数学实践哲学。Terence Tao（2026）列了解题外的目的：发展新理论技术、理解世界、维持社群、培训下一代、贡献累积知识、创作审美价值作。这些与真正解正相关，但AI打破此相关，因同它分离两证明概念之理。所以即便真正解也不满足我们。这不是移动球门，而是承认任何具体球门都不充分；若数学是游戏，它是无限游戏。

此态度非保守。我们既拒斥逻辑证定理即足真正证明的让步，也拒斥“数学AI”缩减为证定理。接受此，我们或发现AI支持人类数学繁荣的许多机会。

余波

我们不否认若OpenAI声明正确，这是非凡成就，但应澄清其类型：此刻它是答案非解。即便将来显为真正解，我们已论证数学实践中解非一切。

重新思考数学价值的急迫性已被社群认识。近期由25位菲尔兹奖得主初始签署的宣言警告AI公司目标与数学社群目标“严重错位”。

数学家需更多检视规范。优先规范非此问题（虽或是另题）。当前未能区分真正解与答案、日益仅聚焦解题才是，此思维受数学功劳经济启发，David Bessis近期博客讨论功劳经济需重思。

AI给数学非结束，而是关于数学实践应成何样的选择。若数学成功过密等同于产出验证答案，数学风险调适至最易基准化自动化的特征。若数学家视AI为推进长远人本目的的技术，技术或促学科加速繁荣丰富。故重要问题非AI会否击败数学家，而是我们欲AI服务何数学目的。

余波中留存的非机器吞尽真问题后人类争抢的残羹，而是澄清数学究竟为何的机会。我们应再问做数学追求什么。

社区对AI进军数学难题的反应陷入分裂：多数人质疑AI真正解决了数学，强调可理解证明、归因与人类过程不可替代；少数人认为形式证明已足够，且AI将服务于更广阔的社会目的。

认为AI没有给出真正的数学解决

• 仅提供答案甚至形式认证不够，数学需要人类能懂的证明来推进；OpenAI只走最后一步，无法向训练数据中的数学家致谢，不配得 credit（较多人） > 仅给答案即使形式认证也不充分，这会把数学贬为可悲的数字诗歌（@octoberfranklin）

认为AI附带的形式证明已足够

• 证明已附上，否定其“不提供理解”是拔高门槛；LLM 可自身推进数学目标，只需让模型消化这些证明（少数人） > 说“不提供理解”不否定存在形式证明，这是在强加超出所需的证明要求（@charcircuit）

认为数学价值在于人类过程与目的

• 类比艺术生成，外行难辨但过程本身是创意核心；数学同理，只衡结果让专家难解释，且数学应为人类理解否则尊严难守（较多人） > 正如艺术不只有产品，数学同样关乎人类求解过程本身，而非仅结果（@camillomiller）

担忧AI导致数学家存在主义危机与社群纽带失落

• 自动化带来“目的死亡”普遍恐慌，失落感源于领域内同志情谊与共同目标，多数人终将适应重定位（较多人） > 因创新速度，每个人类都将体验因自动化而失去目的的恐慌，但会接受并重塑目标（@yazaddaruvala）

认为AI目前仅能暴力证伪未威胁创造性

• 当前 AI 只展示暴力证明存在性、反例，相当于数学除草；创造力提升慢，离创造性解题尚远（较多人） > 眼下AI只会暴力证明存在或反例，离创造性解题尚远，只是在做数学除草（@zarzavat）

认为AI将让数学更雄心勃勃或作为工具服务社会

• 如软件原型降低风险，数学也可更敢尝试；数学本为全人类实用价值，AI出结果好事，目标仍是理解世界（少数人） > 数学本为更广人类提供实用价值，AI能得出结果实属幸事，抱怨者如同马车夫哀叹汽车（@dash2）

认为数学家未来在转译AI证明或提示工程

• 需要快速理解输出的提示工程师；翻译神谕证明成职业但非初衷；对齐需模型互解释留面包屑（较多人） > 数学需要一类能快速理解AI输出的特殊提示工程师，这将是数学家的未来（@brador）

反对以AI暂不能做之事定义自身价值

• 以“AI不能做Y所以安全”是移动球门；从高中到千禧年问题耗时极短，研究 horizon 超两年即危险（高赞/较多人） > 若只以AI尚不能做的事来定义自身价值，很快会迎来残酷醒悟，进步速度已远超读博（@sigmoid10）

公共资助数学研究模式需因AI重新评估

• 数学靠公共资金因信其促科学，若AI更好服务，终身职位增减与资助方向成真问题（少数人） > 无人讨论是否应因AI突破调整数学研究的公共资助，这与体育自费不同（@reisse）

有价值的补充

• OpenAI 呈现的证明读起来像嗑药所作，需二次转译或精简版才能产生正面影响（@niemandhier）
• 若强AI发展出创造性大局解题，其对数学的影响远比对社会经济的冲击次要，因创造力解锁全新经济能力（@zarzavat）