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

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

数学家陶哲轩提出一个精妙类比：人工智能与形式化验证工具对数学领域的渗透，犹如汽车问世对传统城市规划的冲击。这一洞察不仅适用于数学，更映照着整个科学研究与工程技术领域的范式转换。

汽车的绝对速度优势毋庸置疑，但它一旦驶入为马车设计的古老街道，立刻引发系统性瘫痪。我们为此修筑高速公路网络，实现了点对点的高速移动，却又衍生出郊区蔓延、结构性拥堵与生态负担。陶哲轩指出症结：唯有通过前瞻性的顶层设计与适配的规则框架，才能协调高效运输系统与人性化生活空间，实现“汽车生态”与“步行生态”的有机融合。

当古老的“道路”遇上AI“汽车”

现行数学研究体系——包括学术期刊、会议评审、师徒制传承与文献引用网络——本质是一套为人类认知节奏设计的“步行系统”。研究者沿论证链条逐步推进，其价值不仅在于抵达终点：过程本身锻炼数学直觉，勾勒学科知识图谱，并能意外开辟全新研究方向。那些富有启发性的试错路径与未竟思路，同样构成学术传承的关键路标。

矛盾由此产生。AI辅助证明能实现从公理到结论的高效直达，但这趟“特快列车”往往遗失了沿途的认知景观。其结果便是产出一种尴尬的证明形态：它们难以融入传统出版体系，因为同行评审所依赖的论证脉络、思想演变与启发式讨论近乎空白。试图强制AI模型生成符合传统论文范式的输出？陶哲轩认为这无异于将汽车改造为马车以适应旧街道——本质上是战略误判。

与其改造“汽车”，不如规划“新城”

真正的解决方案并非削足适履，而是构建一套并行的、专为AI协同设计的基础设施。新体系的核心使命是互补与增强，而非简单替代人类研究路径。

具体蓝图如何展开？陶哲轩勾勒出几种可能形态：利用形式化证明助手对复杂猜想结论进行机器验证；建立由AI生成的证明草图库，供数学家精炼、优化与概念升华；甚至需要开创一门类似“城市科学”的新交叉学科——或可称为“AI系统规划学”——其核心任务正是确保数学在智能化时代依然保持其“可漫步探索”的知识特质。

AI的价值：不是加速，是拓宽边界

在与德瓦凯什·帕特尔的对话中，陶哲轩进一步阐明其观点：AI确实使他的研究工作“维度更丰富、疆域更广阔”——例如借助可视化图表、可执行代码进行思维推演，或实施更深度的文献语义挖掘。然而，数学发现中最核心的创造性突破，依然诞生于传统的纸笔沉思之中。若剥离这些外围AI增强工具，他完成一篇核心论文的周期并不会显著缩短。

这揭示了AI变革的真实维度：其颠覆性不在于线性加速既有流程，而在于指数级拓展了问题求解的搜索空间。陶哲轩如此总结：“AI已将创意生成的成本降至近乎于零，正如互联网将通讯成本降至近乎于零。这是划时代的突破，但它本身不直接等同于知识增长。真正的瓶颈已经转移：我们现在能针对单一科学问题瞬间生成海量假说与路径。未来十年的核心挑战，将是我们如何有效验证、评估与整合这片思想的海洋。”

这才是问题的枢纽。AI不是更快的马，它是内燃机，迫使我们重新设计整座知识生产的城市。