陶哲轩：AI辅助数学证明如同汽车冲击城市，需构建新型基础设施

IT之家 3 月 22 日消息，据 The-decoder 报道，数学家陶哲轩将人工智能与形式化方法对数学研究实践的影响，比作汽车对城市发展的冲击。这一类比同样适用于包括编程在内的其他领域。

汽车比以往任何交通工具都更快，但它们让原本为人、马匹和马车修建的道路变得拥堵。新建的道路与高速公路让高速出行成为可能，却也带来了城市无序扩张、交通拥堵和环境问题。陶哲轩写道，只有经过深思熟虑的城市规划与交通规则，才能以合理的方式将两种世界融合起来。

IT之家注意到，数学现有的体系 —— 期刊、会议、师徒传承、引用体系，就像古老而狭窄的道路：它们是为人而建的。人类完成的证明或许缓慢，但会产生极具价值的附加效应：研究者锤炼专业能力、勾勒数学版图、发现新的研究方向，并记录下那些富有启发意义的死胡同与迂回路径。

陶哲轩认为，AI 辅助证明可以高效地从假设直达结论，却恰恰在过程中丢失了这些附加价值。这类证明往往不适合发表在传统期刊上，因为人们期待的、关于证明思路与探索过程的叙述几乎完全缺失。他将试图升级 AI 模型以产出可发表论文的做法，比作强行把汽车改造去适应为人设计的街道。

陶哲轩认为，更好的做法不是把 AI 强行塞进现有体系，而是创建适配机器的新型数学基础设施，用以补充而非取代人类的研究路径。他举例：可以借助形式化证明助手验证结论的大型数学难题，或是自动生成的粗略证明库，再由人类将其打磨成更高质量的版本。他还提议建立一门类似城市规划的新学科 ——“AI 规划”，以保留数学“可步行探索”的本质。

在与德瓦凯什 · 帕特尔的对话中，陶哲轩进一步阐述了这一观点：AI 确实让他的工作“更丰富、更广阔”，例如借助更多图表、代码以及更深入的文献检索。但他数学研究的核心工作，依然依靠笔和纸完成。他表示，如果没有 AI 率先提供的这些附加手段，如今一篇论文的完成速度并不会比过去快太多。AI 并没有大幅加快实际研究过程，而是打开了全新的可能性。

“我认为 AI 已经把想法生成的成本降到近乎为零，这与互联网把沟通成本降到近乎为零的方式非常相似。这是一件了不起的事，但它本身并不能直接创造知识的富足。现在的瓶颈已经变了。我们突然面临这样一种局面：人们可以为一个科学问题生成成千上万种理论。接下来我们必须去验证、去评估它们。”陶哲轩解释道。