陶哲轩：AI正将优美数学变成训练废料

数学界顶流陶哲轩（Terence Tao）最近抛出一个刺耳的比喻：硅谷用AI冲击那些悬而未决的数学难题，正在把优美的数学变成“有毒废料”（toxic waste）。这个说法出自Reddit上引发热议的一则讨论，指向的并非AI能否解题，而是它解题的方式正在重塑数学研究的审美与价值秩序。

从“优雅证明”到“原始训练材料”

陶哲轩的核心批评是：硅谷对长期悬而未决的数学猜想有强烈的攻关冲动，但AI给出的往往是可验证却缺乏结构美感的解法。这些解法把数学对象降格为“raw training material”——原始训练材料，而不是值得欣赏的智力作品。

数学界对“优雅”有近乎苛刻的执念。一个证明是否简洁、是否揭示深层联系、是否可推广，往往比“是否成立”更重要。AI的暴力搜索式证明可以跨过终点线，却可能绕开所有让数学变得迷人的路径。陶哲轩担心的正是这种路径的消失：当结果可以被批量生产，过程的美感就失去了生存空间。

“数学优雅性”是数学共同体内部一个虽无严格定义却被广泛使用的评价标准，通常指向证明的简洁性、揭示深层结构联系的能力以及可推广性。与之相对的是“暴力证明”或“计算证明”，即通过穷举、大规模计算或机器搜索直接验证结论，而不提供人类可理解的推理路径。四色定理的计算机辅助证明、开普勒猜想的Formal Proof都曾引发类似争论：结论被接受，但过程是否构成“数学理解”存疑。陶哲轩的批评延续了这一传统，只是AI使暴力证明的生产速度提高了数个量级，从而使审美与效率的张力从个案变为系统性问题。

“有毒废料”比喻的锋利之处

“有毒废料”这个措辞之所以传播得快，是因为它同时指向两层问题。

一层是认知层面的：大量低质量、机器生成的证明涌入文献，会抬高研究者筛选和验证的成本，污染知识生态。另一层是激励层面的：如果攻克难题的荣誉和资源流向AI辅助的“暴力解法”，年轻数学家钻研优雅方法的动力会被稀释。

这并非否定AI的数学能力。陶哲轩本人的态度一向务实，他关注的是AI介入后数学社区如何重新定义什么是有价值的工作。废料的对立面不是“无用”，而是“本可优雅却被粗暴处理”。

硅谷的攻关逻辑与数学社区的节奏冲突

硅谷习惯用“攻克难题”来叙事：选一个大问题，投入算力，宣布突破。这套逻辑在工程领域有效，在数学领域却容易错位。数学猜想的解决往往需要多年沉淀，其价值部分来自解决过程中诞生的新工具和新视角。

当AI跳过这些中间产物直达结论，数学社区失去的不只是一个证明，而是一整条可能通向其他领域的思想路径。陶哲轩的警告针对的是这种结构性损失，而非某一次具体的AI解题成果。

数学猜想的解决之所以重要，不仅在于结论本身，更在于解决过程中产生的新工具、新方法乃至新学科分支。例如费马大定理的证明催生了代数数论的诸多进展，庞加莱猜想的解决推动了Ricci流与几何分析的融合。这种“过程溢出效应”是数学知识增长的核心机制之一。当AI以端到端方式直接输出可验证结论时，中间产物——那些可能被其他领域借用的定义、引理、构造技巧——被系统性跳过，数学社区损失的是潜在的思想基础设施，而不仅仅是一个漂亮的证明。

数学家该如何与AI共处

批评不等于拒绝。更建设性的读法是：数学社区需要主动设计AI的使用方式，而不是被动接受硅谷设定的议程。比如把AI定位于猜想探索、反例搜索、形式化验证等辅助环节，把审美判断和方向选择留给人。

陶哲轩的发言更像一次议程设置——在AI大举进入数学之前，先把“什么值得做”这个问题摆上桌面。数学的美不是装饰，它是这门学科筛选方向、凝聚社区的底层机制。保护这种机制，比争论AI能不能解出下一个大猜想更紧迫。

形式化验证（formal verification）是指将数学证明翻译为计算机可检查的形式语言（如Lean、Coq、Isabelle），由 proof assistant 逐步核验每一步推理。这一过程与AI的结合已有实质进展：DeepMind的AlphaProof在2024年国际数学奥林匹克中达到银牌水平，其解法即在Lean中完成形式化。形式化验证的优点是提供可靠的正确性保证，且形式化库本身成为可复用的公共知识资产；局限在于形式化成本高昂，且形式化后的证明未必更“优雅”。将AI定位于形式化验证的辅助环节，正是陶哲轩所说“把审美判断留给人”的具体落点之一。