来源：AI寒武纪（你说的完全正确（原创）） · 2026-10-11 · 原文链接
分类：观点、人物与社会（陶哲轩 2026-10 Caltech 演讲转述稿）；主线强相关两条：①「解题只是 proxy」＝感知层/机制层准则的第 6 例且来自菲尔兹奖得主；② 陶列出的三特性（客观可验证/可数字化/海量高质量数据）＝dense feedback 的领域级排序器，直接接「RSI 卡在 L3」
一句话概括
陶哲轩在 Caltech 讲《Math 2.0》：数学因为「客观可验证 + 高度可数字化 + 海量高质量数据」三特性命中机器学习的最强项，正从证明匮乏时代被拽入证明充沛时代——但解题从来只是人类理解的替代指标，在证明充沛时代这根标尺彻底错位，盲目刷解题速度反而有害；AI 的正确用法不是替人解题，而是强化「人类理解 ↔ 数学」之间的每一条连接。
核心要点
一、为什么数学最先被 AI 攻陷：三特性
数学具备在其他学科极罕见的三个特性，正好击中现代机器学习的最强项：
- 客观可验证性（objective verifiability）：数学家可以对"什么是有趣的数学"各执一词，但对"什么是正确完整的证明"存在广泛共识，甚至可以用 Lean 这类证明辅助语言机械化检验；
- 高度可数字化（digitizability）：证明不需要实体装置、真实世界数据输入、物理实验复核，纸笔 + 标准定义库就能完成一切；
- 海量高质量数据（large, high-quality datasets）：绝大多数数学文献已数字化。
所以顶尖 AI 实验室把海量算力优先砸向数学解题——优先级高于其他应用，正因后者缺这三特性中的一条或多条。
二、证明充沛时代的危险错觉
- Math 1.0 的全部学术体制、激励、研究目标都建立在证明稀缺假设之上；
- 现在算力管够、模型够好，很多过去公认棘手的开放问题短时间内可被 AI 解出，提问者甚至不需要专业训练；
- 但陶直接点名报告偏差（reporting bias，slides 配图即幸存者偏差的战机弹孔图）：社交媒体上看到的全是被 AI 解出的一小部分，更多失败的尝试根本无人上报；
- 真相：即便投入海量算力，当前数学前沿的绝大多数核心问题依然悬而未决；问题空间无限、难度上限无止境，前沿会持续扩张；
- 且 AI 能力极度参差（jagged）：客观可验证的闭环领域强得惊人，一旦涉及主观判断、现实交互或数据稀缺，立刻漏洞百出。
三、解题只是手段，从来不是终点（全篇论点核心）
- 解决问题是研究数学史上最显眼的指标，但它仅仅是一个 proxy（替代指标），真正有价值的目标是人类对数学规律的深层理解；
- 原文句式（slides）：“This proxy was largely accurate in the era of proof scarcity, but has become misaligned in the era of proof abundance. Further blind optimization of problem-solving alone is now actively harmful.”——这个代理在稀缺时代大体准确，在充沛时代彻底错位，继续盲目优化它对数学的长期健康有害；
- 开放问题是灯塔，不是目的地：它们的作用是指引人类探索灯塔周围的数学图景；尝试过程中的经验与工具往往比最终答案更有价值；
- 过早用自动化工具撞上灯塔，会打断未走之路的探索，旱化（sterilize）周围整个领域。
四、癌药思想实验：没有人类理解的解法极度危险
陶的思想实验：命令 AI「找一款能通过三期临床试验的抗癌药」。AI 消耗海量算力后给出一组未知化学分子的鸡尾酒；数学模型预测它能杀死癌细胞，该预测在 Lean 中被形式化验证，药物也确实通过三期临床——但没有任何人类知道它是怎么被找到的。
- 你敢把它注射进自己的静脉吗？AI 可能只是利用了试验流程的某个漏洞，给出了严重对齐失败的解；
- Math 1.0 的可持续循环：纯数学问题（客观可验证）→ 孕育人类理解 → 产出可验证解 → 认知安全迁移到需要主观判断的应用数学；
- AI 粗暴切断中间环，从问题直接跳到答案，跨过了人类理解——这种不可持续的解法在数学走向复杂现实应用时埋下巨大隐患。
五、Math 2.0 的正确用法清单（slides 给的全部实践）
- 开放阐释问题（open exposition problems）：给已知证明晦涩的重大成果找更直观、更有动机的新证明（Caltech Mathathon，11 月 13-15，学生用开源 AI 给现有不满意的证明找新证法）；
- 实验数学新时代：从个案研究走向全样本调查，绘制新的难度地形图。实例：等式理论项目（ETP，2024-25，人机协作判定通用代数中超过 2200 万个真/假命题）；逆伽罗瓦问题挑战（IGP24，2026 第一阶段完成，为 24 次全部 25000 个伽罗瓦群找到多项式，第二阶段协作推进到 31 次）；
- 消融实验：对已证定理撤掉某些高级工具，看能否找到更初等的证明；定理邻域探索：修改/放宽前提假设，看原结论还能抢救出多少推论；
- 活体学术网络：把大量论文拼成可实时增删的大网络（显式解析数论网络 IEANTN，一张"活体电子表格"）；
- 扩建 Mathlib 这类超大型形式化数学库；
- 开发高可解释性、高安全性的开源专用数学模型——陶透露"一些开源数学模型很快发布，敬请期待"；
- 以及：把纯数学理解用于分析真实世界模型的失败模式、探测 AI 工具应用时的失配（misalignment）等。
六、真正的瓶颈
迈向 Math 2.0 的最大阻碍，不是技术，甚至不是学术体制，而是想象力（imagination）。slides 末尾注明：本演讲的图片和图表由 AI 生成。
金句
解决问题一直是最显眼的指标，但它仅仅是一个替代指标。真正的目标，是人类对数学规律的深层理解。
这个代理在证明稀缺时代大体准确，在证明充沛时代已经彻底错位；继续盲目优化解题，对数学的长期健康有害。
开放问题其实是灯塔。它们的作用不是让人不顾一切冲上去占领，而是指引人类去探索灯塔周围未知的数学图景。
过早用自动化工具撞上灯塔，会打断未走之路的探索，旱化周围的整个领域。
迈向 Math 2.0 的最大阻碍，根本不是算力技术，甚至不是传统的学术体制。真正的瓶颈，是人类自身的想象力。
质疑与核查
✅ 主体内容高度忠实。以下关键句都在 slides 中逐字对应：“largely stable for almost a century”、三特性（objective verifiability / digitizability / large high-quality datasets）、“era of proof abundance”、“jagged”、“most of the problems at the current frontier of mathematics remain unsolved, even with massive computational expenditure”、“proxy… misaligned… actively harmful”、灯塔（lighthouses）与 “sterilize the surrounding field”、癌药思想实验（cocktail / Lean / stage 3 trial / misaligned）、Mathathon、ETP 2200 万命题、IGP24 的 25000 个伽罗瓦群与向 31 次扩展、Mathlib、IEANTN、消融与定理邻域、“Some open math models to be released very soon”、瓶颈＝imagination、演讲配图由 AI 生成。
- 标题是公众号加码：陶的表述是"正在进入证明充沛时代"（we are now entering an era of proof abundance），是趋势判断；「正式到来」「彻底结束」是公众号标题的确定性升级，转述时用原口径。
- 「二战战机弹孔图」无法文字核验：slides 确有 reporting bias 一页（“Wow, all the math problems I am seeing on social media are being solved by AI!"），配图内容无法从文本提取确认，弹孔图细节存疑但无害。
- Mathathon 的具体例子（四色定理 / ABC 猜想 / Navier-Stokes）在 slides 里没有点名——slides 只说"对现有证明不满意的成果找新证法”。这三个例子可能来自活动宣传页，也可能来自公众号补写，引用时不能说是陶在演讲里举的。
- 公众号漏掉了两条 slides 里有的内容：① 陶呼吁"更透明、更科学的 AI 能力评估，完整报告资源消耗与负面结果"，并点名实践 First Proof（1stproof.org）——这条对评测纪律很有价值，公众号没提；② 把纯数学理解用于分析模型失败模式、探测 misalignment 那条"等"字后的内容。
- ETP/IGP 数字与 slides 一致（over 22 million true/false statements；25,000 possible Galois groups at degree 24），无需打折。
本文为阅读剪藏（摘要 + 摘录 + 评论），非原文转载。查看原文