IT之家 3 月 22 日消息，据 The-decoder 报道，数学家陶哲轩将人工智能与形式化方法对数学研究实践的影响，比作汽车对城市发展的冲击。这一类比同样适用于包括编程在内的其他领域。汽车比以往任何交通工具都更快，但它们让原本为人、马匹和马车修建的道路变得拥堵。新建的道路与高速公路让高速出行成为可能，却也带来了城市无序扩张、交通拥堵和环境问题。陶哲轩写道，只有经过深思熟虑的城市规划与交通规则，才能以合理的方式将两种世界融合起来。IT之家注意到，数学现有的体系 —— 期刊、会议、师徒传承、引用体系，就像古老而狭窄的道路：它们是为人而建的。人类完成的证明或许缓慢，但会产生极具价值的附加效应：研究者锤炼专业能力、勾勒数学版图、发现新的研究方向，并记录下那些富有启发意义的死胡同与迂回路径。陶哲轩认为，AI 辅助证明可以高效地从假设直达结论，却恰恰在过程中丢失了这些附加价值。这类证明往往不适合发表在传统期刊上，因为人们期待的、关于证明思路与探索过程的叙述几乎完全缺失。他将试图升级 AI 模型以产出可发表论文的做法，比作强行把汽车改造去适应为人设计的街道。陶哲轩认为，更好的做法不是把 AI ...