AI 在数学中正在引发重大问题

原文 ↗ Hacker News 讨论 ↗

AI 在数学中的作用

  • AI 被视为工具、合作者，以及可能的“神谕”；许多人认为这三种角色都会并存。
  • 当前优势：加速搜索、探索案例、提出步骤、将现有想法形式化并进行验证。
  • 弱点：难以真正生成新的想法或实现大的概念性飞跃；有人认为近期 AI 的“突破”大多只是对已知技术的重新包装。
  • 几位评论者指出，和代码一样，你必须本身就在这个领域足够强，才能可靠地判断 AI 的数学输出。

验证、证明助手与信任

  • 一个核心主题：生成证明与检查证明之间的区别。
  • 证明助手（例如 Lean）一旦把命题正确形式化，就能给出非常高的可信度；“要么能编译，要么不能”。
  • 但你仍然必须信任定理陈述、公理、内核的实现，以及整个软件/硬件栈。
  • 关于“证明的证明”是否有意义存在争论；许多人强调正确性与理解是两个独立的问题。

证明的理解性与实用性

  • 大型自动生成的形式化证明（例如 20 万行 Lean）引发了问题：
    • 支持方：如果定理被形式化证明了，那就足够了；定理本身就是 API。
    • 反对方：不透明的块状内容就像没有源代码的二进制文件——很难复用、扩展或从中学习；数学的价值在于洞见、结构和方法，而不仅仅是答案。
  • 有人认为，不可理解但正确的证明在实践中仍然有用（例如密码学、工程）。也有人认为这会侵蚀数学本身的意义。

对实践与职业的影响

  • AI 也许无法解决长而复杂的证明瓶颈；除非完全形式化，否则验证仍然需要付出努力。
  • 短期内最可能的角色：作为处理琐碎工作的助手（形式化、Latex、局部重构），而不是替代人类创造力。
  • 有人担心，人类数学家会变成“神谕的祭司”，只负责解读 AI 的结果，这被一些人视为反启蒙。

哲学与社会担忧

  • 持续存在的争论：数学是被发现的还是被创造的；公理与“有趣”定理的审美选择仍然是人类的事。
  • 有些人认为有用的数学可能会超出人类的可理解范围；另一些人担心出现“技术祭司”未来，我们将依赖无法理解的系统。
  • 关于可及性与公平性的担忧：强大的模型是私有且昂贵的，可能把数学变成像实验物理那样精英化、资源密集的领域，加剧既有的不平等。