分享数学中的 AI 进展

原文 ↗ Hacker News 讨论 ↗

OpenAI 发布了数百项 AI 生成的数学结果，包括据称证明了诸如 Unique Games Conjecture、“准黎曼猜想”以及低于 n·log n 的整数乘法和 FFT 算法等重大开放问题。评论者认为这代表了在形式化、可验证领域中具有历史意义的进展，并且得益于强大的内部模型和 Lean 等工具；但他们也对这些工作的正确性、缺乏完整人工审查，以及大多数数学家无法接触到的专有系统使用方式存在尖锐分歧。许多人担心著名开放问题被“掠夺式挖掘”、人类研究者和博士生未来的角色与动力，以及科学权力进一步集中到少数 AI 实验室手中；与此同时，也有人欢迎一个自动定理证明与 AI 辅助科学的新时代。

对 OpenAI 数学“倾倒式发布”的总体反应

  • 许多人认为这具有历史意义，并带有“未来感”：据称几十个长期存在的开放问题被解决，往往被视为具有“菲尔兹奖级别”的意义。
  • 也有人感到悲伤或不安，尤其是那些花了多年研究特定猜想、如今却似乎被一个内部模型解决的人。
  • 有人称之为营销式的“垃圾倾倒”；也有人认为这是 AI 驱动发现的一个非凡概念验证。

这些声称结果的重要性

  • 经常被提及的亮点包括：
    • 将 Unique Games Conjecture 提升为“Theorem”，对近似困难性有重大影响。
    • 一个“Quasi-Riemann Hypothesis”以及消除 Siegel 零点，被数论学家描述为该领域百年来最重大的成果之一。
    • 整数乘法和 FFT 低于 (n \log n)（非常“银河级”，但在概念上令人震惊）。
    • 矩阵乘法指数 ≤ 2.25。
    • 在精细粒度复杂性、调度、图论（例如 Barnette’s conjecture）、数学物理以及自旋系统中的各种结果。
  • 在物理学方面，评论者表示这些大多是对许多物理学家早已相信的结果给出的严格证明，短期内几乎没有实验应用。

验证、Lean 与“AI 垃圾”

  • 一些结果已有 Lean 形式化；另一些只有非正式写法或部分形式化。
  • 许多人强调，Lean 只能验证被正确编码的命题；把正确的定理形式化仍然很难。
  • 怀疑者预计会有多处错误，并担心未经充分审查的“LLM 论文”淹没数学界；乐观者则回应说，数学中出现错误很正常，而 Lean 大大提高了正确性门槛。

对数学家、学生与这一职业的影响

  • 博士生普遍感到深深不安，因为他们的论文方向或开放问题可能已经过时；有人把这比作被“抢先发表”，但规模更大、影响更结构化。
  • 有些人预测会发生转变：人类数学家将更多成为问题提出者、解释者和验证者，而非主要求解者；博士答辩会变成对理解的考核，而不是新颖性的考核。
  • 也有人担心动力被削弱：如果 AI 解决了旗舰级问题，人类发现和地位还剩下什么？

专有模型、顾问组与“把关”争论

  • 顾问组曾明确敦促实验室不要在闭源模型上测试高级问题，认为这会用只有少数人能访问的工具掠夺共享的开放问题。
  • 有人认为 OpenAI 的做法无视了这一建议，只是给出结果，却没有提供有意义的模型访问、数据集或详细方法。
  • 一方认为数学家是在“把关”以保护自己的工作；另一方则表示，真正的把关来自集中在少数公司的专有 AI。

AI 风险、权力与未来轨迹

  • 一些评论者把这视为接近 AGI 或递归自我改进的强有力证据，并预测它会迅速扩展到物理、生命科学和应用领域。
  • 另一些人认为，这些突破仅限于严格可验证的形式化领域；在混乱的现实任务（政治、机器人、对安全关键控制）上的表现仍然要弱得多。
  • 更广泛的担忧集中在权力集中（国家和企业）、潜在武器化（网络、 生物）、以及一个人类在智力上被边缘化或沦为“生物奖杯”的未来。
  • 少数人总体上持乐观态度，认为这将带来一个即将到来的“发现黄金时代”，并主张危害更多来自资本主义和治理，而不是数学能力本身。