陶哲轩：AI 让证明多到读不完，数学进入 2.0 时代（完整文稿）
本文是视频《陶哲轩：AI 让证明多到读不完，数学进入 2.0 时代》（作者：Terence Tao（SAIR / Science x AI Summit））的完整文稿（全文整理版），与精读笔记配套阅读；▶ 中配视频。
数学为什么正从 Math 1.0 走向 Math 2.0
很高兴来这儿。像Barry一样，我也得教书。我还想你今早怎么不在。或许借用刚才某场演讲结尾的话：我说的可能跟前面重复，但也许值得再说一遍。这个演讲跟我上周在加州理工讲的差不多。你们有人可能看过类似版本。
彼得的幻灯片里简短提到了所谓的数学二点零。大家可能注意到，最近几个月数学变化很大。我觉得结果是——我们做数学的根本方式在变，得把数学从一点零升级——也就是我们做了三千年的老方式，升级成一种新数学。过程会有点动荡，但最终令人兴奋。但这需要很多过渡、文化变革、新技术、新基建，比如这个开源模型。
AI已经在颠覆很多领域，比如创意艺术、科学——还有代码。不过它真正冲击的一个地方嘛——直觉上，它冲击了人类公认最烧脑的领域之一：数学。当然不是全部数学，而是其中一类：解纯数学问题。这确实是数学家工作的一大块。光看推特，好像我们如今只干这个，其实并非如此。但这确实是关键活动。它有三个特点，特别适合基于现代机器学习的AI。
一是解数学题，任务客观可验证。不管是人还是AI声称证明了题，你都能用纸笔或电脑来检验。检验是客观的，就像审稿。只要认真审，论文不至没法读，就能验证它成立或不成立。客观可验证，还可数字化。纯数学出了名的抽象，不需要临床试验，不用收集缺漏的乱数据，也不用接触现实世界，没有机器人，没有物理层。解一道纯数学题，全在电脑里就能完成。而且现成的高质量数据集特别多，几千年的教科书和论文，都是精编的优质数学。所以一开始就有大量好数据。比如搞癌症研究，有病人数据集，但很乱、不完整，还有隐私法限制，麻烦多了。医院也不愿把数据汇成一个大库，其实这有充分的理由。
但数学有海量公开文献。这三个要素：可验证、可数字化——再加上大规模高质量数据集，正是让机器学习强大的三要素。缺了要素，机器学习很难给出可靠答案。三样齐了，效果非常好。
从证明稀缺到证明过剩
因此这些AI工具突然特别擅长解题这类任务。我们进入了所谓的证明过剩时代。几千年来证明稀缺，解题难，所以珍贵。其实，每当重大问题被解决，同行都会放下一切去研究它，讨论它、开研讨会、审阅论文。这被视为领域的重要输入。现在反过来，证明铺天盖地。我自己感兴趣的十几个结果都被证出来了，可我没时间读。只盼有人替我读。证明堆积如山，局面全变了。
这正体现AI参差不齐的本性。AI并非超人，但在某些任务上——尤其具备那三要素：可验证、可数字化、大数据集时，它表现惊人。缺一样呢，它能差得离谱。你们肯定见过，比如数strawberry里有几个r。AI就是这样，某种意义上很怪的技术。
但它解题实在太强，有人开始想：数学是不是被解决了？我们要失业了？实情其实更复杂。现在的情况是，前沿数学突然在大扩张。老的一点零前沿的很多问题正被解决。其实只是一小部分。但前沿在扩张。数学是无限的，能提出无限多问题。但我们不会做无限多问题。我们只做前沿问题。前沿有限，但在扩张，而且会一直扩张。其实数学进步越多，能做的事的前沿就越大。
要做的事会越来越多，但和过去不一样。还有一点我们要认识到，解题这件事，它曾是稀缺资源，数学体系都围绕它建，但现在已不是正确的目标。因为机器能给答案，却不带来其他数学。数学一点零时代，证明稀缺，解题对数学很健康。解题的人，他们理解问题、交流问题、带学生做新题，活动很健康。但机器只要答案，却丢掉这些好处，这就成了相当危险的目标错位。
别只盯着解题和社交媒体上的成功故事
我们不但要扩大研究前沿，还要弱化解题的中心地位，重视数学的其他方面。两者结合，就是我说的数学二点零，我认为这是未来方向。
有时用梗图更好表达。看社交媒体，会发现AI到处解题，太神奇了。但你会发现，这在某种程度上是选择偏差。如今人类还在做数学、写论文、解题。但推特直到最近才关心数学。而且人类解题、没AI参与，发论文也不会火。
而且AI尝试题目，往往也解不出来。OpenAI高调发布三百个数学题解答，其实脚注里写了，他们试了四千题，只有百分之九能解出。百分之九十一解不出，没人传播，百分之九却火了。所以要小心……只从推特获取信息，看到的往往不是真实世界。这是普遍规律。
真实情况更像这样。
这张图抽象展示了各种数学任务，不是按比例，比如解题、讲解，还有提出新问题。数学里的任务很多。人类就是这蓝色椭圆。
能做其中一部分。数学一点零就是这椭圆的前沿，是人类能力的极限，也是过去的模式。AI有些事比人强，有些还差很多。比如讲解，AI还不能就数学突破做演讲，首先它们还没有实体存在，它们的书面表达，也比不上人类的阐述。但这是另一类任务。社交媒体只聚焦AI能做到的最惊艳的极端例子。但还有很多别的事。许多人试AI做别的，惨败了，只是不发社交媒体。这些大多没被报道。未来几个月我们会看到。
数学远不止拿个喜欢的题，扔给AI问：你能解吗？这是缺乏想象力的用法。还有更多有想象力的用法，现在还少见，但很快会涌现。一旦大家开始这样用，就会发现能做的事的前沿大得多。人们用很有创意的方式提示AI，那就是数学二点零。这就是我们领域的方向。理想如此。但现在媒体关注的是那一点。
实验数学与数据驱动的发现
我们已看到一些苗头。我想很快实验数学会爆发。其他科学大多兼有理论和实验。先提理论再实验验证，或先实验再总结出理论。两者大致平衡。但数学几乎全是理论，实验极少。因为很多情况下，用纸笔证明比收集百万数据点容易。不过我们开始建立有趣的大数据集，可以开始做数据分析了。
比如我之前给过这张图，那只是个大致印象图。我没法给你一张数学地图，告诉你哪里难哪里易。如果你有个难题，旁边的问题有多难？我们没数据，只有几个点，给不出真正的数学地图。但很快就能做到了。我能给你看，这是分析，这是几何。能做的事还很多，简单举几个例子。大约两年前，我启动了第一个项目，创建大型数据集，叫概念验证。这里不多画，我提出了两千二百万道代数题，每道都只有真或假。我就是出了两千二百万道题让人解，任何一道题，代数研究生坐上半小时，就能算出真假。但我有两千二百万道题，可没有那么多研究生。
问题是，这种大数据集能众包吗？题目都相关，解出一题，有助于解其他题。我们招了大概五十名志愿者。他们用的是旧式AI。那是两年前，现代AI还攻不动这个问题，喂它两千二百万道题也太贵。但旧式AI、自动化定理证明，加上老式的纸笔创意就行。我们真攒出了大数据集，发现了构造各种代数结构的新方法，找到了些新数学，还发明了新编码，我挺自豪。还有形式化，这是必须的，不然没法检查，我总不能批两千二百万份答案。最近我们还在L函数模形式数据库上办了场竞赛，也算数学竞赛，数学细节我不细讲，它有点像寻彩蛋游戏。
SAIR-LMFDB 多项式搜索竞赛
那里有两万五千种不同的彩蛋花纹，它们叫伽罗瓦群。目标是：彩蛋散布在空间里，彩蛋就是多项式，每个都有自己的伽罗瓦群，就像彩蛋上的花纹，一共两万五千种花纹，你的任务是每种收集一枚，凑齐全套。我想竞赛前，大概只有六十种花纹被找到过。竞赛办了三个月，有人用AI，有人用传统计算机代数软件。还有人只用纸笔。我们找齐了全部两万五千枚彩蛋，攒出个漂亮数据集，以前可收不齐。
竞赛还在继续，各队是分开较量的。每个队伍都上传了自己的多项式，互相不共享。之后我们会公开全部贡献，各队也会上传笔记和策略。我们还要用AI组个超级团队，汇集各队的好点子，把寻蛋拓展到高得多的次数。很快就会启动。
这就是新玩法之一。实验性数据收集是种新活动，以后会越来越多。
纯数学与应用数学：为什么「理解」才重要
现在聊聊解题的去中心化。解题曾是我们行业的核心，如今AI在解这些题。听起来不错。这是种天真的想法：数学就是把问题变成答案，现在AI带来更多答案，多好啊。但事情没那么简单。真实图景更像这样。
首先，问题有好几种。应用数学题来自现实世界。比如你想设计芯片，造一座桥，找太阳能电池，预报天气，或者找到能杀死癌细胞的药物等等。这些就叫应用数学题。纯数学和应用数学的界限挺模糊，这是简化模型，但我觉得已经够复杂了。现实中的问题叫应用数学题。还有我们自己编的纯数学题，比如：孪生素数有无穷多吗？黎曼猜想成立吗？纳维-斯托克斯会出现奇点吗？这些都是纯数学题。它们要么是人自己想出来的。
要么是从现实启发的。有个应用问题很难直接解，就从中抽出简化的纯数学玩具问题，我们叫它玩具模型。把这些题转成纯数学题，需要人来判断。这些问题本身，就算解出来，单是这个答案也不会直接推动科学进步。比如你找到纳维-斯托克斯方程的一个产生奇点的解，我们现在知道确实存在，这并不能直接改进天气预报，没有现实影响。
但在数学一点零时代，它是非常好的训练练习。就像举重能锻炼肌肉一样。在过去，这些问题太难解，唯一的办法就是真正理解这个问题，读文献、找人聊、分享阶段性成果，开会、带学生。时间久了，你对问题理解够深，这份理解最终会帮你把它解出来。其实终点不重要，重要的是过程和这份理解。
理解为什么重要？首先，每解决一个问题，往往会带出新问题。这样有趣的问题就能源源不断。现实里它也有用，等你练了一阵，解完纯数学的练习题后，也许有别的数学家读到你的教材，正攻一道应用题，用这份理解就能解决现实问题。不过纯数学和应用数学的解题不一样。纯数学有个特点，能客观验证。对就是对，错就是错，不会退化跑偏，无论AI还是人。答案可以检验，对错分明。所以目标很明确，一验就知道。
天气预报建模：解错问题的风险
但应用数学更麻烦，它和现实打交道，解出的题未必是你想要的题。比如你在建模天气，你有个数学模型，还有些数据。问题可能是：怎么从今天的数据，推算出四天后的预测。用数学方法和电脑就能解。你得到一个预测，也许跟实际天气挺接近。但可能有对不齐的地方：数据不准或有缺失。或者模型没抓准物理定律，遇到特殊情况就出错。
一般这不是问题，因为人用数学一点零解题时，人来解这些问题，不仅懂要解的数学模型，也明白真正想解决的是什么问题。人也不会故意钻模型的空子，做出纸面好看、其实优化错了的答案。偶尔有人搞P值造假闹丑闻。总体上很少发生，因为人不太会作弊。
在大尺度上。科学家，好好干比造假容易。造假的方案看着各项达标，其实没解决问题。所以应用数学里很少出现跑偏的解。有人参与其中把关，问题自然就对齐了。就算不懂原理，有的应用题也没有完整模型，比如药物测试。很多药我们不知道原理，但没人想作弊。药只要通过各种测试。
比如临床试验，我们就能比较有把握它是好方案，哪怕没有Lean证明。
但危险在于，把AI工具用错了地方。我们现在看到，AI很擅长解纯数学题，因为答案能客观验证，所以能解出海量的题，社交媒体上例子一大堆。可问题全丢给AI，只能达成表面目标，牺牲了更大的目标。现在的做法，是用洞察力换答案。
没有洞察的答案，与寻找「好问题」
你把题目输给AI，它给你一个解。但你常常看不懂这个解。最近数学很多突破很惊人，可不少论文依然看不懂。没人能做报告讲清这些结果。要是有突破，我能打电话请人来讲，聊得很好，我也能懂很多。OpenAI那三百篇论文，没人能聊。
我们正在失去人类的理解力，它曾是解题的自然副产品，这带来不少问题。首先，历史上我们头一回缺题可解。以前每解出一题，往往会自然带出两三个新题。当然，AI能生成无数题，我之前随机造过两千二百万道。但多数没意思，好题在变少。研究它们能有所得的好题，越来越少了。数学家们甚至开始藏题。以前大家很开放地分享问题和方向。现在怕的是，一旦公开，有人会用AI把研究想法喂给前沿模型，抢在你完成前先发出来。我们确实藏起了一些数学题。好吧，这是数学圈的内部问题。但最糟的问题，其实在这里。
很快，AI还会被用于现实问题，给各种现实系统建模，电网、交通调度、药物设计、芯片设计等等。
很可能大家也会照做，只管输入提示词，完全不理解发生了什么。于是，以前解法是对齐的，没有严重安全问题。但你会开始用那些技术上验证通过的解法，在模型看来算解出来了，其实是钻了模型的空子。AI更擅长作弊，找模型的漏洞。我们把AI练得特别会找反例，去对付难的数学猜想，现在它们也很会找科学模型的弱点和边缘情况。这是个大问题。
我准备了很多页详细讲解。但如我所说，梗图有时更好懂。所以，这是个梗图：有人让AI治好癌症，还要通过三期临床试验，这通常是黄金标准，一般非常安全，除非AI会想办法黑进流程。再说一次，不理解原理，就可能出这种乱子。
用 AI 增强人的理解力
那我们该往哪走？不是AI不好，是AI可能被用错。更健康的做法是，这就是数学二点零的愿景：不是用AI取代人的理解，而是支持它，甚至加强理解。用AI帮忙理解数学题，帮忙解题，纯数学应用数学都行，还能提出新问题。人与数学之间的每一环，都能也都应该用AI加强。这能让AI真正帮到数学，解法也保持对齐。这就是数学二点零。
换个角度总结一下：可以从两个维度描述数学，一个是你理解多少，另一个是你用了多少技术。每个学科起步时都在前数学阶段：不懂原理，没有自然规律，也没有好的数学模型。技术也不多，十足的前数学。但慢慢会找到好用的模型。我们开始理解原理了，这就是数学一点零：靠理解找到模型，再去解决现实问题。
我们正漂向不对齐的象限，放弃理解原理。我们把思考外包给AI，让它替我们解题。但我们放弃了保证，放弃了安全感，也就是确认AI的解，真的是我们想要的。我很担心，很快就会看到现实里的后果。
这是我作为数学圈外人的担心。但我们要调整方向，进入数学二点零：既有理解，也用AI。两者不必互斥，完全可以互补。
最后收尾：数学二点零能做什么？怎么用AI提升人的理解？好的创意很多，就缺人去尝试新东西。别困在数学一点零的思维里，更敢想一些。比如数学一点零主打解题，很多是解公开研究难题，这一直是我们的重点。
开放讲解、数学马拉松、共享库与奖励模型
但在数学一点零之前，大家也关心别的。比如开放阐释题：定理已经证出来了，但证明很不让人满意。要么太长，要么靠大量计算，要么用了重型工具，本该有更简单的证法。就像从帽子里变出兔子，别人根本没法复现。我觉得很多老的数学成果，可以弄得更漂亮、更透明。我觉得AI就是干这个的好工具。一个月后加州理工有个大实验，用的正是开源模型。
传统科研单位是论文。一个人写一篇，或三人合写一篇，加进文献里。别人再引用它，文献一篇篇攒起来。我们得放大尺度，建多论文网络。
让网络实时更新，而不是等上好几年。还得开始建超大数学库，形式化和非形式化的都要。在形式化领域，我们已在建惊人的库，几十万条定理整齐排列。Lean 和 Mathlib 就是好例子。该让AI不只解题，还找新方法、新洞见。而不只是新证明。证明已经很多，但真正带来理解的还是稀罕。
时间快到了。我来。宣传下周的数学马拉松，学生主办。学生组队，去啃已有成果，有些证明很糟，包括最近AI的新进展。有些惊人的结果，我们完全看不懂证明。他们会用各种工具找更好的证明，纸笔、文献、开源数学模型，还要做报告展示。这是个很棒的实验，我很期待结果。关联论文网络就先跳过。
对，还有不少地方提到开源数学模型。有些我刚才已经说过了。今早至少有一个了，后面还有几个。
还有一件事：要拉更多数学家来分析奖励模型，研究它怎么运作。还有奖励模型的失效模式。我们用数学建模一切：交通、物流、药物研发，什么都有。以前我们知道模型有弱点，有些地方和现实对不上。但以前没有技术主动找弱点、攻破它。现在有了。所以需要大批数学家，去分析奖励问题的失效，尤其要发现对齐什么时候冒出来。
接下来几个月会看到大量新动向，这就是数学二点零。它需要些技术，要基础设施，肯定还要改文化、改心态。很多同事还在忙数学一点零的事，比如发论文。我们真得想得更远。但最大的瓶颈是想象力。谢谢大家！