“我身边搞数学的，最近都去搞趣味数学了，”一位前沿模型研究员调侃道，“大家都觉得搞数学已经没意义了，竞争不过AI。不如去搞点趣味数学，搞搞乐子，教教小朋友。”
读完这篇报道，我最在意的是一个变化：当解题速度大幅提升，研究的价值该如何衡量？答案的数量、答案的可信度，以及人从研究中获得的能力，正在变成三个必须分别讨论的问题。
解题越来越快，科研评价需要换重心
据报道，OpenAI一次公布了722篇模型生成的数学手稿，涉及372个结果系列和约4000个测试问题。这样的产出规模，已经把压力从解题端传到了审核端。
过去，数学研究的一条重要评价标准是：谁先解决某个公开问题。课题、经费和阶段性成果，也往往围绕这条标准组织。如果AI显著缩短了解题周期，受到冲击的就包括整套科研组织方式。
报道用陶哲轩提出的“Math 1.0”和“Math 2.0”概括这种转变：从重视率先解题，转向更加重视解释、社区建设和开辟新的研究方向。
我认为，这比“数学家还有没有工作”更值得讨论。解题能力变得充裕之后，什么问题值得研究、不同结论如何联系、一个证明带来了什么理解，会在评价中占据更大的分量。
至于研究员调侃大家转去做趣味数学，我更愿意把它看作旧有职业路径受到冲击的情绪表达。它不足以支持“数学研究已经没有意义”的判断。
机器验证有两道不同的关口
报道把可靠性问题集中到了Lean上。它要求将数学命题和证明写成精确的形式化表达，再由程序检查推导是否成立。
这里必须区分两件事：形式化表达是否准确对应原来的问题，以及证明是否在给定假设下成立。
如果第一步把假设改了、把结论弱化了，即使第二步通过检查，也可能只证明了另一个命题。把这种情况说成“正确证明了错误的定理”容易引起误解。更准确地说，是证明通过了，但它没有回答原本的问题。
验证工具自身的可靠性又是另一层问题。报道提到，Lean曾出现让错误证明通过检查的实现漏洞；OpenAI公布的手稿中，也有3篇随后被撤回。这些案例说明，“通过检查”需要说明检查了什么、依赖哪些假设和工具。
我的判断是，形式化验证仍有重要价值，但可信度不能被压缩成一个通过标记。命题翻译、推导过程和验证程序，每一层都需要有人承担责任。
证明的生产速度，已经超过理解速度
当AI批量生成证明，人类逐篇阅读、理解和复核的能力，就可能成为瓶颈。报道所说的“证明消化不良”，描述的正是这种失衡。
如果生成工具、检查工具和修复检查工具的过程都越来越依赖AI，我们还需要判断：这些环节是否具有足够独立的纠错能力。报道转述的黑尔斯对隐秘缺陷的担忧，应当作为验证链条的问题来理解，不能据此认定已经存在后门。
我认为，成果生产者需要把验证成本纳入交付。批量发布结果之后，再让学术共同体承担全部辨伪工作，会让产出与责任脱节。
能复核的证明、清楚的假设、自然语言与形式化表达之间的对应关系，都应当成为成果的一部分。产出越快，对这些工作的要求就越高。
论文数量与社会进步之间，还有很长的路
报道中的另一个判断值得保留：模型能力提升，不会自动转化为同等速度的科研落地和现实交付。
数学结果需要被理解、连接和使用。涉及物理世界时，还要经过实验、工程和组织协作。某个环节提速，并不意味着后面的环节已经完成。
因此，我不会用几百篇手稿直接推断科技即将全面爆发，也不会因为短期应用不明显就否定这些结果。更有意义的是看：哪些成果经得起验证，哪些带来了新方法，哪些正在被后续研究采用。
数量容易展示，影响需要时间证明。把两者混在一起，既会制造繁荣的错觉，也会放大被替代的焦虑。
科研还承担着培养人的任务
科研除了获得结论，也在训练人提出问题、处理不确定性、识别错误，并为自己的判断负责。
如果评价只剩下成果数量，AI会迅速改变竞赛格局。但如果研究过程培养出来的人同样是目标，我们就需要重新设计课题、训练和协作方式。
在我看来，AI越能承担推导和搜索，人越需要练习选择问题、理解关键步骤和审查结果。让人保有这些能力，才能持续使用、纠正和发展机器带来的成果。
面对这场变化，我更关心科研共同体能否建立新的评价和责任机制：让快速生成的答案得到可靠检验，也让参与研究的人继续成长。