夜雨聆风
嗨大家好，这里是硅潮。
陶哲轩最近做了一个很少见的动作。
他没有宣布某个新定理，也没有评价某个模型的胜负。他公开调整了自己的数学工作习惯：以后会减少对新证明的实时跟进，只优先处理几类情况，比如期刊审稿、青年研究者的成果、与自己工作高度相关的结果、经过形式化验证的证明，以及作者已经花力气做过充分解释的材料。
这件事的信号很强。数学界正在从“证明稀缺”进入“证明丰裕”。当候选证明变得越来越容易产出，真正稀缺的资源开始转向验证、消化和判断。
一、过去的数学，奖励“第一个走出来的人”
几千年来，数学大体生活在证明稀缺的环境里。一个重要猜想可能悬在那里十年、二十年，甚至更久。一个人或几个人花很长时间拿下它，这就是数学史里最熟悉的英雄叙事。
在这样的环境里，“谁先给出证明”天然是一个好指标。原因很朴素：能先走出来的人，通常也已经读过关键文献，理解前人卡住的地方，掌握了核心技术，并且能向同行讲清楚这条路为什么能走通。
证明、验证、理解，在人类研究里往往绑在一起。一个数学家完成证明时，消化过程已经在脑子里发生了很多轮。
陶哲轩这次真正提醒大家的地方在这里：这个绑定关系，正在被模型工具拆开。
二、三段式工作流：生成、验证、消化
陶哲轩把问题解决过程拆成三段：proof generation，proof verification，proof digestion。
第一段是证明生成，也就是找到一条可能成立的路线。现在模型已经可以快速提出候选路径、构造引理、整理证明草稿，甚至在一些题目上给出完整方案。
第二段是证明验证。Lean、Coq 这类形式化工具，再叠加模型辅助，正在让一部分检查工作变得更机械、更严格。候选证明能否通过逻辑检验，开始有更自动化的处理方式。
第三段是证明消化。它的含义更宽：这条证明和已有文献怎样连接？核心困难在哪里？有没有新概念可提炼？哪些技术能迁移到别的问题？一个研究者能否站在黑板前讲清楚，并回答追问？
目前最拥堵的地方，正是第三段。
三、Erdős Problems 的积压，是一个早期信号
Erdős Problems 网站已经专门整理 AI 相关贡献。页面里有一个“Pending assessment”区，收纳等待评估的候选结果。最近这一栏出现了明显积压，里面既有声称完整解决的条目，也有部分进展。
这类积压说明一个很现实的问题：模型可以让候选材料快速增多，但评估并不会自动同步扩容。专家时间、形式化成本、文献对照、概念提炼，全都需要人来承担。
数学第一次遇到一种类似“数据洪流”的处境。生物学有测序数据爆炸，天文学有望远镜数据洪流。轮到数学，洪流的形式变成了候选证明。
四、正确证明也可能没有被真正吸收
这件事最麻烦的地方，并非模型会犯错。错误证明可以被检查、被驳回、被修正。更难处理的是另一类材料：逻辑上可能成立，但尚未转化为人类可继承的理解。
数学研究有显性目标，也有隐性目标。显性目标是把某个定理证明出来。隐性目标包括理解结构、发现新概念、训练直觉、连接文献、启发后续问题。
过去这两类目标高度重合。人类研究者在证明过程中会自动完成大量隐性工作。模型工具介入后，显性目标可以被加速，隐性目标却需要额外安排。
一个问题被标记为“已有候选解”，可能会让后来者减少投入。可如果这条路线没有被讲清楚、整理好、放回知识体系，它对领域的真实帮助就很有限。表面上多了一个答案，社区理解未必同步增长。
五、古德哈特定律也进入了数学
陶哲轩提到了 Goodhart’s law：当一个衡量标准变成目标，它就会失去作为衡量标准的可靠性。
“第一个证明出来”在证明稀缺时代很好用。它和真实进步高度相关。进入证明丰裕时代后，这个指标开始失真。
如果所有人继续围绕“谁先给出证明”竞速，系统会产出更多待评估材料，专家被迫把时间投入判断真伪和补充解释。长远看，这可能拖慢真正的理解。
新的奖励对象需要扩大：验证者、解释者、整理者、形式化者、能把复杂证明变成新概念的人，都在承担越来越关键的工作。
六、数学给科研人提前打了样
把视角从数学拉远一点，这个结构会出现在几乎所有知识工作里。
代码可以被模型快速写出，review、测试、架构维护会成为新瓶颈。 论文草稿可以批量出现，真正阅读、复现、判断贡献的人更稀缺。 实验假设可以快速生成，能设计关键验证、排除伪相关的人更重要。 诊断和分析可以很快给出，能够承担责任、解释推理、处理例外的人更值钱。
接下来，很多团队会发现自己缺的并非更多输出。缺的是把输出变成可靠知识的流程。
七、以后看模型答案，先过这张检查表
对科研人和内容团队来说，这个信号很实用。以后评估一份模型产出的材料，可以先问五个问题。
它有没有被验证，验证方式是什么？ 有没有人能讲清楚核心想法，而非只复述结论？ 它和已有文献、代码库、实验记录怎样连接？ 它是否提炼出可复用方法，能迁移到下一次任务？ 它是在训练人的判断，还是只增加待处理材料？
如果这五个问题答不上来，这份材料就还停留在“原料”层面。它可能有用，但还没有变成知识资产。
八、真正升值的，是消化能力
陶哲轩按下暂停键，并没有表达对工具的排斥。相反，他给出的方向更务实：承认证明生产变快了，然后重做工作流。
数学未来会需要新的竞赛规则、新的审稿习惯、新的形式化协作方式，也会需要更多把证明讲清楚的人。
对更广泛的 AI 科研工作流来说，这就是预告片。模型会继续降低产出成本，但理解、验证、组织和判断会变得更贵。
产出过剩之后，真正的高手不再只是“拿到答案的人”。更关键的人，是能把答案变成可继承知识的人。
往期推荐
ChatGPT Images 2.0 做科研配图，关键不在好看，在可控：https://mp.weixin.qq.com/s/nsR71V7ZbKloo0p70SG1xw ChatGPT Image2 科研绘图模板库：机制图、流程图、综述图、封面图都在这：https://mp.weixin.qq.com/s/4nvf8HhZ-CisazWxpU2C4Q Claude 用量翻倍背后：科研 Agent 的真实瓶颈：https://mp.weixin.qq.com/s/KoYBvlUY8BzdMBboGOb4cg
