导语
The Decoder 这篇文章梳理了数学家 Terence Tao 对 AI 与数学研究关系的一套核心判断：AI 和形式化工具会显著提升效率，但它们对学术实践的改变，更像汽车改变城市，而不是简单地给原有流程装上一台更快的引擎。
Tao 的类比是，汽车比以往任何交通方式都快，却也堵塞了原本为行人、马匹和马车设计的道路。后来修建的新公路和高速公路虽然带来了快速通行能力，却同时带来了城市蔓延、交通拥堵和环境问题。只有经过审慎的城市规划和交通规则设计，两个世界才可能被更合理地结合起来。
在他看来，现有数学研究的基础设施——包括期刊、会议、导师制度和引用体系——就像为人类研究者修建的老路。传统的人类证明虽然慢，却会自然产生很多“副产品”：研究者积累直觉与专长，勾勒数学地形，发现新的研究方向，也会把无效路径和绕路过程记录下来。
核心信息
而 AI 辅助证明虽然可能更高效地把假设推进到结果，却恰恰容易丢掉这些过程性价值。Tao 认为，这也是很多 AI 生成或 AI 辅助产出的证明并不适合直接进入传统期刊的原因，因为它们往往缺少人类学术共同体所期待的那种“通向证明的叙事”。
因此，他主张与其强迫 AI 去适配旧体系，不如建设一套新的、对机器更友好的数学基础设施，而且这套基础设施应该补充人类路径，而不是替代人类路径。比如，可以把大型数学挑战交给形式化证明助手来验证，或者先由系统自动生成粗略证明库，再由人类研究者继续提炼成更高质量的版本。
Tao 甚至提出了一个类似“urban planning”的概念——“AI planning”。他的意思不是让 AI 主导数学，而是像城市规划那样，为高效率工具设计新的规则与空间，同时尽量保留数学研究原本那种“walkable”的特性，让人类仍能理解、学习并在其中探索。
更多细节
在与 Dwarkesh Patel 的对谈中，Tao 进一步解释说，AI 确实让自己的工作变得“更丰富、更宽广”，例如可以加入更多图形、代码和更深入的文献检索；但他完成数学核心工作的方式依然是纸和笔。若把这些新增能力剥离掉，一篇论文真正核心的数学推进速度，并没有因为 AI 而出现同等幅度的加快。
他给出的总结很有代表性：AI 让想法生成的成本几乎降到零，这一点很像互联网把沟通成本降到接近零。但这本身并不会自动创造 abundance。新的问题在于，研究者现在可能一下子面对成千上万条理论路径，真正困难的不再是“想不出点子”，而是怎样验证、筛选和评估这些点子。
从这个角度看，AI 带来的不是终点式自动化，而是研究瓶颈的位置变化：过去的紧缺资源是创意，现在越来越紧缺的是验证能力、评价机制，以及能让机器输出重新进入人类知识体系的中间层基础设施。对数学如此，对编程和其他知识密集型领域同样可能成立。
