菲尔兹奖得主陶哲轩：数学 AI 的瓶颈在证明之后

来源：市场资讯

（来源：图灵人工智能）

转自多是别君词，仅用于学术分享，如有侵权留言删除报道

来源：SAIR（Foundation for Science and AI Research，科学与人工智能研究基金会）
主讲/嘉宾：陶哲轩（Terence Tao），加州大学洛杉矶分校（UCLA）数学系教授、2006 年菲尔兹奖得主、SAIR 联合创始人
主持人：无固定主持人，简短分享后由现场观众自由提问
原视频：https://www.youtube.com/watch?v=PZRb6NIki2w

陶哲轩用交通堵塞比喻当下的数学：马路是十九世纪修给人和马车走的，汽车突然出现，全堵在路上。

他把这个状态叫作证明消化不良（proof indigestion）——AI 生成证明的速度、形式化工具验证证明的速度，都远远超过了人类理解、讲解、发表、教学的速度。这场分享是他在 SAIR 的一次公开发言，现场提问从"怎么让大公司对齐"一直到"用 AI 生成的数据训练下一代 AI 会怎样"。

SAIR 的全称是 Foundation for Science and AI Research（科学与人工智能研究基金会），一年前由陶哲轩参与创立，2026 年 2 月正式对外启动。分享的主题是当时还在筹备中的"开放数学模型计划"（Open Math Model Initiative）：数学界自己造开放权重的模型，而不是只当别人模型的用户和评测题源。计划在 2026 年 9 月 18 日由陶哲轩正式公布——他做这场分享时，话还只能说到"我们希望很快有消息"。

值得读的地方在于他没停在感慨：他把数学的"解题"拆成一条六个环节的流水线，指出 AI 只压中了两环；然后用两场比赛的真实数据，说清开源模型与前沿模型的差距有多大、一张"小抄"怎么补上一大截。

数学的流水线，只有前两环被 AI 提速了

先说这条流水线。一个未解问题被提出；有人找到证明；有人验证它对不对；有人把它写成同行看得懂的讲解；经过同行评审，它被社区接受；最后它被编进教科书，下一代学生用它当常识——陶哲轩把这最后一环叫"正典化"（canonicalization）。

问题本身通常没什么用。他举的对照是：研究癌症找到疗法、研究能源做出更好的太阳能板，这些直接有用；纯数学是好奇心驱动的基础研究，从给小孩做的应用题一直到 Clay 千禧年难题里的 Navier–Stokes 正则性问题，价值不在问题自身，而在它逼出来的东西。他引同行的比喻：未解问题是灯塔，人们并不去灯塔，但灯塔照亮整片地形，让人安全航行。

现在的问题出在流水线的中段和后段。AI 已经极其擅长生成证明，在 Lean 这类形式化证明助手里做验证也相当可靠；可验证之后的环节几乎没有变化。

"我们突然造出一大堆证明，它们甚至被验证是对的，但没人看得懂，没人在发表，也没人讲解，我们没有东西可以给学生看，下一代数学也没有从这里长出来。"

还有一件事被他专门点出来：教科书正是 AI 的燃料。AI 数学之所以强，原因之一是人类花了几百年给线性代数、群论这些基础科目写教科书，这些打磨了几百年的文本成了最有价值的数据集。AI 现在吃的是前几代人攒下的"正典"，而它自己产出的东西，正卡在流水线中段没人接手。

他给的方向不是踩刹车，而是修路。三月他用 AI 生成过一张图：只给马车用的街道，汽车一出现就全堵死。他想要的是为 AI 证明修出高速路和运输走廊，同时保留人行道、公园、无车区，让人还能在里面做数学。

一张小抄，把开源模型从 50% 拉到 80%

第一个例子是他两年前带过的众包项目"等式理论计划"（Equational Theories Project），SAIR 后来把它改造成了"数学蒸馏挑战"的第一阶段。

这个项目造出了一个大约 2200 万条代数命题的数据集，全部是"真/假"判断，绝大部分难度相当于一个代数方向的研究生半小时内能解出来的题——每条都配了 Lean 里的证明或反证。问题在于，人手上不会有 2200 万个研究生。

到了 2026 年 1 月，把其中一条丢给前沿闭源模型，它能做对大约 99%，想五分钟给出答案。换成能在本地跑的开源模型，正确率掉到大约 50%，跟抛硬币差不多。

于是比赛题目就变成了：能不能给开源模型一张"小抄"？规则是提交一段提示词，长度限制约 1 万字符。陶哲轩的类比是，一个期中考试只能考 50 分的学生，给他一张什么样的纸，能把分数提上去。

结果是正确率从 50% 提到 80%–90%，等于涨了 30 到 40 个百分点。那页纸做的事，是把 2200 万条命题里最要紧的特征压缩进一页。他觉得这个范式可以迁移：遇到一个复杂到没人能整体读懂的数据集，蒸馏一张小抄，顺便办一场比赛。

第二阶段已经结束（他坦言还没看到最终分析），要求抬高了一层：不再只要 yes/no，每道题都得给出 Lean 能机器验证的证明，或者一个让前提成立、结论失败的 magma 反例；小抄的规模放宽到约 10 万字节的 Python 文件。比赛允许调用一定量的 LLM，但获胜方案几乎没怎么用——他说，有时候 LLM 并不是答案。

16.6 万个签名，AI 找到了 98.9%

第二个例子是逆 Galois 问题挑战（IGP24），背景是代数里一个经典的未解问题：是否每个有限群都能作为某个数域的 Galois 群出现。

翻译一下：每个整系数多项式都对应一个 Galois 群，它描述多项式根之间的对称结构；再加上一个更细的量叫 signature。陶哲轩的比喻是，多项式像复活节彩蛋，Galois 群像彩蛋壳上的花纹图案。

数字是这样的：24 次多项式对应 25,000 个传递群，算上 signature 一共有 165,836 个目标。竞赛开始时，LMFDB 数学数据库里只有 286 个群、622 个 signature 有具体多项式，不到目标的 0.4%。

第一阶段就是一场"找彩蛋"：参赛者用 AI 或任何手段，为尽可能多的目标找出具体多项式。最后他们找到了 98.9% 的 signature。据 SAIR 与公开报道，到今年 7 月，24 次的情形已被完全解决。

有意思的是冠军。几乎所有人都用了 AI，但甩开其他队伍拿到第一的，是一组几乎不用 AI、只靠传统计算的专家——公开报道里是帕德博恩大学 Klüners 与凯泽斯劳滕 Malle 领衔的团队，他们找出 14.3 万多个多项式，AI 只用来写批量提交的脚本。

第二阶段干脆改成协作：第一阶段所有参赛者公开自己的数据和方法，用一个 AI 整合成一支"超级队"，一边清掉剩下的签名，一边把次数推到 31。这是他熟悉的路子：他的 Polymath 项目就是这么做的——先用竞争拿到有价值的初始结果，再切换成完全公开共享。

能被判分的东西，和重要的东西几乎不相交

提问环节比前半场更直接。

有人问：怎么让只顾往前冲、事后再说抱歉的前沿实验室对齐激励？陶哲轩答，学术界比自己以为的更有软实力。"人们是真心尊重数学和科学的，这是世界上剩下不多的、有客观基础的学科。"那些公司更大、钱更多，但追这些目标，一部分原因正是想借数学的声望——"我们说我们看重这个问题，他解出来了，于是声望归他。那么如果我们重新定义我们看重什么，这本身就已经有很大的力量。"

有人追问：你说 AI 公司应该去比"有用的洞见"而不是"解出题"，具体指什么？

"这些 AI 结果常常是这样：没人给它做报告，甚至没人写论文，也没有同行评审。偶尔有科学家站出来，用自己的志愿时间和精力去解释某个证明，因为他觉得这重要。公司就这样把东西倒出来，是不负责任的。正确很重要，但不是我们唯一在乎的东西。"

他接着给了一句更冷的判断：AI 做不了"洞见"，因为洞见没法自动判分。而能被判分的东西，和我们认为重要的东西几乎是两个不相交的集合。适度优化时两者还能对齐；一旦过度优化，几乎任何能被判分的东西都会变得没用。

新问题从哪来？他答，来自教科书的缺口——写到某一章你会突然发现那里有个洞，那就是个该问的问题；也来自慢工出细活的过程，你正慢慢琢磨一个问题，忽然注意到一个有意思的现象。AI 直奔答案，沿途全错过，"被摧毁的正是这个"。

最后有人拿克隆小鼠说事：多代克隆之后，最后一代小鼠活不下来。现在 AI 生成的数据越来越多，拿它们训练下一代模型会怎样？陶哲轩答，加速的一个后果是产出总量暴涨、平均质量下降，噪声比变差；数据污染以前不是问题，现在是了。现在的 AI 能建在几百年高质量文库上做出惊人的事，但把 AI 生成的内容喂给下一代 AI，出来的是好东西还是退化，没有人知道。"我们不知道会发生什么，却愿意改变一切，这很惊人。"这是高度非线性的系统，数学的教训恰恰是：大多数系统不按"一点点好，所以很多更好"这条直线走，放大十倍百倍之后更是如此。

"我们得慢下来。这个速度快得离谱，而且根本没有必要这么快。"

SAIR 想造一个数学界自己能检查的模型

回到 SAIR 本身。它还在长身体的阶段：赞助活动、做播客、办数学竞赛，接下来打算把竞赛扩到计算机科学，也在设立物理学青年奖。真正的大动作是模型——造开源的数学模型，也希望造开源的科学模型；已经找到能提供算力、能出钱、以及很好的学术伙伴，但当时还不能宣布细节。

他给这个计划的理由是：数学界需要能独立检查、能自己改进、能自己运行的模型，开发应由共同的科学优先事项指导；治理要透明，与产业伙伴合作的前提是不牺牲数学界的研究独立性，共享资源的用途由数学界自己决定。2026 年 9 月 18 日，计划正式对外公布。

他还报了两件事：一个是 SAIR 的第一个计算机科学挑战——Lean 内核优化挑战，目标是让 Lean 更快；另一个是当天刚宣布启动的 Andrews–Curtis 挑战，围绕组合群论里的 Andrews–Curtis 猜想（字幕里读作 "Andrew Curtis"，按 SAIR 官方仓库应为 Andrews–Curtis Challenge）。

他做这场分享的当天上午，刚和二十多位菲尔兹奖得主联署了一份声明《数学领域中人工智能的严重错位》，发布在 mathandai.org 上。声明的判断和分享一致：把解决数学难题当作基准测试来推进，会把数学本来重视的理解、解释、知识积累和学术协作排挤出去。

单词解释

• • 形式证明（formal proof）：用 Lean 这类证明助手写的证明，每一步都由程序检查，不留"显然""易证"这种人类默契。

• • Lean：开源的证明助手兼编程语言，数学命题写成代码，由它的内核判定证明是否成立；本文里的验证、判分都靠它。

• • 定理证明（theorem proving）：把数学命题变成机器可验证证明的过程，这正是流水线上被 AI 提速的第一环。

• • 基准测试（benchmark）：一套固定题目加判分规则，用来横向比较模型；把数学难题当基准刷分，正是那份联署声明的矛头所指。

• • 开放权重模型（open-weight model）：参数公开、可下载、能在自己机器上跑的模型，对应只能通过 API 调用的闭源模型。

• • 证明消化不良（proof indigestion）：陶哲轩的说法：证明产量暴涨，而人类理解、讲解、发表、教学的速度没变，于是全堵在路上。

• • Galois 群与 signature（Galois group / signature）：Galois 群描述多项式根之间的对称结构；signature 记录实数根个数的信息，比群更细一层。

• • 蒸馏（distillation）：把庞大数据集或大模型的能力压缩进很短的提示词或小模型；文中的"小抄"就是一页提示词蒸馏。

对做数学 AI、做形式化验证、做科学模型的人来说，这场分享的落点在评测和数据两件事上。如果目标函数只奖励能被自动判分的结果，你优化出来的东西会越来越像考试，越来越不像数学；反过来，谁能让"理解、讲解、正典化"这些环节变得可规模化，谁就补上了这条流水线上唯一还空着的部分。

开放权重模型之所以被反复强调，是因为它至少满足最基础的一条：任何人都能下载下来、自己跑、自己检查。数学的问题不需要下周解决，这不是一场世界危机——这是他敢慢下来的底气。