定理经济的衰落

原文 ↗ Hacker News 讨论 ↗

对这篇文章的总体反响

  • 许多评论者认为这篇文章异常深刻、论证扎实，是他们读过的关于数学本质的最有趣的内容之一。
  • 也有少数人觉得语气有些以自我为中心，或者政治上有些天真（例如“在资本主义下重新发现疏离感”），但即便是批评者通常也同意它提出了重要问题。

数学、理解与 AI

  • 反复被呼应的核心主题是：数学真正的“产物”是概念上的理解和新的思维方式，而不只是定理或形式证明。
  • 一些人担心 AI 能批量生产正确的定理和冗长的形式证明，而人类永远不会真正理解这些内容，从而在“人类数学”之上形成一层“机器数学”。
  • 讨论集中在这样一个问题上：这种仅由 AI 产生的结果，是否仍应被称为“数学”，还是更适合标记为“工程”、“神谕”输出，或“工程化的可信数学”。
  • 也有人强调，传递理解才使某件事成为科学；纯粹的 AI 对 AI 工作将缺少这一点。

纯数学的价值与目的

  • 有人认为，大多数高级纯数学实际上就是一种自洽的解谜游戏，与现实世界并无真正关联；如果 AI 能做得更好，社会也不会损失多少。
  • 另一些人反驳说，基础研究就像风险投资：大部分工作都是“无用的”，但少数抽象想法后来会改变技术（例如历史上的数论或拓扑学案例）。我们无法提前知道什么会变得重要。
  • 还有批评指出，制度奖励的是定理生产，而不是解释、重构和教学法，尽管后者可能才是许多真实价值所在。

AI 对职业与机构的影响

  • 有人担心，AI 加上大型科技公司的资金会掏空学术基础研究，把数学家变成应用型专家或 AI 工具使用者。
  • 一些人预见“定理证明”职业的前景黯淡；另一些人则认为，人类会在选择问题、引导 AI 资源和解释意义方面获得新的角色。

证明、严谨性与软件类比

  • 与编程的比较反复出现：软件依赖测试和“实战测试”，而数学坚持证明，因为替代方案是整个理论崩塌。
  • 评论者指出，数学本来就有许多非正式、有漏洞或只经过部分检查的证明；像 Lean 这样的形式系统既揭示了这一点，也提供了一条通往机器检验严谨性的路径。
  • 关于自下而上与自上而下的抽象构建方式的讨论，将数学理论构建与软件架构联系起来，不过数学实现了比典型软件生态系统更深的复用和更累积的结构。

出版、开放性与获取

  • 多个轶事描述了失调的期刊流程：多年延迟、杳无音信、邮件丢失、任意拒稿，甚至在外部介入后出现“撤销拒稿”。
  • 有些人担心 AI 优势会把科学和数学进一步推向封闭的、私营资助的孤岛；另一些人则认为，实验约束和大型协作会保留一定的开放性。