数学的危机时刻：机器一口气证掉七百个难题之后，人类还剩什么

先说结论：这期 Lex Fridman 播客（约三个半小时，依据英文转写整理）自称「紧急专题」，讨论的是他所说的「数学与人工智能的危机时刻」——节目称过去几周里，机器先后声明解决了纳维-斯托克斯方程、准黎曼假设、唯一游戏猜想以及数百个其他结果，费马大定理也被 Anthropic 以 1300 万行 Lean 形式化证明。请来的三位嘉宾是华盛顿大学流体力学专家 Steve Brunton、MIT 理论计算机科学家 Ankur Moitra（本年在普林斯顿高等研究院访问）与罗格斯大学数论学家 Alex（转写未给姓氏，从其 Lean/Mathlib 与解析数论背景疑为 Alex Kontorovich，下文按转写称 Alex）。真正的矛盾不在「AI 会不会做题」——这道题已经有答案了——而在于：当「解出难题」可以从按一个按钮获得，数学共同体过去两百年围绕「谁先解出难题」建立的训练、审稿、奖励与声望体系，都骤然失去了地基。但三位嘉宾几乎都反对按下恐慌键：机器证明的正确性可以验证，而理解、提问与品味仍然稀缺，后者恰好是人的位置。

一个月三连击：费马大定理、纳维-斯托克斯与「七百篇证明的一晚」

按节目中 Alex 的时间线重建，这场冲击是三连击。第一击：Anthropic 放出费马大定理的 Lean 形式化证明——Alex 称其多达 1300 万行、无「sorry」（Lean 中表示待补漏洞的标记）、从公理一路证到定理陈述。冲击感来自落差：他两天前刚在普林斯顿数学系 colloquium 上细致论证「AI 至少还差三年才能做这种远离 Mathlib 库群的工作」，周五结果就掉了下来。他称参与这次形式化的只有两三个人，多数提示词是大写的「继续」，没有领域专家介入——梗图式的说法是提示词就一句「做个突破（do a breakthrough）」。作为对照，节目提到 Kevin Buzzard 拿着五年期百万美元经费的计划，本来只想把费马大定理的证明归约到 1980 年代已知的数学。Alex 的结论是：autoformalization（自动形式化）这个子问题「基本已被解决」，尽管证明本身还是拼凑式的、远达不到 Mathlib 的工程质量。

第二击：Labor Day 假期回来，轮到纳维-斯托克斯方程。Steve 解释，克雷研究所官网列了该问题的四个版本，这次被证的是带光滑外力的「受迫版」——构造出一个三维反例：特殊设计的外力逐项抵消方程中的耗散，涡管像花样滑冰运动员收臂一样被拉长变细，能量保持有限而涡量在细丝上于有限时间爆破。他强调这是数学上的大事（找反例这条路线本身只有约十五年历史），但对工程界「日常几乎完全没变」：流体照样难模拟、风洞照样昂贵，用他的话说，「我们解决的是百万美元的数学题，前面还有万亿美元的工程题」——节目称飞机减阻一个百分点就可能给航空业省下数百亿美元，而湍流预测每改善一点，人工心脏、风机、燃机都会受益。

第三击是压轴的一个周二傍晚：OpenAI 一次性放出约 700 篇证明，含准黎曼假设、唯一游戏猜想、快速傅里叶变换的改进等。Alex 与 Ankur 当晚恰好在纽约国家数学博物馆（MoMath）的晚会上，一手威士忌一手不停刷新手机。Alex 说他看到的第二个条目就是 quasi-RH，当场「无法处理所见之物」；此前数周业内已有唯一游戏猜想、RL=L、矩阵乘法的传闻，Ankur 的第一反应反而是「哇，都是真的，谢天谢地终于放出来了」。节目称 OpenAI 实际提示了数千个问题、只公布解出来的，成功率约一成。至于情绪：Alex 不愿称之为危机，说是「混乱中的机会」、数学从千年烛光换成了手电筒；Ankur 说自己被拉向两个方向——提问与跨界学习的能力被放大，但给学生的人生蓝图失效了，「比以前更智识孤独」；工程师视角的 Steve 整体乐观（人工心脏、飞机、可解问题范围都会扩大），但坦承不确定性巨大：要么被另一种智能完全盖过，要么得到一个超强工具，「这是两个非常不同的世界」。节目还引了陶哲轩（Terence Tao，菲尔兹奖得主）的话：许多以年计、耐心而刻意缓慢的研究努力被一次发布「随意扰乱或摧毁」——「就像无法收回的电影剧透，一旦知道已有解，就无法再那样富饶地探索一个问题」。

凸包还是半群：机器是怎么解题的，边界在哪里

这期最硬的技术讨论，是关于机器证明的「成色」。有人贬低说这些证明都在「凸包」（convex hull）里——全是已知想法的线性组合；Alex 引 Tim Gowers 的说法，更准确的比喻是「半群」（semi-group）：像铺砖，每块砖都是已知的，但可以无限往外铺，能到达的距离远超人类探索过的范围。以准黎曼假设为例：经典结果只给出一条越往上越窄的无零点细带（七十年未挪动，对应素数定理的最好误差项），新证明直接证出 zeta 函数与 Dirichlet L 函数在实部 7/8 到 1 的整条竖直带内无零点（节目称还有第二个 11/12 版本的证明），但所用的每一步招式都是数论学家的「面包黄油」，只是级联方式令人震惊；这套方法原则上够不到实部 1/2，全 RH 仍然需要新思想。关键在于验证：Alex 说该陈述早已在 Mathlib 库里，拿到 sorry-free 的 Lean 证明让他对正确性「百分之百确信」——他已经读过证明，所用思想（如 Möbius 函数与扭曲特征的组合，细节转写疑似）完全合法且出色。

唯一游戏猜想这条线更显出「人机接力」的戏剧性。Ankur 从 SAT 与 P versus NP 讲到上世纪九十年代上过《纽约时报》头版的 PCP 定理、近似难度理论，再到 Subhash Khot 提出的这一猜想为何有「组织整个领域」的力量。他坦承自己原本站在怀疑派——因为它蕴含的结论「太完美不像真」。人类这边并非没有进展：Irit Dinur 与 Dor Minzer（转写两次拼法不一）等人先证出了较弱的 2-to-2 定理（转写读作 two-to-one），被称为理论计算机科学的「响彻世界的枪声」；而 drop 前几小时，Ankur 在 NYU 恰好问 Khot「若他们放出正面证明你读吗」，答曰「不读」——难题被解，出题人反而失去阅读的胃口，这种「雷被别人抢了」的心情是全场的暗线。Ankur 还提到一个 OpenAI 之外的例子：一个 Anthropic 的 3SUM 新算法结果（由其同事 Virginia Vassilevska Williams 与 Josh Alman 撰写，转写疑似）推翻了社区押注，动摇了整个精细复杂度理论的条件硬度大厦。

至于边界，三位给出的是三种「不自欺」的框架。Alex 的判据：AI 尚未给出真正的新定义、新概念——「它还没有做到这一点」；但准 RH 这类结果已经永久改变了边界本身，「改变的不只是可达范围，而是有趣问题的方向」。Steve 反对把「凸包」当贬义：人类自己都没把这个气球内部走遍，雾中给出雷达已是巨大价值；而且人类造新定义、拉出新的边界点，是另一种质变。Ankur 的警告是别把机器拟人化：他用对抗样本研究（前 MIT 同事 Alex Madry 组的「对抗样本是特征不是 bug」）说明深度网络解题方式与人不同，「OpenAI 的那些解看起来不像人做的题」——这个质差恰恰是人机协作（centaur math）的机会，但「下周就可能被证明我错了」。Alex 的自我校准更干脆：「今天说的 40% 到 80% 五年后都会被证错，因为一切变化太快。」

按钮给出证明之后：验证、期刊与知识的重新组织

如果说解题可以被商品化，验证与理解呢？节目里最长的回望是佩雷尔曼与庞加莱猜想：论文挂上 arXiv 后，他到 Stony Brook、NYU、普林斯顿做三小时即兴讲解，全世界的同行用几年时间逐页核到「第 247 页的引理 412」，整个真理确认过程由共同体人肉完成、刻意地慢。这套系统在 AI 之前就已超载——审稿人疲惫、arXiv 洪峰、开源维护者被 pull request 淹没——如今又叠加数百篇机器证明。Ankur 提到已经有人在跑「爬取开放问题、批量产出论文淹没 arXiv」的工作流，「我不觉得那是好策略，肯定不是好玩的策略」。

而 Lean 与 Mathlib 提供了另一条路：把数学变成类似开源软件的 PR 模式——陈述自带规范、引理像零件一样可复用、「不能以错误的方式使用」；Mathlib 十年来的梦想就是让数学「像一门科学一样运转」。Alex 补了两个细节：一是他所谓的「canonization」（把拼凑代码重构入库、找到引理的规范位置）AI 还不擅长，费马证明的 1300 万行正是 jerry-rigging 的产物，把它整理成库质量是接下来「值得做的苦工」；二是论文的「工程」与「叙事」是两回事——他讲了自己教实分析的实验：跳过两周构造实数，直接进 ε-δ 计算，直到 Bolzano-Weierstrass 在有理数上失效才回头问「实数到底是什么」。未来论文很可能是「故事 + 附带的 Lean 形式化」：故事负责让人懂，Lean 负责让机器确认工程上成立。对「黑箱证明」的思想实验，Alex 认为由于逻辑规则与公理只有寥寥数条，不可理解只可能来自规模；Ankur 则提出要发展「unformalize」的能力——把黑箱反拆成可提问的简易版，重建人类层面的理解。

谁得到、谁失去：蓝图、奖项与保密的诱惑

利益图景是这期最现实的部分。直接失去的是「做题家蓝图」：Ankur 说过去带研究生有一张简单地图——挑一个大家关心的问题改进它，发顶会、开门、成名；现在结果多到没人消化得了，蓝图作废，得重新设计制度。奖项体系首当其冲：Alex 说起今年夏天费城上一届菲尔兹奖颁布时，圈内已经在讨论「会不会是最后一届」——按他判断，解大问题不再稀缺，也就不再值钱；他引用佩雷尔曼那句「如果证明是对的，那是我需要的全部荣誉」，以及此人拒领菲尔兹奖与百万美元克雷奖的唯一记录，暗示「佩雷尔曼式价值观」正在从怪癖变成常态。更隐蔽的输家是开放文化本身：Ankur 担心大家会对好想法保密——因为想法一旦流出，AI 最擅长补上缺的那块砖、穷尽整片区域；「先过门者通吃」的旧竞赛规则若不改，数学界最珍贵的开放传统就会受损。节目的地缘注脚同样直白：多项式时间分解整数若被证可行，电子商务与安全通信当场崩塌（后量子密码、格方法因此已在推进）；NSA 雇佣着「数千名」数学家；而有嘉宾直言，OpenAI、Anthropic 真正追逐的是「自我改进的研究者」，这类突破若真出现，公司根本不会发表。Steve 给出一个可迁移的两轴框架：可验证性 × 错误代价——数学证明错误代价低、可验证性极高，是 AI 的完美用例；桥梁、医疗等高代价低可验证领域需要「防火墙」，别让惯性把决策权整体外包。

人的新角色：提问者、建模者，与教育要换的课表

如果解题贬值，什么升值？三位给出的答案高度一致：提问、建模、品味。Ankur 的理论框架是「超越最坏情况分析」：SAT 在最坏情形下没有已知超线性下界，但 SAT 求解器在寄存器分配上好用得惊人——「很多我们当作难的问题实际上是暗自容易的，难的是说清它们为什么容易」；他用《安娜·卡列尼娜》开头作比：问题容易的原因各不相同。他把它推到深度学习：拟合四层网络在最坏情形下是密码学难题，但每天都在被解，「自然界厌恶计算难的问题」——蛋白质折叠的演化实验（只有折叠得好的序列存活下来）说明自然数据被进化「调容易了」，语言亦然，这与 LLM 为何有效纠缠在一起。他在 OpenAI 的 drop 里没有看到任何解释深度学习的结果，这仍是人的大题目；他自己关于低秩语言模型的工作引出了「阈下学习」实验：让模型 A「热爱猫头鹰」再生成随机数，用这些数微调模型 B，B 竟开始逢人就聊猫头鹰——概念远多于维度、向量不正交，微调的外部性可被协调叠加（他比作「通灵板」）。Steve 顺势把多智能体版推向漫画式极端：一个猫头鹰执念在系统里滚四小时，「人都没了、满地猫头鹰」——玩笑背后是对依赖加深后「简单规则涌现极端复杂」的担忧，也是他主张「可证明的严谨」的理由。Steve 对人机分工的另一贡献是方法论：七十到八十年代聪明人问过但撞上计算墙的问题（如湍流的低维坐标）是当下沃土——「坐标变换总是先于物理突破，日心说先于牛顿」；果蝇翅膀上数十到数百个应变敏感神经元做出的局部鲁棒控制，是「不需要解方程也能飞」的存在性证明。

教育一节几乎是一份行动清单。Alex 观察到本科成绩从高斯分布变成双峰：用 AI 检验自己理解的学生成绩上升，只要答案的学生作业与考试脱钩——「要待在分布的头端」。他重提计算器出现七十年后仍要背九九表的教训：当年听信「不必学了」的一代人「承受了大量真实痛苦」。Ankur 的建议最扎心也最可操作：为内在理由做事，因为外部里程碑会先耗尽；「假装你已经赢了，然后问自己会做什么」——他引 Sanjeev Arora 在 MIT 给他的话：拿 tenure 最容易的方式是假装已经有了。还有那条被多人转述的职业三判据：重要、有趣、擅长，得其二已属幸运。Lex 最后把话题落回人本身：Max Tegmark（转写作 Tagmark）说要一半主流一半野路子，Tom Waits 说「我喜欢我的 Tom 里带一滴毒」；而 Alex 的收尾是全场的锚——当智能被 AI 商品化，家人、同事、真实的人才是地基，智力成果只是「旁边的樱桃」。

对行业来说，这一晚的意义不在于某道题被解，而在于「已解决」的定义权移到了拥有模型与算力的公司手里，数学界第一次要在几周内消化别人几十年的积累。接下来值得盯的指标很具体：AI 是否开始提出新定义而不只是组合旧招（Alex 的边界检验）；Mathlib 式集体验证与「论文+形式化附件」能否成为新惯例；期刊、奖项与 hiring 制度如何重写激励；数学家对好想法的保密是否蔓延；以及本科成绩的双峰会不会向上游蔓延到中学。对个人读者，这期给的框架足够清楚：把价值锚从「抵达终点」移到「过程、提问与理解」；用 AI 到达自己的最近发展区而不是代替思考；并且记住 Ankur 的那条反直觉时间观——急着做的、下一代模型肯定能解的题，「不如去度假」，值得做的只有那些多年后你仍然会在乎的问题。

（归属说明：本文事实与引语均来自本期节目英文转写，嘉宾观点为其个人陈述，节目中的结果数量、成功率、时间线均为「节目称/嘉宾称」未经独立核实；转写专名校正：Anker/Encore=Ankur Moitra、Perlman=Perelman、Max Tagmark=Max Tegmark、Langlands tunnel=Langlands–Tunnell 定理、two-to-one 疑为 2-to-2 定理、Virgi Vasilevskaya=Virginia Vassilevska Williams、Camilo de Leles 疑为 Camillo De Lellis、Dor Minzer 转写两次拼法不一；Alex 全程未给姓氏，疑为 Alex Kontorovich 但未在转写内证实；「与 Alex 公理化 solved axiom 的同事 Thomas Coverda」及「Möbius 函数 twisted biseptic 特征」无法确认，保留原文并标注疑似。）