陶哲轩最近聊到了AI和数学这事儿，给大家打了个比方，说人工智能跟形式化方法对数学研究的影响，就像当年汽车冲进城市一样。这个说法不光是针对数学的，对编程还有其他学科也有启发。他说，汽车虽然让咱们出行方便多了，可也把传统的道路堵得一塌糊涂，弄得城市到处扩张没有章法。这就得靠科学的规划和管理，才能让老路子和新路子和平共处。 在数学里，以前大家用的那些体系——比如发文章、开会、师徒带徒弟、互相引用——就好比是专为人类大脑设计的窄胡同。虽然人脑推理证明起来慢腾腾的，但这种慢过程里藏着不少好东西：研究者练出了本事，画出了知识网，发现了新方向，还记录下了路上遇到的各种坑和惊喜。这些收获都是做数学研究必不可少的。 陶哲轩发现，AI帮忙证明虽然能快速从假设跳到结论，但它常常跳过了人类思考的那些关键步骤。这种证明因为没有详细展示探索的路径，很难达到传统期刊的要求。他形象地把硬改AI模型来适应现有学术体系的做法，比作让汽车在给行人设计的街上跑——看着能跑通，其实违背了技术发展的根本逻辑。 为了解决这个难题，陶哲轩提了个构建新型数学基础设施的法子。他建议用形式化工具来验证复杂命题，或者先让机器弄个初步证明库出来，再让人来优化完善。这样既能保留人类脑子的创造力，又能发挥机器计算的高效率。他特别强调得发展个像城市规划一样的“AI规划”学科，确保数学研究还能保持“走着走着就探索到”的那个味儿。 和同行聊天时，陶哲轩进一步说了说AI对数学的实际影响。他承认这些工具能帮人看图表、写代码、找文献，确实把视野给拓宽了。不过真正出活儿的时候还是得靠手写推导这一套老办法。他说要是没有AI帮忙，现在写论文的速度跟以前其实也快不了多少。AI的价值不在于把事情做得更快，而是把原本想都不敢想的可能性给打开了。 陶哲轩解释说，“AI把想法生成的边际成本压得几乎为零”，跟当年互联网降低沟通成本的效果其实是一样的。“但这并不直接带来知识生产的大爆炸”，现在最大的问题是大家能针对同一个科学问题堆出一堆理论来，“怎么挑哪些理论值得信”就成了新难题。这种变化逼着研究者得想出新的评估标准和验证办法，好对付信息爆炸带来的脑子不够用的问题。