## 人工智能在数学中的角色：迷思与现实，Terence Tao 抽身而退

数学界已沸腾数周。耸人听闻的头条宣称人工智能已攻克数十年来无法解决的问题，助长了关于数学家即将被淘汰的理论。但必须有人打破这种夸大的叙事，而这个人正是人工智能与数学交叉领域最热情的研究者之一：Terence Tao。

在一场体现紧迫感的早起行动中，Tao 更新了他在 GitHub 上的文档，批判性地质疑了人们对人工智能成就的解读。他的信息直截了当：不要把“产生可验证结果”与“精通数学”混为一谈。这个区别至关重要，但常被忽视。

### 断章取义的解读问题

当人工智能解决 Erdős 问题时，存在一种自然的倾向——夸大其成。然而，Tao 指出，这种简化的视角掩盖了根本的复杂性。首先，Erdős 的问题在难度上并不等同。有些代表极端挑战，而另一些则是“低悬的果实”，用现有工具可以相对轻松解决。仅以“已解决问题的数量”来衡量，而不考虑其复杂性，就像用数字而非背景来衡量成就一样。

还有一个关键因素：许多在公共平台标记为“未解决”的问题，缺乏详尽的文献审查。当人工智能“解决”其中之一时，常常会发现早已有解决方案藏于科学资料的某个角落。“首次由AI发现”的叙事在审查下崩塌。

### 由可见性偏差造成的场景

公共记录主要捕捉成功案例。失败、无进展的尝试、探索的死胡同都未被记录。这种信息的不对称不可避免地扭曲了我们对实际能力的认知。

此外，Tao 在分析如何在 Lean 等助手中形式化证明时，发现了微妙的陷阱：引入额外的公理、误解的陈述、利用数学库的特殊行为。一份形式验证的证明并不总意味着其概念上的有效性。

### 超越正确答案

Tao 在这里触及了数学家的核心意义。数学中的“证明”不仅仅是提供一个可验证的答案，而是将答案嵌入更广泛的知识网络中。人类的证明通常包含背景、历史动机、与前人工作的比较、方法的范围与局限。

相比之下，人工智能主导的证明常常缺乏这种“意义的光环”。它们在技术上正确，但在认识论上对接受者来说贫乏。

### 人工智能真正的作用

Tao 对其评估持谨慎但公正的态度。人工智能作为工具表现出色：文献检索、论证重写、现有证明的形式化、自动审查、流程跟踪。在具体案例中，比如#728 y el #729的问题，早在2026年1月初，Lean 中就已获得完整验证的解决方案，证明在某些细分领域，AI 确实可以生成“可执行的证明结构”。

但这并不等同于全面的数学能力。AI 不是数学家；它是工具链中的一个复杂组成部分。

### 无崇拜的未来

未来的数学很可能不再是孤独思想家的作品，而是由指挥者调度的合成智能军队。人类提出深刻的问题，建立新颖的概念，洞察重要的联系。AI 则挖掘、形式化、验证、加速。

Tao 的呼吁是追求平衡：既不妖魔化，也不神化。要认识到AI的变革潜力，但避免陷入由孤例推动的神话，不让夸张取代严谨分析。