数学余波

# 数学之后 来源：https://terrytao.wordpress.com/2026/09/12/after-math/ *\本文为客座文章，作者为 Silvia De Toffoli (https://www.silviadetoffoli.net/) 与 Eamon Duede (https://eamonduede.com/)。本博文最初以其他文件格式撰写，并通过人工智能转换。 — T.\]* Silvia De Toffoli (https://www.silviadetoffoli.net/)*（帕维亚高级研究大学学院）* Eamon Duede (https://eamonduede.com/)*（普渡大学与普林斯顿大学）* 2026年9月8日，OpenAI宣布（https://openai.com/index/navier-stokes-solution/），其已产生一个由人工智能生成的、针对Navier–Stokes存在性与光滑性问题的解答——这是七个千禧年大奖难题之一。该公告引发了关于成果归属以及人与机器对该结果各自贡献的辩论。此外，这一声明进一步激化了已有的比较：将此事与此前人工智能在曾被认为能彰显人类智慧的领域中的“征服”相提并论。参与Navier–Stokes事件的数学家之一Tristan Buckmaster在最近的一份声明（https://cims.nyu.edu/~tristanb/statement.pdf）中写道：“这是一个‘深蓝-卡斯帕罗夫’时刻。” 数学的生存性问题随之而来：如果人工智能如今能回答数学最前沿的问题，那么这门学科是否像许多人曾断言的国际象棋和围棋那样，即将被“解决”？如同棋手们，数学家是否也应“继续下棋”，并重组他们的实践方式？ “继续下棋”这一回应有其合理之处。正如哲学家C. Thi Nguyen（2019年 (https://philpapers.org/archive/NGUGAT-2.pdf)）一直强调的，进行一场游戏的目的并不仅限于其目标（获胜）。真正的要义不仅在于结果，更在于过程。这一点在“扭扭乐”这类派对游戏中或许比国际象棋更为明显：玩扭扭乐的目的当然不是赢。但类似的情况也适用于深刻的智力游戏，如国际象棋和围棋。例如，下一局出色的围棋，即使落败，也可能是一种成就。 但在数学实践的语境中，这感觉像是一种不必要的退缩。相反，我们可以采取更强有力的举措：*从一开始就拒绝将数学描述为一种游戏——正是这种描述使得“退缩”显得必要*。 那么，问题不仅在于一旦人工智能能回答数学最难的问题之后会发生什么，还在于我们最初从事数学时追求的到底是什么。 认为人工智能已“解决”数学的叙事建立在两个假设之上，这两个假设都诱人且看似合理，但都是错误的： 1. 人工智能确实解决了一个数学问题。 2. 数学仅仅是关于解决问题的。 第一个假设是错误的，因为要真正解决一个数学问题，仅仅提供一个答案（即使是形式上经认证的）是不够的。缺失的是一个可被人类数学家理解并用以推进数学目标的、可理解的证明。而且，正如我们将在下文论证的，即使人工智能给出了这样的证明，故事也不会结束，因为第二个假设是错误的。数学显然是一项比解决问题广泛得多的事业。数学家努力发展新的概念和理论，提出并解答新的问题，统一不同的领域，教育并维系学术共同体，并创造因其美和深度而备受珍视的作品。 因此，我们可以（并且应该）拒绝人工智能在数学上战胜人类的叙事，并开始认真思考数学究竟是什么，以及我们希望它成为什么。 **并非所有答案都是解** OpenAI对Navier–Stokes方程是否会产生奇点的问题给出了答案：*是*。在《银河系漫游指南》中，Deep Thought对生命、宇宙以及一切的答案是：*42*。两者都并非完全是我们想要的。 当然，OpenAI给出的远不止一个“是”。Deep Thought只提供了一个数字，而OpenAI则产生了两个人工制品，许多人愿意称之为证明。第一个是Lean形式化，用于验证有效性。与之相伴的是一份似乎包含相应非形式证明的手稿。那么，为什么这仍然令人不满意呢？原因与证明本身的基础概念有关。 事实上，存在两种证明概念：一种是*逻辑*概念，另一种是*可理解*概念。 现代逻辑将证明定义为演绎有效性，使得证明可以通过一个无需理解数学论证本身的机械程序来检查。Lean形式化完全符合这些标准，因此，Navier–Stokes结果的Lean形式化是一个真正且重要的贡献：它通过了逻辑证明概念的要求，从而确保了确定性。 但数学家对证明还希望得到更多。他们希望获得理解（Thurston 1994 (https://arxiv.org/pdf/math/9404236)）。他们想知道是什么让一个命题为真。这类知识处理的是数学思想，他们能够掌握、与其他专家交流、与现有知识联系，并用于取得进一步进展。这就是可理解的证明概念。目前尚不清楚OpenAI的结果是否为数学界带来了可理解证明概念所期望的那种价值。 真正的证明同时兼具逻辑性和可理解性。历史上，这两种概念往往交织在一起。这是因为，任何数学家都不可能在首先掌握使定理成立的关键的、可共享的思想之前，就产出极其复杂的逻辑证明。逻辑证明概念主要用于验证可理解证明的正确性（Burgess and De Toffoli 2022 (https://philpapers.org/archive/BURWIM-6.pdf)）。 但随着人工智能的出现，这两种概念现在可能截然分开。我们最终可能得到形式上正确但完全脱离可理解证明的证明。 这并非对形式证明的批评。反过来的问题至少同样严重。一个可理解的数学论证可能传达了一个宏大的思想，却未能确立该结果确实为真。Jaffe和Quinn（1993年 (https://arxiv.org/pdf/math/9307227)）曾著名地以Thurston对Haken三维流形的几何化定理为例：一个伴随不够完整证明的重大洞见，可能会成为“障碍而非启发”。而Hales的Flyspeck形式化项目的一个动机，正是为了验证关于Kepler猜想的可理解（但难以检验）证明确实是一个真正的证明（Hales等人 2009 (https://arxiv.org/pdf/0902.0350)）。 因此，未能达到逻辑或可理解证明概念的任何一方，都会在真正证明本应为数学进步扫清道路的地方制造障碍。一个真正的数学解需要同时满足逻辑正确性和可理解性。 这一点在七大千禧年大奖难题的案例中尤为明显。它们被选中，并非因为数学家仅仅想要七个*答案*，而是因为他们想要*富有成效的解*。克雷数学研究所本身也解释（https://www.claymath.org/millennium/navier-stokes-equation/）了为什么证明在Navier–Stokes问题中如此重要：“因为一个证明不仅提供确定性，还提供理解。” OpenAI给我们的只是一个答案。但尚不清楚他们是否提供了一个富有成效的解。也许我们将来会发现他们确实提供了，但目前情况远未明了。一个真正的解将提供相信该结果的充分理由，同时提供一个可理解的数学论证，使该结果能成为被数学家所理解和实践的数学的一部分。 然而，如果事实证明OpenAI提供的仅仅是一个答案，这并不足以驱散数学面临的生存性威胁。未来的AI系统很可能产出既经过形式认证、又能被数学家完全理解的真正证明。因此，仅仅坚持“真正的解”而非“简单的答案”，并不能完全消除当前关于数学即将被人工智能“解决”的担忧。 **“解决数学”需要的远不止解** 即使未来的AI系统能产出像“大师”数学家那样的真正证明——逻辑正确且可理解，认为数学将像国际象棋或围棋那样被“解决”的想法仍然是错误的。 在国际象棋和围棋中，我们接受人类与机器之间极度不均衡的竞争，因为两者在相关意义上，*进行的是同一场游戏*。 但数学并非（或至少不完全是）一场游戏。首先，它没有赢家。数学不是一场有着明确胜利条件的对抗性游戏。数学家当然会为名声、奖项、工作和荣誉而相互竞争。棋手也会做这些事。但棋手也会赢得国际象棋。数学则没有相应的获胜条件。数学中没有“将死”。 在数学中，将AI视为助手而非竞争对手更为自然。正如Jeremy Avigad（2026年 (https://proofsandprompts.com/2026/09/07/what-is-mathematics-now-and-what-should-it-be/)）所言，“我们应记住，AI无非是为实现我们目标而设计的技术。将数学家与AI视为竞争关系是误入歧途；当我们开车时，我们不是在比谁开得快；当我们使用手机时，我们不是在比谁声音大。” 但在竞争框架之下，存在一个更深层、在许多方面也更先决的问题。它要求接受这样一个假设：解决问题是衡量数学成功与否的活动。 真正地解决问题当然是数学的主要目标之一。然而，它并非唯一目标。数学是一个由学术社群参与、诠释和消化的知识体系，而非一个抽象结果的记录。这一简单的观点甚至催生了数学哲学中的一个完整运动：数学实践哲学 (https://plato.stanford.edu/entries/mathematical-practice/)。 Terence Tao（2026年 (https://arxiv.org/pdf/2608.16753)）列举了数学除解决问题之外的诸多目标。这包括发展新理论和技术、理解世界、维系社群、培养下一代数学家、为累积知识做出贡献，以及创造具有审美价值的作品。当然，这些目标与真正的解是正相关的。 但人工智能打破了这种关联，原因与其分离了两种证明概念相同。因此，即使是真正的解也无法满足我们。 *这不是在移动目标门柱，而是认识到任何特定的门柱都是不充分的。*如果数学是一场游戏，它就是一场无限的游戏。 这种态度并非守旧。我们既拒绝“通过逻辑确立一个定理就足以构成真正证明”的让步，也拒绝将“AI在数学中的应用”简化为证明定理。接受这一点，我们或许能在数学中发现许多支持人类数学繁荣的AI应用机遇。 **余波** 我们不否认，如果OpenAI的宣布属实，这是一项非凡的成就。但我们应该清楚这是何种成就。此刻，它是一个答案，而非一个解。而且，即使该结果最终被证实为一个真正的解，我们也已论证过，在数学实践中，解并非一切。 重新思考我们在数学中珍视何种价值的紧迫性，已在数学界内部得到认识。在一份近期声明（https://mathandai.org/）中（最初由25位菲尔兹奖得主签署），数学家们警告AI公司的目标与数学界目标之间存在“严重的错位”。 数学家需要做更多来审视自身的规范。优先权规范在此并非问题所在（尽管它可能是一个独立的问题）。当前未能区分真正的解与答案，以及日益聚焦于单纯解决问题，才是问题所在。这种思维方式受到了当前数学界荣誉体系的启发，正如David Bessis最近在其博客（https://davidbessis.substack.com/p/the-fall-of-the-theorem-economy）中所讨论的，荣誉体系需要重新思考。 AI带给数学的并非一个终结，而是关于数学实践应成为何种样貌的一个选择。如果数学成功被过于紧密地等同于产出经认证的答案，数学就有可能去适应那些最容易被基准衡量和自动化淘汰的特征。 反之，如果数学家将AI视为推进其长期且核心的人类目标的技术，那么这项技术或许会有助于该学科加速繁荣与丰富。因此，重要的问题并非AI是否会击败数学家，而是我们希望AI服务于何种数学目的。 数学之后留下的，并非仅仅是机器吞噬所有真正问题后供人类争抢的残羹冷炙。相反，它是一个澄清数学究竟为何的良机。我们应再次自问：当我们从事数学时，我们追求的到底是什么。 （本文的扩展版本将在别处发表。）