当人工智能解决数学问题时：特伦斯·陶抑制了热情(但不否认进步)

近年来，关于“AI解决数十年来未解数学问题”的耸人听闻的标题层出不穷。一方面激发了等待AGI的希望，另一方面也让担心人类智慧衰退的人感到担忧。在这种叙事升级中，反常的是，数学研究的主要支持者之一、由AI增强的数学研究的倡导者特伦斯·陶（Terence Tao）决定出面发声，将讨论拉回到现实。

陶的谨慎：并非所有已解决的问题都同等重要

在他关于数学与人工智能关系的GitHub声明中，陶并不否认AI的进步，但他拆解了“可验证结果=高级自主数学能力”这一简单等式。问题的核心在于？不是统计AI解决了多少问题，而是要理解哪些问题被解决，以及这些解决方案在科学上的意义。

埃尔德什（Erdős）的问题范围极为广泛。除了学科中的未解杰作外，还存在许多被社区少关注的“长尾问题”：正是这些领域，现有工具表现出色。没有专业的文献审查，很难区分低水平的“果实”与真正的杰作。

“发现”早已存在于文献中

另一个混淆点在于：许多被标记为“Open”的问题没有经过系统的文献验证。当AI给出一个解决方案时，常常会发现——令人惊讶的是——有人早已提出了类似或等价的答案。这使得一些颂扬的标题变得脆弱且不稳定。

陶还强调了一个关键的方法偏差：公众主要关注成功案例。AI的失败、未完成的尝试、没有后续发展的实验都在官方记录中不可见。这种片面的视角系统性地扭曲了对现实的认知。

人类数学的隐藏价值

这里揭示了最深层的哲学问题。解决一个问题并不等于其数学意义的全部：重要的是，这个解决方案如何融入更广泛的知识体系，揭示了哪些联系，如何照亮可迁移到其他领域的方法。

由AI生成的证明，即使在形式上正确（如在Lean等语言中翻译后），也常常缺乏这种“认知氛围”。缺少背景、动机、与前人文献的批判性对比、方法的局限性。技术上无可挑剔，但在集体知识进步方面实际上有限。

此外，在Lean的形式化过程中，偷偷引入额外的公理、误解原始问题的陈述，或利用数学库的边缘行为也很常见。异常简短或过于冗长的证明都需要特别审查。

AI在发现链中的真实角色

浏览陶关于人工智能与数学关系的文档，可以看到一个多样化的图景：AI在多方面做出贡献。生成完整或部分的解决方案。识别之前缺失的文献。形式化已有的证明。重写论证以提高清晰度。执行高级文献检索。

一些问题由机器完全解决，比如(如#728 e il #729，经过形式验证)，但后来发现早已有人提出。这不否认技术上的贡献，但可以理解为对科学意义的补充。

人类仍是领航者，AI是工具

如果走向极端——认为AI在数学中毫无用处——也是错误的。更平衡的说法是：AI在数学的执行性和工程性工作中表现出色。它遵循模式。弥补技术差距。精确形式化。挖掘文献。优雅地重写。

但数学的深层精神——提出突破性问题、发明革命性概念、编织意义网络——仍然牢牢掌握在人类手中。

也许未来的数学家不再是浪漫传统中的孤独思想家，而是由一支硅智军队组成的领袖：人类规划路线，AI开辟道路、构建基础设施。数学与人工智能的关系不是冲突，而是有意识的协同，其中角色的明确划分对于最大化双方潜力至关重要。