陶哲轩：SAIR 开放数学模型与证明消化不良

原始视频：Terence Tao: SAIR’s Open Math Model Initiative

SAIR · 2026-09-18 · 25 分 15 秒

演讲：陶哲轩（Terence Tao），加州大学洛杉矶分校数学教授、菲尔兹奖得主、SAIR 联合创始人

补充一手资料：25 位菲尔兹奖得主联合宣言 · SAIR 开放数学模型主页

2026-09-11，由 SAIR、加州理工学院与默金纯粹与应用数学中心联合举办的 Science x AI 峰会在加州理工学院开幕。陶哲轩在峰会上发表开幕主题演讲。本文依据完整英文演讲与官方字幕整理。

加州理工学院的演讲台上，陶哲轩坦言自己度过了人生中最离奇的一周。就在当天上午，他和 24 位菲尔兹奖同行共同发布了一份联合宣言，呼吁关注人工智能在数学领域的严重价值错位。

前沿实验室正在以前所未有的速度生成数学答案，但整个数学界却陷入了一种前所未见的堵车状态。AI 能够高效生成形式化证明，却无法替代人类消化、解释与传承知识的过程。

解题只是起点：数学认知的完整链条

纯数学属于好奇心驱动的基础研究，许多著名猜想更像航行中的灯塔。水手不会把灯塔当作居住目的地，但灯塔照亮了周边的航道与礁石，让后人看清整个数学地貌。

一个开放问题的解决，需要经历漫长而完整的认知链条。研究者提出解法只是第一步，初版手稿往往充满杂乱步骤，需要同行核验确认正确性。

接下来是阐释与重写。糟糕的原始证明必须被改写得清晰易读，让更多专业同行理解其中的核心洞察。

论文经过同行评审与正式发表，获得学术共同体的接纳。这个阶段鲜有聚光灯，学术界常为解题者颁发奖章，却很少给默默审稿的研究者发奖，但审稿机制维系着整个学术共同体的信任基石。

整个链条的终点是典范化。零散的论文被梳理融汇，最终写入教科书，下一代学生才能站在巨人的肩膀上理解知识之间的脉络关联。当今大语言模型之所以能够处理代数与群论，基础正是人类数百年沉淀下来的教科书体系。

“证明消化不良”：机器刷题与理解断层

当前的结构失衡在于，AI 在解题生成与 Lean 形式化验证这两个环节展现出极高效率，但链条后半段的阐释、发表与教材沉淀几乎毫无改观。

这种上下游的严重脱节导致了陶哲轩所说的“证明消化不良”。大量机器生成的定理即便被 Lean 判定为无误，连按下回车键的研究员自己也解释不清机器究竟发现了什么。

陶哲轩用交通演变打了个比方：二十世纪初街道原本为行人和马车设计，汽车突然涌入街道造成全城拥堵。理想的状态应该包含两条平行轨道：一边是供 AI 进行大规模高通量计算的高速公路，另一边是供人类漫步思考、讨论灵感的步行街与公园。

眼下的现实却更像重型推土机横冲直撞。前沿实验室热衷于宣布攻克重大猜想，但这些堆积如山的符号序列往往难以转化为人类可吸收的真实理解。数学基础研究并不急于下周交卷，这种粗暴压缩时间的方式正在稀释数学的核心价值。

25 位菲尔兹奖得主发声：过度优化可评分指标导致错位

演讲当天发布的 mathandai.org 宣言，汇集了包括陶哲轩在内的 25 位菲尔兹奖得主签名。宣言直指商业实验室对单一可评分指标的盲目追逐。

前沿机构倾向于优化容易打分的事情。形式化验证能够给出一个明确的是非对错标签，但数学最看重的解释、概念洞见与启发性教学却难以被简单量化。

只要优化强度适度，打分指标与实际价值尚能维持一致。一旦进入极端过度优化阶段，能够被打分的指标与真正有价值的科学洞察几乎彻底脱节。

学术共同体拥有比自身预期更强大的软权力。商业公司之所以热衷于攻克数学经典猜想，是因为它们急需借用数学殿堂的严密声誉为模型背书。只要学者们坚持捍卫数学真正的价值标准，就能促使行业重新校准研发方向。

SAIR 启动开放数学模型计划

一年前，陶哲轩与 Chuck 共同创立了非营利机构 SAIR。面对前沿闭源模型的垄断，SAIR 正在筹备联合学界与开源社区打造一套开放数学模型。

这套开放模型旨在让研究者能够自由检查权重、本地运行、改进算法并用于日常教学。SAIR 正在联合提供算力、资金支持以及学术机构的各方伙伴，建立负责任的科学 AI 范式。

闭源商业模型将数学探索封装成黑盒服务，研究者无法审计其内部推理逻辑，更无法将其深度融入长期的数学人才培养。

开放数学模型的目标是为数学家提供一把趁手透明的数字标尺。研究者不仅能看到运算结果，还能追踪推理路径，让机器成为辅助思考的脚手架。

蒸馏挑战：10KB 提示词让开源模型准确率提高 30% 到 40%

在筹备大模型的同时，SAIR 举办了一系列探索人机协作边界的数学挑战赛。第一项挑战是基于等式理论项目衍生出的蒸馏挑战。

该项目基于 Lean 形式化语言构建了 22,000,000 道代数是非题，难度通常需要一名研究生花费 30 分钟推导。商业前沿模型在经过 5 分钟思考后能达到 99% 的准确率，而能在本地独立运行的开源基础模型准确率仅有 50%，与掷硬币无异。

第一阶段比赛要求参赛者提交一份不超过 10KB 的提示词，相当于给参加期中考试的学生提供一张单页参考备忘录。比赛结果显示，优质提示词让开源模型的准确率提高了 30% 到 40%，整体表现跃升至 80% 到 90%。

刚刚结束的第二阶段将限制放宽至 100KB 的 Python 脚本，目标是直接生成 Lean 形式化证明代码。赛后分析出现了一个耐人寻味的结果：表现最优的获奖队伍在执行过程中几乎没有调用大语言模型，证明算法设计在很多时候远比堆叠模型更有效。

反伽罗瓦挑战：从竞技猎蛋到协作超级战队

另一项具有代表性的是反伽罗瓦挑战。针对 24 次多项式，理论上存在约 165,000 种可能的伽罗瓦群特征签名，此前人类数学界仅找到了约 600 种，覆盖率不足 0.3%。

挑战赛第一阶段采用类似彩蛋猎寻的竞赛模式，号召全球研究者寻找匹配多项式。参赛者在短时间内找出了 98.9% 的签名，几乎扫平了绝大部分盲区。

令人深思的是，第一阶段以绝对优势登顶的冠军团队由 2 位人类专家组成。他们采用传统代数计算方法，全程几乎没有使用任何 AI 工具。

第二阶段将转入完全公开透明的协作模式。所有第一阶段选手将思路与代码汇集到同一个交流频道，由 AI 统筹吸收各家所长组建超级战队，共同攻克最后 1.1% 的冷门签名，并向 31 次更高阶多项式发起冲击。

数据污染与非线性反噬：数学并不急于下周交卷

面对听众关于模型用合成数据反复自训练的提问，陶哲轩表达了对数据污染的警惕。正如生物学中克隆小鼠经历多代克隆后无法存活，AI 数据闭环面临类似的退化风险。

当前 AI 之所以展现出惊人能力，是因为它踩在人类数百年积累的高质量经典理论之上。倘若未经消化吸收的机器废料充斥网络并被反哺给下一代模型，输出的平均信噪比势必急剧恶化。

数学规律深刻表明，现实世界大多是非线性系统，简单假设把计算规模扩大 10 倍或 100 倍就能获得线性收益往往会遭遇反噬。

面对技术浪潮，科研人员需要主动掌握节奏。盲目加速与机械刷题无法催生真正的数学洞察，唯有重拾严谨的阐释、对话与批判性思考，才能守护科学知识的纯粹底色。