OpenAI 一夜解出 372 个数学难题
The Mathocalypse
昨天，OpenAI 一次性发布了 372 个数学领域的重大突破，其中包括困扰学界多年的 Unique Games Conjecture 证明。作为复杂性理论家 Dana Moshkovitz 的丈夫，我亲眼见证了她职业生涯的终极目标被 AI 轻易攻克。虽然这些由 AI 生成的证明目前还难以被人类完全理解，甚至被形容为“外星人”的作品，但这标志着数学研究进入了全新的时代。从 L=BPL 到黎曼猜想的进展，AI 正在以前所未有的速度解决那些曾让无数数学家皓首穷经的问题。
想象一下，一个在严酷雨林中生存了一辈子的狩猎采集者，突然旁边出现了一座拥有直升机停机坪和恒温泳池的巨型度假酒店，而他却毫不犹豫地表示：好吧，那我现在的新工作就是为游客经营荒野 retreat。
HN 评论区
227- ks2048
读起来像是个嗑了药的人写的。内容含糊不清，逻辑不通。文中堆砌了大量过往工作的名词，却未讨论为何在存在不可能性定理的情况下这些工作依然可用。
基本上，这篇论文写得如此糟糕，不借助 AI 根本无法阅读。
这挺有意思的，在所有关于此事的报道中我还没见过这种说法。
读起来肯定很痛苦——就像试图理解别人写的一堆混乱代码，尽管它还能输出正确结果一样。
- nostrademons
顺便提一句，光看第一句话就能判断这不是 AI 写的：
> 妈妈，听说你被干翻了！听说有个机器人解决了一辈子都在钻研的数学难题！OOF！
我家 8 岁的孩子说话完全就是这个调调。我完全能想象他在餐桌旁用同样的语气这么说。
我问了 ChatGPT：“假装你是今天的 8 或 9 岁小孩。你会怎么嘲讽妈妈的工作被 AI 取代？”它给出的回答是：
> “妈妈，AI 抢了你的工作，因为连机器人都说，‘是啊……我们能做得更好。’”
> “妈妈，恭喜！你被电脑取代了。连 Siri 都有工作了，你却没有！”
> “妈妈，AI 抢了你的工作？真惨。看来连机器人看了你的工作都说，‘我来搞定。’”
> “别担心，妈妈。你还是有用的……比如教 AI 怎么做我的午餐。”
除了显得相当尴尬和机械之外，这些回答都带着一股千禧一代的调调。相信孩子们和语言演变才是最好的 AI 检测器。
- ajjenkins
文中关于“理解外星人”的那句话让我想起了 Ted Chiang 的短篇小说《人类科学的进化》（2000 年）。
强烈推荐一读。写于 26 年前的作品，却极具前瞻性。
https://gwern.net/doc/fiction/science-fiction/2000-chiang.pd...
- an0malous
> 但似乎目前还没有人类真正理解这些证明中的任何一个
有人验证过 OpenAI 生成的任何证明吗？还是大家都只是假设只要 Lean 代码能跑通就是对的？Lean 代码本身会不会就是写错了？
- parksb
> “OpenAI 模型”在人类之间引发了一场疯狂的竞赛，去消化和解释一个混乱的 AI 证明（这项工作很容易变成吃力不讨好、几乎得不到认可、充满竞争且毫无乐趣的活计）
可悲的是，这也正是当下许多工业界软件工程师的日常写照。我把时间都花在阅读和验证成千上万行混乱的 AI 生成代码上。与真正创造东西相比，这确实是一项吃力不讨好、几乎得不到认可且毫无乐趣的工作。
- softwaredoug
勾股定理难道不是有几十种证明吗？目标不仅仅是“证明”它，而是要创造出对普通从业者来说写得清晰、直观的东西。通过获得更深的理解，我们才能提出更好的问题。
- dualvariable
除了故事中妻子提出的那些问题外，这里还有一篇关于 Navier-Stokes 结果的元分析，对所有的这些解都提出了质疑：
https://arxiv.org/abs/2610.08144
> 自动形式化越来越多地用于验证数学文本，包括由 AI 生成的文本，例如 OpenAI 宣布的关于 Navier-Stokes 方程解爆破的证明。在这个过程中，AI 系统将自然语言（NL）文本翻译成 Lean 等形式语言。一旦完成翻译，形式语言中表达的论证就可以轻松地进行机械验证。本文旨在说明，由于语义忠实翻译过程中的各种困难，这一过程可能无法让人对原始 NL 论证产生任何信心。特别是，我们强调，解决数学 NL 文本中的歧义问题（这是提供语义忠实翻译所必需的），在可解性复杂度指数（SCI）层级/算术层级中处于任意高的位置（SCI =∞）。因此，非正式地说，提供语义忠实的 AI 自动形式化比任何计算问题都更难，包括停机问题（其 SCI =1）。为了展示这一结果的影响，我们提供了几个实际案例，说明 AI 将 NL 语句和证明翻译成 Lean 时的误译，导致 NL 证明与其 Lean `验证'之间出现不匹配。其中包括 Op […]
- furyofantares
仅仅依靠模型能力，而不是代理群（swarms of agents），就达到这种程度，这让我头晕目眩。我们要多久才能接触到这些能力？我们要多久才能本地运行类似的东西？
到时候，前沿实验室又会搞出什么怪物？
也许我反应过度了，我得先把脑子装回去，才能消化这一切。