数学的流水线，停在了第一站
10月5日，陶哲轩的博客上挂出一篇客座文章，《数学的未来》，作者是CMU的Jeremy Avigad——Lean形式化数学社区的核心人物。文章里有一句平静到近乎惊悚的判断：一年前还够得上”体面论文”水平的数学结果，如今借助AI已经可以轻松生成。数学家们引以为傲两千多年的那条流水线——提出问题、拆解近似、逐一攻克、发表晋升——第一站还在人类手里，后面的站点正在被机器逐个接管。而文章透露的数学界整体反应，居然是”积极”。被拆掉的是自己的流水线，全场鼓掌，这个画面本身就值得一篇博客。
一、”够发表”这三个字，正在肉眼可见地贬值
先把一个误会拆掉：论文从来不是知识的容器，论文是信号。学术界真正流通的货币是”此人具备产出新知识的能力”这个信号——职称、经费、教职、头衔，全部锚定在这枚货币上。”发表”只是这枚货币的铸造工序。所以当AI可以批量铸造”够发表水平”的结果时，发生的不是知识爆炸，是货币超发。
超发的机制藏在Avigad那句被轻描淡写的话里。他说数学家的日常工作流——把难题拆成近似、解决近似、再变参数推广——正在被直接打断。注意这个工作流的性质：它不是数学创造的核心，它是数学劳动的执行层。而执行层恰好是大模型最擅长的事：大规模、不知疲倦、不嫌枯燥的系统性搜索。人类博士三年认真做十个近似，模型一晚上扫一千个变参数。一年前”够发表”的门槛是按人类产能标定的，现在产能涨了两三个数量级，门槛还钉在原地——结果就是”发表”这两个字的含金量，像通胀里的纸币一样，面额没变，购买力腰斩。
数学界的”积极”反应，短期看每一方都是赢家：教授产出翻倍，学生毕业提速，期刊永不缺稿。所有人都在忙着花新钱，没人盯着汇率。同期还有个注脚可以对照看：同一周，一支Claude Opus 5.5智能体团队与合作研究员跑了几百次DFT计算，筛出两种室温反铁磁半导体候选材料，计算数据、代码连同已知瑕疵清单全部公开，任何人可验证。连材料学这种烧钱的实证学科都开始进入”AI自主发现、公开可验证”的节奏了，而数学——一个验证成本本该最低、形式化程度本该最高的学科——衡量产出的标准居然还停在”是否够得上发表”这种以人类为中心的老尺子上。用印钞时代的标准管理金本位的声誉，数学界的乐观，恐怕是算错了账。
二、被夺走的不是王冠，是中间那一段
把数学创造这件事拆开看，它有三段结构：一端是提出值得证明的问题，靠品味；一端是验证证明对不对，靠机械；中间是漫长的拆近似、算特例、换参数，靠苦功。AI这次拿走的是中间那段，形式化工具又在蚕食末尾那段——Lean社区这些年干的就是把”验证”从同行评议的手工作坊搬进编译器。三段里只剩下第一段还完全是人的。
我不同意把这读成坏消息。恰恰相反：证明免费之后，”值得证明什么”的定价权第一次完全回到了人类手里。菲尔兹奖从来不奖励证明的字数，它奖励第一个打通某条路的人——顶层荣誉体系早就承认，问题的价值高于解答。真正扭曲的是顶层之下的整个激励体系：作业、资格考试、博士论文、终身教职的成果清单，全部训练和定价的是中间那段苦功。也就是说，数学界从”解题者公会”变成”出题人公会”的大转型里，上层建筑已经换了打法，地基还是旧的。
这才是”社区反应积极”背后被略过的部分。积极，是因为现役数学家恰好站在转型的受益侧：他们的品味已经长成了，AI替他们干了学徒期。就像自动化来了之后，最开心的是已经在管理岗的老师傅。但一个行业的转型不能只看现役选手的体感，还得看它还收不收新学徒——这就引出了真正的麻烦。
三、流水线入口的窘境：博士们在学一门刚被自动化掉的工种
看一眼数学博士生的课程表：读文献找缺口，拆引理算特例，磨技巧凑推广——这套手艺训练的，恰好是被AI接管的那一段中间工序。相当于自动驾驶普及的前夜，驾校还在重点教换挡。Avigad的文章说要重新定位研究方向、重新培养下一代数学家，方向没说错，但文章没有展开的是转型期的代价：有两三代博士生，入场时学的是手艺，出场时手艺已经成了共享基础设施。
更安静的问题是：品味从哪来？很多人默认”提出好问题的能力”是天赋，其实它绝大部分是从几十年的解题苦功里长出来的——做过一千个近似的人，才知道第一千零一个近似值不值得做。现在的方案是把这个学徒期整体外包给机器，然后期待下一代人类凭空长出品味。这就好比取消了所有的练习赛，直接培养决赛选手。转型期最需要的两种能力——判断什么问题值得做的品味，和读写形式化证明的素养——没有一样在现行的培养方案里被当作主课，前者根本没法教，后者几乎没人教。
于是出现一个很安静也很荒诞的闭环：教授用AI找题目，学生用AI补证明，答辩委员会用AI审论文，链条上每一环都很高效，整条链合起来却回答不了一个问题——这一届人类，到底是谁学会了数学？数学界今天在陶哲轩博客评论区里讨论的这个问题，看着像学术圈的内部事务，其实是其他所有学科的前瞻预告片。
结语：证明免费之后
数学是所有学科里最先走完这条曲线的，原因很朴素：它的验证最便宜、形式化最彻底，所以自动化最先穿透它。这也意味着它是最早拿到完整剧本的学科——证明免费之后，数学家能卖的东西只剩下一样：知道哪里值得证的判断力。这个结论很快会排着队走向其他领域：写代码免费了，卖什么？写报告免费了，卖什么？数学只是先替所有人把账算了一遍。
所以流水线并没有停。它还在转，只是把人往上游挤了一站，从”做解答的”挤成”提问题的”。挤得上去的，头衔从解题者换成出题人，反而解脱；挤不上去的，才是真正被停掉的那部分。两千年前欧几里得对托勒密说”几何学中没有王者之路”，意思是数学没有捷径。这句话要改改了：通往证明的路现在到处都是捷径，只是那条路上，已经不怎么需要人了。
题图与文中配图：封面为程序生成；两张实拍图来自Unsplash，署名如下。
📷 Photo by Roman Mager on Unsplash
📷 Photo by Austin on Unsplash