7.1
深览指数
科技Bestblogs·Lex Fridman··AI 生成
AI 引发的数学危机：Navier–Stokes、黎曼猜想与复杂性理论｜Lex Fridman 播客第 503 期
Lex Fridman 与 Brunton、Moitra 及化名 Alex 的数论研究者讨论据报由 AI 取得的数学突破，核心区分是「形式正确」与「人类理解」：Lean 能检查证明步骤，却无法解释结果为何成立。嘉宾逐一澄清准黎曼结果、带强迫项 Navier–Stokes 爆破、唯一博弈猜想各自的问题边界，Moitra 用 SAT、PCP、近似算法论证最坏情况复杂性不能概括实际可学习性。适合关心 AI 数学能力与科研制度的人。原文 ↗
核心观点
- ▍数学工作的核心价值不在得到一个被验证的定理，而在形成思想、抽象、解释和人类理解；更好的问题本身仍是数学工作的一部分。
- ▍形式化（Lean/Mathlib）改变的是数学知识的分享与检查方式，但形式证明检查与解释结果为何成立是两种不同的劳动。
- 01嘉宾明确区分完整黎曼猜想与更弱的无零点条带结果，指出准黎曼结果不能等同于完整猜想。
- 02Brunton 区分了据称在带强迫项 Navier–Stokes 方程中构造爆破的结果，与实际预测、控制湍流和逆向设计等工程问题。
- 03Moitra 借助可满足性问题（SAT）、概率可检验证明（PCP）、近似算法、在线算法和自然数据，说明最坏情况计算困难性无法概括所有实际问题的可学习性。
- 04讨论提出一个假设性的「已解决公理」：AI 是否最终能独立完成任何人类与 AI 合作能完成的事；嘉宾强调这不是对当前系统能力的既定描述。
- 05关于隐性学习的讨论把数学模型与隐藏行为迁移风险联系起来。
- 06嘉宾主张科研制度与教育应奖励理解：当前审稿体系超负荷，学生激励在变化，应重视好奇心、批判判断、内在动机和学术共同体。
反方 / 局限
- — 播客中讨论的重大突破仍是讲者的主张，相关论文与代码不在转录的核验范围内，本分析未独立核实。
- — 「已解决公理」只是一个假设性思想实验，嘉宾自己未将其当作对当前 AI 系统能力的描述。
- — 形式正确与人类理解之间的区分虽然被反复强调，但嘉宾并未给出可操作的判据来决定哪些理解是数学工作所必需的。
Lex FridmanSteven BruntonAnkur MoitraAlex（化名数论研究者）Navier–Stokes 方程黎曼猜想唯一博弈猜想LeanMathlib可满足性问题（SAT）概率可检验证明（PCP）计算复杂性理论Lex Fridman 播客
4 分钟 · 6 卡片 · 17 资料
读原文 →