OpenAI 的 Navier–Stokes 发布包含了一个 Lean 4 形式化证明

原文 ↗ Hacker News 讨论 ↗

OpenAI 据称使用大型语言模型“agent swarms”和 Lean 4 形式化证明解决了一个 Navier–Stokes 千禧难题，这引发了敬畏与怀疑并存的反应。评论者一方面权衡这一技术成就及自动证明形式化的前景，另一方面也关注巨大的算力成本、AI 是否抄袭或过度依赖人类研究者工作的问题，以及数学是否会变成机器在做而人类却无法真正理解的事情。很多人还在探讨对 Lean 之类形式化验证工具应有多少信任、哪些 bug 或陈述误设仍可能让结果失效，以及这类否定性存在证明是否真的具有现实物理应用。

AI 与人类形式化的成本与效率

  • 讨论质疑“四个数量级”节省的说法：粗略估算显示，约 $40M 的算力成本对比约 $130M 的人力劳动，虽然仍然巨大，但差距更小。
  • 有人认为形式化中经典的“每页 40 小时”说法已过时，因为自动化和库更好了；也有人认为它对复杂的研究级材料仍然成立。
  • 协调约 100 万小时的人类努力，被认为相较于一个大型 agent swarm 在实践中几乎不可能。

Lean、自动形式化与性能

  • 许多人指出，现代 Lean + mathlib 对本科层级材料能大幅降低工作量，但深度研究证明仍需要巨大投入。
  • Lean 在这种规模下被认为很慢（例如多天、230 GB 的验证），不过几位指出 agent 生成可能是大规模并行的，而验证大概主要是在单机上完成。
  • 讨论了优化 Lean 的 kernel，并证明其优化版本与简单版本等价；还提到了在 Lean 中重新实现 Lean 的项目，作为一条路径。

验证、信任与可能的 bug

  • 共识是：如果公理和定理陈述正确，一个经过检查的 Lean 证明就非常可信；主要风险在于把陈述形式化错了，而不是内部证明步骤。
  • 有人指出 Lean 过去曾有过 kernel bug；AI 理论上可能利用这种 bug，而不是真正证明定理。
  • 对“对抗性”形式化的担忧在于，它们可能会微妙地更改定义；检查定理陈述和假设仍然是人类的责任。

伦理、抄袭与数据使用

  • 有一个很大的分支在争论 AI 的关键想法是否“抄袭”了使用更早模型的研究者，尤其是通过训练私聊数据。
  • 一方认为，时间线和问题变体表明 AI 解决了更难的情形，而近期的私下工作不可能已经进入训练过程。
  • 另一方认为，数据匿名化和混合使得“不可能知道”模型受到了什么影响；对实验室伦理的不信任加剧了这种怀疑。

意义、理解与价值

  • 有些人惊叹于一个通用模型既能求解又能形式化验证这样的问题；也有人担心，这个结果只是“一个比特的信息”，缺少相应的人类理解。
  • 还有批评认为，大型 AI 实验室追逐的是头条，而不是深层的数学阐释，而且它们不会回答后续问题，也没有与更广泛的数学界整合。

Navier–Stokes 结果的实际影响

  • 关于现实世界相关性的争论：有些人认为这个负结果主要表明 Navier–Stokes 只是一个不完美的物理模型；也有人认为其直接应用有限。
  • 将其与纯数学中悖论式或高度人为构造的例子进行比较；怀疑这种奇点对工程或湍流建模并不重要。

关于 AI 与数学的更广泛反思

  • 情绪复杂：既为自动形式化以及未来在 abc 猜想等问题上的工作感到兴奋，也担心人类数学创造力正在被“机械化”。
  • 担心未来会出现人类无法在可行范围内、无需巨大算力就检查的 AI 生成证明，以及对形式化验证工具链的潜在攻击。