数学末日

AI 结果的性质

• 许多人认为这项工作是“统计驱动的蛮力搜索”，能得到正确答案却几乎没有理解；也有人认为这仍然是实质性进展，就像进化的蛮力搜索产生了生物学一样。
• 打破长期存在的复杂性壁垒（例如把指数稍微削减一点）被辩护为重要，因为它否定了最优性猜想，哪怕改进在数值上看起来很小。
• 一些评论者强调，在几个小时的计算后解决大约 8,000 个困难问题中的约 5% 已经非常惊人，而且按每个结果计算经济成本很低。

可理解性与验证

• 多份报告称，许多论文写得很糟、晦涩难懂，给人的感觉像“迷幻”或“乱糟糟的代码”式数学：逻辑密度很高、表达很差、过度堆砌术语，且对已有工作如何使用说得不清楚。
• Lean 证明被广泛引用为形式化陈述正确的证据，但：
  • 自动形式化可能会把自然语言证明错误地翻译成 Lean。
  • 另一篇论文论证了这种翻译在原理上极其困难，并展示了具体的不一致之处（包括 Navier–Stokes 结果）。
  • 有人提出 Lean 可能存在漏洞或类似利用攻击的行为，不过也有人说已知的健全性漏洞都很冷门。
• 人们援引计算机辅助的四色定理等先例：即使缺少人类可理解的证明，正确性也可以被接受，但许多人仍然希望之后出现更简单的证明。

对数学与职业生涯的影响

• 博士生和年轻研究者出现强烈焦虑：担心技能和问题正在被自动化取代，并且 AI 创造了不公平的竞争环境（封闭的内部模型“截胡”了多年工作）。
• 也有人认为数学从来就不是主要为了收集定理；真正的价值在于新概念和新工具。人类可以：
  • 提炼并解释 AI 证明。
  • 提取新技术。
  • 判断哪些问题和想法真正有趣。
• 有些人认为我们将需要 更多 数学家来解释、组织并在 AI 输出之上继续构建；另一些人则预计资金和激励会转向人类之外。

信任、所有权与激励

• 对封闭实验室存在深度不信任：人们质疑证明的来源、用户想法是否可能被挪用，以及公关/IPO 动机。
• 建议包括：延迟使用内部模型去截胡外部研究者；更早分享工具；或者把“翻译和解释”视为一个应当获得署名的新职业角色。
• 争论的焦点还包括：是否可以用数百篇难以阅读的预印本把领域淹没；有些人支持开放发布而不是传统同行评审，另一些人则称这是一种不负责任的“垃圾内容”。

与编码和工具的类比

• 许多人将其类比为生成式 AI 代码：AI 产出庞大、难读的“PR”，技术上能工作，但需要繁琐的人类审查。
• 类似的担忧包括：缺乏清晰抽象、难以在杂乱产物上建立理解层级，以及从创造转向审计。

对未来 AI 进展的预期

• 乐观者认为模型很快也会生成优雅、适合人类尺度的解释；怀疑者则把这种信心比作过去被过度炒作的技术（加密货币、完全自动驾驶）。
• 也有人认为，随着系统超越人类认知极限，许多情况下完全符合人类可读性的证明可能会变得不可能，因此分层验证和“可观测性工具”会比直接理解更重要。