精华速览

数学家陶哲轩在加州理工学院演讲中提出「数学2.0」概念，认为AI正让数学研究从「证明稀缺」走向「证明富足」，但得到正确证明不等于理解证明为何成立。他主张用AI寻找更易理解的证明、整理分散成果并系统分析大量问题，例如等式理论项目已对超2200万个命题作出判定。他同时呼吁公开AI解题的计算资源消耗与失败尝试，强调未来数学研究需兼顾AI扩展探索范围与人类对证明及现实应用的理解判断。

要点透视

  • 陶哲轩于10月11日公开在加州理工学院的演讲《数学2.0》，提出AI正降低部分数学问题求解成本，使数学研究从「证明稀缺」转向「证明富足」。
  • 陶哲轩指出，多数前沿数学问题仍未解决，不能仅凭公开传播的成功案例判断AI整体能力；得到正确证明不等于研究者理解证明成立的原因或掌握可迁移的新方法。
  • 等式理论项目通过人类与自动化工具协作，已对超过2200万个命题作出判定，被视为AI辅助数学系统分析的案例。
  • 陶哲轩呼吁公开AI解题的计算资源消耗、失败尝试等信息，以便更准确评估AI能力边界。
  • 他主张AI应帮助寻找更易理解的证明、整理分散研究成果，并保留人类对证明及其现实应用的理解和判断。

文章拆解

陶哲轩的「数学2.0」提法，核心不是宣告AI已经能替代数学家，而是重新划分人与AI在数学研究中的分工。过去数学研究的瓶颈之一在于证明的产出速度，一个前沿问题可能耗费数年甚至数十年；AI的介入让部分问题的求解成本显著下降，于是「证明富足」成为可能。但陶哲轩特别提醒，证明的数量增加并不自动带来理解。一个由AI生成的正确证明，可能像黑箱一样只给出结论，却无法告诉研究者为什么这个结论成立、能否迁移到其他问题。这正是他主张AI寻找「更易理解的证明」的原因。

从行业影响看，这一判断对当前AI for Science的叙事有纠偏意义。等式理论项目对2200多万个命题作出判定，说明AI在系统性、规模化分析上确有优势，但这类成果更多是「判定」而非「洞察」。如果研究界只以解题数量或竞赛成绩衡量AI能力，容易高估其真实水平。陶哲轩呼吁公开计算资源消耗和失败尝试，实际上是在要求一套更透明的评估标准——成功案例往往被放大，而失败和成本被隐藏，这会扭曲对AI能力的判断。

对数学研究者而言，数学2.0意味着工具链和协作方式的变化：AI可以承担文献整理、猜想生成、反例搜索等重复性工作，人类则聚焦于提出好问题、理解证明结构和判断现实应用。潜在风险在于，如果年轻研究者过度依赖AI给出的证明路径，可能弱化独立推导和批判性思维。另一个尚待确认的变量是，AI生成的证明能否被形式化验证系统高效检验，以及这种协作模式在纯数学前沿领域能否规模化。陶哲轩的立场是审慎乐观：利用AI扩展探索范围，但不放弃人类对证明的理解与判断。

查看原文