来源：市场资讯
（来源：图灵人工智能）
您想知道的人工智能干货，第一时间送达
孔某人推荐序：
能看到本文的读者应该众所周知：纯数学是目前LLM攻坚的主要方向之一，在进步速度上没有比Coding慢。
那么在有如此强工具的介入下，现在的数学学界到底怎么样了呢？数学进展飞速了么？而这就是本文回答的问题。
实际上数学进展并没有飞速，而这过程中让大家重新认识了我们为什么需要数学证明，除了能够证明之外我们还需要什么。
从本文可以窥见其他理论领域未来面对的问题，以及对于其他领域应该也有很多参考意义。
title: Terence Tao: New mathematical workflows | Future of Mathematicsurl: https://www.youtube.com/watch?v=Uc2zt198U_Udate: 20260513
文字凝练版
00:00:04
Jared:
我们非常荣幸邀请到Terence Tao作为主讲嘉宾。他是UCLA数学教授，也是IPAM（Institute for Pure and Applied Mathematics）的特别项目主任。
Terry告诉我，几个月前IPAM举办了一场类似主题的会议，这些话题已经在不断涌现。实际上早在2021年的IPAM会议上，他就观察到许多趋势正在汇聚，并为数学界敲响了警钟——我们现在开始看到的进展，以及未来一年可能发生的变化，他很早就在关注了。
Terry在2006年获得了Fields奖，研究涵盖数论、组合学、偏微分方程和分析学。但今天，他将和我们讨论未来几年我们可能需要思考的新数学工作流程。
00:01:26
Terence Tao:
我的演讲会着眼于比其他许多报告更宏观的层面。目前AI辅助数学的前沿水平大约处于解决单个问题的级别——选一个开放猜想，可能写出一篇论文。但数学不仅仅是一堆互不相关的定理和论文的集合，它上面有一整个系统。我认为我们必须开始思考这个更大的系统，甚至可能需要降低问题层面优化的优先级，因为它正开始与系统层面的优化相冲突。
数学作为一个整体，几百年来没有太大变化。如果你回到100年前、200年前的数学会议，也许语言是德语或法语，没有PowerPoint或Beamer，但做数学的方式基本没变。而其他科学在近几十年已经发生了变革——甚至在AI之前就有其他革命。
在其他科学中，大规模协作变得越来越常见。现在多作者论文中不只是两三个合著者，而是10个、50个，这种情况正变得普遍。从图表中可以看到，数学几十年来基本保持在一两个合著者的水平。
另一个变革是数据爆炸。许多科学领域曾处于数据稀缺时代，获取数据很困难。但现在它们进入了数据丰富时代，被数据淹没——也许不是无限数据，但能获取大量数据。基因测序就是一个很好的例子。
我认为在数学中，我们正在进入一个类似的时代。几千年来，我们一直处于"证明稀缺"时代——证明很难找到。现在我们正进入"证明丰富"时代：并非一切都能被证明，但生成证明的能力已经开始远远超过数学其他环节的处理速度。我们必须适应这一点。
传统上，数学工作方式是这样的：少数人一起合作，通常在黑板前。我们仍然经常面对面交流，虽然也能通过Zoom和邮件做一些事情，但主要还是当面。我们仍然使用纸和笔。我们需要每个人都是专家——博士水平的数学家。每个人都审查彼此的工作。
正因如此，我们需要合作者之间的高度信任。特别是因为证明的可靠性取决于最弱的环节——如果有一个不可靠的合作者搞砸了某个关键步骤，而没有其他人审查，整个证明就会崩溃。其他科学有更多鲁棒性，比如一个数据点偏差一点不是大问题。但在纯数学中，我们的论证结构不具备那种鲁棒性。应用数学嘛，某些类型的东西可以容忍一些数值误差。
00:05:31
还有一个我们以前不需要做、但现在变得极为重要的区分——项目有两类目标。
显式目标是我们明确说出来想要的：证明这个定理、解决这个猜想、回答这个问题。但实际上还有许多隐式目标附着于显式目标之上，我们以前不需要专门说明，因为解决显式目标的人类往往自动地也完成了这些隐式目标。但AI不一定会这样做，这正在成为一个重要问题。
比如你和合作者说"我想证明这个猜想"，这是显式目标。但在过程中，你同时还在实现各种隐式目标：弄清楚你的证明如何与过去文献关联；自然的后续问题是什么；正在发展什么新技术，它们对其他问题有多大用处；关键困难是什么，如果有多种技术，哪种技术在解决哪个困难；故事是什么，叙事是什么——即高层概览。最后同样重要的是，研究项目的一个主要隐式目标是训练作者自身变得更擅长解题，而且不仅是作者，读论文的人也应该从中提升能力。你不只是想让人看到有个了不起的证明但他们自己无法复现，你还想要训练他们。
这些隐式目标以前不需要明确提出来，因为人类在解题过程中自然会记录困难点在哪里，如果使用了过去文献就会引用它，并且会从项目的成功和失败中学习。
但现在有一个危险，我认为已经开始出现了：AI工具可能会将这些目标彼此解耦。我们开始看到一些AI解决方案，技术上确实解决了显式目标——它们解决了问题——但你看那个解答，它们并没有满足我们期望人类生成的解答所应达到的隐式目标。
也许它们会生成一个猜想的证明，甚至在Lean或其他可靠验证机制中通过了验证，但它们不会引用影响来源——它们会使用论文中的想法但不引用该论文。我们经常发现，这些证明虽然验证正确，但花了大量时间在相当常规的步骤上，而那些新颖且有趣、真正应该被突出的部分，往往只是被塞在论文的某个小节里。它们不一定能提出什么是关键新想法、可以研究什么新问题的洞见，也不会训练任何人类变得更擅长这类任务。
这是当前AI的情况。其中一些缺陷可以通过更好的prompt来改善，但这不是我们以前需要关注的事情。很多解题尝试，人们只是高兴得到了答案，再加上一个Lean验证的勾作为奖励，然后就结束了——"好了，其他任务留给别人去收拾吧。"
但我们即将进入一个时代：会有一个人们关心的问题，有一个AI给出的解答，但没有人能就此作报告——没有任何一个人类能理解这个证明到足以做报告并回答问题的程度。也许你可以说让AI来做报告，但我认为这会是一个非常不令人满意的局面：一个问题被解决了，但整个领域并没有进步，因为我们无法使用这个证明。
00:10:16
传统上我们有同行评审。我不会点名，但确实存在一些人类写的论文解决了问题，却没有很好地解释关键想法或训练下一代。但我们把它们送给审稿人，审稿人可以在一定程度上指出这些问题并部分纠正。随着时间推移，会有后续论文、也许有教材和其他阐释，有一个我称之为"proof digestion"（证明消化）的过程——证明被简化，主要想法被提取，最终可以在某个研究生课上讲授。
但AI生成论文的数量已经使得人类审稿人基本无法处理所有这些任务了，除了最重要的结果之外。所以我们必须转向自动化方法。
形式化证明验证至少可以排除错误的证明，但正确只是我们想要的隐式目标之一。我们还希望证明是可理解的，希望它能指向进一步的方向。形式验证至少免除了审稿人逐行检查正确性的职责——也许这部分可以外包给Lean之类的工具。但即便审稿人只需评估重要性和与文献的联系，数量仍然太大。
那么可以用其他AI评审来评估论文的趣味性、引用是否完整。这可能会有帮助，但并非万无一失。特别是reward hacking是一个非常严重的问题，你不能将其作为主要防线，只能作为额外的过滤器。
我最近一直在用的类比是：AI技术就像汽车的发明。我们现在有了速度快得多的交通工具，但我们的基础设施——期刊、课程、教材、培训学生的方式、审稿系统——来自19世纪，是汽车出现之前的街道。你可以造出更快、更高效、载客更多的车，但交通不仅不会改善，反而会恶化。整个传输网络的容量可能因为你不断改进汽车技术而实际下降。
优化单个人从A到B的原子交通问题，并不能优化整个人口如何尽可能高效地满足交通需求的全局问题。
所以我们需要新的基础设施——设计一个能容纳自动化证明器等新技术的整体数学系统。但你同时也需要"步行道"。汽车很好，但你不会希望它们无处不在——这个房间里就没有汽车，这是有道理的。你需要明确划分：数学的哪些部分允许无限制的AI输入，哪些部分允许部分AI输入——也许是"滑板车"级别的，哪些部分是纯人类的。
在我们建立这样的基础设施之前，拥有更好更快的AI、产出更多证明，超过某个点之后就不再有帮助了。这是我们现在必须面对的问题。我们必须超越传统工作流程——少数人在一起花几个月解决一个问题、消化它、发表它的模式。
00:15:04
还有什么其他工作流程呢？比如Polymath项目，来自21世纪初的"远古时代"——前现代AI时期。我们通过大规模协作解决了一些问题——按数学标准的"大规模"，也就是12到20个人在线协作。
大约有15个这样的项目，主要通过博客和wiki运作，典型的2000年代互联网工具。它们能解决一些开放问题，但更典型的做法是拿一个已有证明来优化——比如改进某些界，或者丰富它与其他领域的联系。
这些项目不擅长深度——不像某个数学家在阁楼里闷头工作七年那种挖掘全新洞见。但它们擅长的是广度。因为项目是开放的，你能让来自数学各个领域的几十位专家进来评论。相比传统的三人合作——你只能获取那三个人的专业知识加上文献检索——Polymath项目中，当有人说"我这里需要一个优化理论的引理"，很可能就有人跳出来说"我认得这个，这跟某某有联系"。
现代AI与此有相似之处——AI也擅长广度，它们是在整个互联网上训练的，这是它们的超能力之一。
这些Polymath项目还有一个有趣的演化模式：开始是混沌阶段，几百人评论，尝试各种不同方向。然后大多数方向被修剪掉，某一条路径显得有前景，但几百人中可能只有五六人对追踪这条路径感兴趣。于是就像量子波函数坍缩一样，Polymath项目坍缩成三四个人的传统协作，之后要么转到线下，要么继续在线但本质上就是普通合作了。Polymath项目的价值在于识别出正确的方法，并集结出正确的合作者组合。
另外一个不太被认识到但我收到很多反馈的价值是：这些项目足够开放，研究生和刚学数学的人能真正看到问题解决的实际过程。你看论文或听报告，通常都是非常光鲜的成功故事——不会展示死胡同、失败的尝试、以及如何修复问题。但因为Polymath的一切都是公开进行的，大家能看到这些，这是另一个重要价值。
00:18:54
然而，这些项目最终衰退了是有原因的——它们不可扩展。要运行这样的项目，基本上得有人处理涌入的几百条评论，进行审核，温和地劝说那些方向不对的人别再继续推进死路，同时鼓励有前途的方向，还得检查所有贡献。这是在Lean和AI出现之前，一切都是手动完成的，所以基本上得有人把这当全职工作。
而且2000年代初的技术——博客和wiki——也没有GitHub、Overleaf这些工具，连基本的版本控制都没有。所有沟通都是通过文本评论来回传递，而不是用一个GitHub仓库或其他现代工具。这些问题有些可以用现代技术解决，但Polymath项目整体而言，它的时代已经过去了。
举一个最著名的例子——Polymath 8。张益唐证明了素数之间存在有界间距——可以找到无穷多对相差有界的素数。他的计算给出的界是7000万，但他在论文中也指出7000万没什么特别的，这只是他的证明给出的结果，他没有花功夫去优化。但一旦这个结果公布出来，优化它就成了一个非常诱人的目标。
起初是个人作者各自尝试——"我能到6000万"、"我能到5000万"。然后我们把它众包起来，大约一年后，界被降到了246。这是一个成功的众包项目案例，跟传统研究项目很不同。
它之所以成功，有几个关键因素。第一，有明确的目标和清晰的度量标准——这一点对AI领域的人可能很有共鸣，有了度量标准就容易优化、容易做基准测试、可以有排行榜来追踪进展。
第二，它是模块化的，张益唐的证明有若干独立组件，优化其中一个组件的界就能自动改善最终结果，所以可以去中心化，不同小组独立处理不同部分，参与者不需要理解整个项目。
第三，允许部分进展。把7000万改进到300万但没到200万，这仍然有价值。不像很多定理证明——要么证出来要么没有。
第四，可尝试的空间极大，有很多构造方法和变体，一两个人可能无法识别所有可能的优化方向，所以适合众包。
这里展示的就是当时的排行榜——至少是第一页——可以看到界在这一列随时间稳步下降，有些大的突破性跳跃，还有各种组件数字以复杂方式汇入这个总数。但这一切也是手工完成的，这是一个由人类维护者维护的wiki，不是自动生成的。
Polymath项目已经过时了，但它有现代版本——形式化项目。这类项目有非常相似的模块化结构：你要形式化一个大定理，就把它拆成小块，人们可以认领单个部分来形式化。现在我们有了GitHub、Lean和持续集成，验证部分至少可以自动化。项目可以去中心化，不同人认领不同的任务簇，通过论坛进行松散协调。
我们使用现代项目管理方法——有可分配的任务，比起当年只靠博客评论、由人手动追踪谁在做什么，组织化程度高了很多。论坛讨论也更加结构化，可以搜索。
我们正在开始将AI用于这类项目的小型组件。把大定理拆分成很多引理后，有人可以认领一个引理，手动形式化或者交给AI。有时候AI会报告某个结果无法证明，因为存在反例——而这实际上是因为语句的形式化有误。这时你就得回到社区讨论如何修复，可能需要修改其他地方的定义。所以目前还无法完全自动化，有些问题仍需要人类介入，但论坛讨论的形式很适合处理这类协调问题。
00:24:59
不过我们目前面临的挑战是，技术已经超越了基础设施。现在AI不仅能形式化单个定理或引理，还能处理整篇论文——把论文喂给一个自主Agent，它会自己尝试分解和形式化。但我们发现，即使它在技术上成功了，要把结果整合进一个现有的形式化项目仍然很困难。
问题有几方面：项目可能有自己的分解方式，而Agent用了不同的分解方式；风格可能不同；它们可能反复证明类似的语句，而实际上应该提取一个统一的抽象引理调用多次。当前的形式化AI工具没有遵循最佳形式化实践——它们主要被训练来让代码正确编译，这当然是基本条件，但形式化还有其他隐性目标，我们还没有在这些方面正确训练AI。
另一个问题是，现有基础设施——聊天论坛、GitHub这些——都是为人类优化的。AI在形式化过程中遇到问题时，它不会跑到Zulip上发帖提问，等人类回复，然后去修复。也许将来会有AI机器人出现在这些论坛里，但目前人类的协作工作流和AI的自主工作流几乎是不相交的。它们只能在微观层面被粘合：一个人认领一个子任务，私下与AI协作完成，然后回来跟团队沟通。所以整合仍然是一个持续的挑战。
我们可能需要做的是区分两类形式化任务。一种唯一目标就是验证某个定理为真——不关心证明有多丑、代码是否可复用、是否优雅可读，唯一要的就是那个验证勾号。这类任务现在有个流行说法叫"merely true"——我们只知道它被证明了，仅此而已。对于这类没有其他隐性目标的任务，当前AI工具是够用的，你可以直接把它扔给任何LLM。
但还有一类多目标形式化项目，除了形式化本身，你还希望代码优雅、可读、可复用、能和其他代码集成——有很多隐性目标。对于这类项目，在现阶段我们无法让AI超越一定程度，AI必须被限制在解决极度明确的子任务上，人类必须负责编排。也许将来会改变，但目前我们必须做出这种区分。
00:28:45
即便你做了这种区分——把行人区与高速公路分开——仍然会产生一个激励差距的问题。假设有一个你想证明的重大结果，比如有限单群分类定理，你希望得到一个形式化证明。现在假设有一个大规模的自动形式化工程，把所有相关论文都消化了，输出一个百万行的代码仓库，在Lean中证明了有限单群分类定理——但完全是意大利面代码式的证明，没有任何解释说明各部分如何组合在一起，你唯一学到的就是"分类定理是对的"。
这在某种意义上比没有好，但问题来了：如果你还想要一个规范化的形式证明——结构清晰、模块化、识别出关键步骤、整合了文献中的简化证明——突然间激励就消失了。因为我们整个数学社会系统奖励的是"第一个做某事的人"。你不再是第一个形式化这个项目的人了，你能招募到的志愿者会少得多，因为别人会问："为什么还要做这个？已经做过了。"
这里存在一个悖论：在显式目标上做得更好，可能实际上对更广泛的目标有害。人们不愿做剩余的工作，因为生成激励的显式目标已经达成了。即使有人确实开始做规范的形式化，也存在很大的诱惑去直接从混乱的形式化中抓取代码片段，而不像自己手工编写时那样花精力打磨。
这种速度与质量之间的权衡正变得越来越紧迫。我们在形式化项目中看到了这一点，也在问题求解中看到了——虽然问题求解不是数学家做的唯一事情，但确实是核心组成部分之一。
一个正在实时上演这种动态的实验场是Erdős问题数据库。这是一个问题集合，首先，这些问题所在的数学领域似乎因某种原因特别适合AI方法；其次，它有足够大的问题集且难度梯度多样，你可以清楚地看到进展随时间推移在改善。最重要的是，它有一个网站和论坛，论坛有明确的AI政策，欢迎某些类型的AI贡献。
这一点很重要。其他问题论坛，比如MathOverflow，AI政策限制严格得多，基本是"仅限行人"的区域，AI使用非常有限。因此你在那些网站上看不到多少AI贡献。但另一方面，它们也没有经历Erdős网站正在经历的"交通拥堵"问题。所以这是一个权衡。
00:32:53
Erdős问题大约有一千个。去年9月时，大约380个已被解决，主要来自已有文献。后来陆续有文献中找到的解答、人类的新证明，以及越来越多的AI贡献。
2026年初有一段混乱的爆发期——大约50个问题被通过各种方式解决，有的大量使用了AI，有的完全没用AI，还有混合的。我觉得它们互相催化了，因为大家看到别人都在做这些问题，于是吸引了大量关注。之后进入了一段平台期，基本上所有容易的问题或之前没人看过的问题，现在都已被多个AI和多个人类检视过了。然后就在最近一个月左右，又开始回升——GPT-5.5的发布是一个重要因素。我们开始看到又一批问题被解决。但未解决问题的紫色线仍有六七百个。
要说明的是，这些问题的难度差异极大。有些一页纸就能解决，有些基本上是Annals of Mathematics级别的论文才能解决或取得部分进展。这些是原始数字，没有按难度加权——虽然有些问题确实附有美元奖金（笑），但我们没有尝试做加权处理。
AI在解决这些问题上的用处是多方面的。最早的成功在文献检索方面——大约一年前AI在这方面变得非常强。然后是验证和形式化已有证明，确保其正确性。还有重构——把复杂证明精简为更短的证明，或优化常数。现在AI在生成现有证明的变体方面也非常出色，在各种数值探索和模拟方面也很强。而且越来越常见的是，通过半自主甚至完全自主的方式，只需最少的prompt，就能生成部分或完整的解答。
00:35:44
我们发现了一种阻抗不匹配。解决一个数学问题实际上有三个阶段：第一是证明生成——找到一个完整的证明；第二是证明验证——确保证明没有错误；第三是证明消化——理解关键思想是什么，与已有文献有何关系，叙事是什么，回想起来你自己会怎么想到这个证明，以及现在能回答哪些新问题。
直到大约一年前，这三个阶段都很难，都主要由人类完成。由于它们难度大致相当，我们可以主要关注证明生成——如果你花几个月生成了一个证明，在这过程中你可能也已经完成了验证和消化的工作。我们不需要把这些目标彼此解耦。
但现在随着AI和形式验证的进步，前两个阶段正在变得自动化和快速化，第三个阶段却纹丝未动。于是我们第一次经历了"证明消化不良"——我们在大量生成证明，甚至在验证这些证明，但解决过程并未完成，因为没有人充分理解这些证明到能做报告、能向别人解释的程度。我们没有从这些证明中学到东西——它们只是三分之二的证明。
我认为正确的衡量标准不是证明是否已生成或已验证，而是是否有人能就此做一场报告并接受听众提问。当前AI生成的解答只完成了这个任务的三分之二。
我们在Erdős问题上看到的典型情况是这样的：有人发帖说"在使用GPT-5多次之后，我解决了这个问题"，然后写道——"这份草稿通过了几轮AI检查，但我没有时间亲自验证每个细节，因此发在这里，非常感谢任何评论和检查。"这个案例目前仍未被验证。这就是激励差距——这个人加上GPT获得了解决问题的功劳，但清理和验证的后续工作就没人做了。以前这类解答频率很低，志愿者乐意花一小时帮忙。但现在有大约20个这样的待处理案例积压，都说"我没时间检查或解释"，这变成了别人的问题。我们确实面临着证明消化不良。
而且AI生成的证明读起来往往令人沮丧。比如Jared今早提到的那个案例——Liam Paninski和GPT解决了Erdős问题1196。GPT生成了大约10页的证明，它是正确的，但你读它时会发现：其中一个关键引理，如果你懂数论，就会知道它就是Mordell定理。但证明中从未提及这一点，只是写"这是一个定理，这是证明"。在人类写的论文中，这里会写"由Mordell定理可知"，然后直接往下走。但AI呈现的方式让你觉得这是证明的核心组件，而实际上它只是一个微小的组成部分。人类写作中那些基本的表达特征——强调论证最重要的部分、弱化不重要的部分——在第一代AI生成的证明中往往看不到。
你可以把这些AI证明再喂给其他AI说"请改善表达"，这有一点帮助。但由于激励差距，人们的激励往往只是尽快发布第一个证明，而不做清理工作。这正在成为一个问题。
00:40:44
正如我所说，Erdős问题网站现在第一次出现了交通拥堵。我维护着一个记录所有AI数学贡献的wiki页面，其中有一栏是"待评估的提交"，以前通常只有一两条，现在有二十条。我们在很多情况下缺乏去审查它们的激励。目前我们会挑选看起来最有希望的、贡献者花了时间清理输出并提供人类可读摘要的那些。我们开始在其中一些上推进，但大量仍在积压——而且可能会永久积压下去。
这种情况到处都在发生。你看所有开源项目的pull request，情况非常类似。期刊很快也会面临同样的问题。
一个明显的应对措施是：我们不看AI生成的解答，除非它附带Lean证明。这会有帮助，但那只是第二道过滤。最终我们会面对大量经过形式验证的AI生成证明，仍然需要被消化。这只是部分解决方案。
我认为，直到最近我们只关注证明生成和证明验证作为两个主要步骤，但现在必须认识到：即使证明被验证了，那也不是解决过程的最终阶段。证明消化是重要的第三阶段——它过去在前两个阶段完成时会有机地发生，但现在我们必须把它显式化、赋予它价值，真正重新定义什么叫"一个解答"，并改变激励结构。
这里有一段Bill Thurston非常切题的名言："我们不是在追求定义、定理和证明的某种抽象产量配额。成功的衡量标准是，我们所做的是否能让人们更清晰、更有效地思考和理解数学。"
以上是AI贡献如何给传统工作流制造瓶颈的情况。但还有另一个选择——建造高速公路。也许我们应该接受传统数学是有速率限制的，它能吸收的AI辅助只有这么多。但存在一些以前不可能、现在借助AI变得可能的新数学方式，也许可以扩展规模——我们也应该去尝试这些。我举几个例子。
00:43:36
第一个是我两年前启动的Equational Theories Project，想看能否通过众包自动证明数以百万计的微定理。我挑了一个非常基础的课题——泛代数（universal algebra）。我生成了一系列代数律，比如交换律、结合律，以及其他4000条律，然后问哪些蕴涵哪些。例如，交换律是否蕴涵结合律？每个满足交换律的二元运算是否自动满足结合律？答案是否定的，因为你可以构造一个满足其一但不满足另一个的反例。但这样的问题有2200万个。任意一个问题，代数方向的研究生用纸笔工作一小时大多能判定真假并给出证明，但我没有2000万个研究生。
而且有少数问题确实很难——当律的长度足够长时，判定蕴涵关系是不可判定问题。我限制了律的长度，只允许使用四次运算，这就给出了4000条律和2200万个问题。
三个月内我们解决了所有问题。大约95%可以完全自动化完成，99%可以用各种方法解决——我们主要用的是传统的自动定理证明器，而非现代AI。最后剩下大约100个真正困难的问题需要人工解决，所有结果都在Lean中形式化了。
这个项目非常适合众包，因为有一个清晰的benchmark——有个dashboard显示还有多少蕴涵关系未解决，数字持续下降。人们可以认领一组问题去研究，整个过程高度去中心化：有人给出人工证明，别人转化为Lean代码，又有人将方法自动化并扫描其他2200万个问题看是否适用，运作得非常好。
现在如果你把这些问题输入前沿模型，它能解决99.9%的问题，甚至给出Lean证明。但它每个问题要思考三十分钟，而你有2200万个问题。我们这个项目没有预算，全靠志愿者。原则上一家大型科技公司的前沿模型可以复现整个项目，但成本极其高昂。所以不应该把前沿模型作为第一道防线——应该先用最便宜的工具，比如上世纪九十年代就有的自动定理证明器，尽可能清除低垂果实，然后逐层升级自动化和人工，把最昂贵的资源——人类专家和前沿AI——留给经过筛选的最困难问题集合。
00:47:05
这个项目的一个副产品是，我现在拥有了2200万个代数问题的数据集，这其实是一个很好的测试集。如果你拿一个开源模型——DeepSeek或Qwen之类——给它这些问题，甚至不要求证明，只问蕴涵关系是真还是假，正确率大约只有55%，几乎跟随机猜测差不多。所以当前开源模型在这类问题上非常弱，但它们比前沿模型便宜得多。
目前我正与Damek Davis合作，在Simons Foundation赞助下运行一个挑战赛，看能否通过更好的prompt来提升开源模型的表现，使其接近前沿模型的水平。我们称之为"蒸馏挑战"或"cheat sheet挑战"——类比考试场景：优等生能轻松拿满分，普通学生只能在真假题上拿50%，但如果给普通学生一页cheat sheet，他们在2200万道题的随机抽样上能否提高正确率？
比赛已经运行了大约三个月。参与者免费注册，提交cheat sheet，在我们的playground上针对各种开源模型做benchmark。第一阶段刚结束，最佳cheat sheet能达到80-90%的正确率，即使我们筛选出特别困难的问题，也能看到显著提升——大致在随机猜测和前沿模型表现的中间水平。
现在我们正在运行第二阶段：参与者不再只提交prompt，而是提交Python代码，可以调用LLM，但有预算限制且只能使用开源模型。目标也不只是回答真假，而是要提供Lean证明或反证。看看效果如何会很有意思。
这类任务中，不受限制地使用AI是完全可以的。人们创建自己的harness，用各种自制工具精炼cheat sheet，结果很有趣，而且不受传统数学瓶颈的限制。所以我认为我们必须区分两类工作：传统工作流因结构性原因仍将以人为主导；但我们也应该开创新的挑战——AlphaProof就是一个AI友好挑战的好例子——在这些领域可以真正发挥现代AI的全部能力。
我们需要生成新挑战，同时对于现有任务比如解题，我们需要改变激励机制。仅仅是第一个证明某件事或第一个形式化定理，这不应该继续被视为首要目标——它只是目标的一部分。阐释和消化正变得远为重要。
更广泛地说，我们需要更善于清晰表达目标。给人类一个任务，人通常不仅理解你明确说出的内容，还能读出言外之意、理解你的隐含目标。但AI就像那些能非常字面地实现愿望的精灵——你让它做什么，它就做什么，但你随后意识到还有其他你也想要但没有说出来的东西。所以我们需要更多思考：我们的目标到底是什么？我们为什么做数学？
00:51:59
观众1:
你提到激励机制的差距，让我想到Szemerédi定理——最初有一个复杂且不透明的证明，之后出现了更具启发性的证明，而这些后续证明同样受到推崇，尽管它们并没有证明什么全新的东西。这个类比对于思考如何应对AI有参考价值吗？
Terence Tao:
是的，这种证明演替在人类数学中已经发生了。第一个证明定理的人往往不是最适合解释证明的人。而且仅仅是知道定理为真这一心理突破，本身就能间接启发其他证明。所以AI给出一个不可压缩的证明仍然有价值——这已经在发生了，很快就有其他证明出现，部分受到AI证明的启发。
但新的问题是阻抗不匹配（impedance mismatch）。以前，愿意消化证明的人数及其能力，大致与生成证明的能力相当。但如果证明生成能力增加了一两个数量级，而消化能力没有提升，就会产生交通拥堵。如果你有十个甚至一百个能产出定理的人，却只有一个能消化这些工作的人，那就是个问题。
观众2:
你提到了"只需形式化验证"的证明类别，Equational Theories Project是个很好的例子。在更传统的数学领域中，有没有类似的情况——不值得去理解实际证明，只需要验证？
Terence Tao:
有的。我现在正在做的数论领域中，有一个分支叫显式解析数论（explicit analytic number theory）。解析数论经常说某个量渐近趋于零，对任意epsilon存在常数C满足某个界，我们大量使用大O记号。但通常我们不写出具体常数，因为太混乱了，就说"存在一个常数"，但不写出它具体是什么。
而显式解析数论就是仔细算出所有常数——这个常数是6.5，这个界在N大于10的46次方时成立，诸如此类。这个领域的人极其谨慎，做大量精确数值计算和微优化，工作非常枯燥。但我们又对论文中任何错误都极度偏执，因为这些结果层层叠加相互依赖。
所以我们希望有自动化方式来验证和生成新结果。每当某个界被改进，它如何传播？如何影响其他常数？就像更新Excel表格中的一个单元格，其他单元格也应该随之更新。你没有在做什么有趣的新数学，只是在重新计算，然后用Lean之类的工具验证。这完全适合AI来做——没人想做这种事。传统数学中确实存在这类非常适合外包给AI的任务，我们应该多想想还有哪些类似的项目，让它们与人类数学研究并行运作。
00:56:27
观众3:
你提到证明生成和验证不再那么优先，但我们仍需要proof digestion。你会建议如何改变数学教育？从研究生的分析课到本科的线性代数课，怎样才能适应这种变化？
Terence Tao:
我们还没有答案，但我认为需要降低"得到正确答案"作为主要评估标准的优先级。我们已经处于这样一个时代：几乎任何本科数学课程的随机作业题甚至考试题，AI都能正确解答。
我认为我们需要转向演示、项目、讨论、对话等形式。有一些有趣的实验——哈佛有位数学教授让整个班级协作生成一个prompt，目标是让AI尽可能准确地解答两年前的期末考试。学生分成几个团队：一个负责数据生成（创建新的测试题），一个负责prompt工程（设计好的prompt），一个负责评估AI输出，还有一个负责整体编排协调。最终的prompt大约能正确解答50%的期末考试题，表现令人印象深刻。而且这个过程对所有参与的学生都非常有教育意义。
所以我们需要创造性地应对。至于传统的评估方式，除非你在完全没有AI辅助的环境下进行现场考试，否则我认为基本上已经行不通了。
00:58:45
观众4:
能否用带人类反馈的强化学习（RLHF）来做证明消化？
Terence Tao:
我的简短回答是不行。当你只有一把锤子时，一切看起来都像钉子。你确实可以制造出看起来像证明消化的东西——制定评分标准来判断引用是否正确、要点是否突出，让AI互相评判。但如果你过度依赖这类度量标准，就会出现reward hacking，反而可能让问题更严重——你会得到看起来在解释问题的论文，但很久之后才发现那些解释其实是误导性的，没有强调正确的东西。
消化需要时间。有些论文的影响两年后才被意识到，当时没有任何明显的度量指标能表明这是一个突破。后来在某个语境下发现了与其他数学领域的联系，回顾起来才知道那篇论文预见了当时没人看到的发展。优化有它适用的地方，但也有些事情是优化会伤害的。不能因为优化在某些时候有效，就把它当成解决一切问题的锤子。
Jared:
或许费马是第一个这么干的人——他说空间不够，没法写完证明，堪称第一个"不消化者"。
Terence Tao:
哈哈。确实，现在这个问题更普遍了，但未来我们可以做更多的消化工作。
热门跟贴