← #804

数学与理论计算机科学中的十项进展

文章摘要

这是 OpenAI 在 2026 年 8 月 1 日发布的一份成果公告。开篇的定位是「赋能科学家与数学家、加速发现」，并提到他们此前宣布的 ChatGPT for Academic Researchers 计划——为 10 万名科学家和数学家提供免费使用其最好模型的机会——以及持续在开发过程中用开放研究问题评估模型的做法。

作为背景，他们提到今年 5 月曾分享过一个由 AI 生成的、对 Erdős 单位距离猜想的反证，那是在评估一个尚未发布的模型时发现的，并称该工作已经启发了数学和理论计算机科学的后续进展。而这次公布的是十项结果，每一项都解决了或在一个长期开放问题上取得了实质性进展，覆盖高维几何、编码理论、算术电路复杂性、群论、算子代数、量子复杂性、格密码学和极值组合学。

十项结果分别是：

高维球堆积：将球堆积密度的上界改进到 Cohn–Elkies 阈值。
二元码与球面码：在任意给定最小距离下，对二元码最大规模的界给出指数级改进，并对高维球面码给出类似结果。
非 sofic 群：给出一个构造，确立非 sofic 群的存在性，解决群论中的一个核心开放问题。
Connes 刚性猜想：反证了「某些群由其冯·诺依曼代数唯一决定」这一长期猜想。
算术电路复杂性：对用算术电路和公式计算 permanent 给出新的下界，其中算术公式的下界达到 n⁴/log n 量级。
量子并行重复：对一般的两人量子博弈给出指数级并行重复定理，把经典复杂性理论中的一条基础原理推广了过去。
最近向量问题：给出最近向量问题（CVP）近似的多项式因子难度，这是与后量子密码学相关的一个基础格问题。
Ehrhart 体积猜想：在每个维度上确定了「以其重心为唯一内部格点的凸体」的最大可能体积。
多色 Ramsey 数：给出多色三角形 Ramsey 数的超指数下界，解决 Erdős 第 183 号问题。
极值数猜想：在极值图论中的紧致性猜想和退化性猜想上取得结果，解决 Erdős 第 146 号和第 180 号问题。

关于方法与成本。 OpenAI 说明这些结果是由 Astra（他们的下一个主要模型）的一个内部版本取得的。文中给出了一个被后续讨论反复引用的数字：按 Sol API 的价格计算，找到这些问题解答所需的 token 总量成本大约为 2000 美元。这些论证随后由人类（使用同一模型）整理成手稿，之后模型将每个论证在 Lean 中形式化为证书。他们同时为每个解答发布了模型对自身思考过程的叙述（reasoning walkthroughs）。

关于对数学共同体的责任。 文章有专门一节讨论署名与责任问题，其中被引用最多的一句是：为一个完全由 AI 系统生成的证明主张人类作者身份，会同时错误地表述该系统的贡献和真正的人类智力工作的性质；他们表示自己帮助准备了手稿并在 Lean 中形式化了证明，并对其正确性负责。

HN 评论精华

这条帖子拿到了 627 分，是本期讨论量最大的一条。讨论大致分成几股：数学家职业前途的焦虑（以及围绕「和国际象棋类比」的激烈争吵）、对方法论透明度的质疑、对 Lean 形式化到底保证了什么的技术澄清，以及关于成本核算方式的争论。

piker 开了最大的一条串。他不认为数学家的存在性焦虑是对的：这些结果反而把数学带向了主流，他个人很期待人类数学家对这些结果意义的解读与讨论。他承认主要是超级明星从关注度中获益、不那么有名的人分享不到这份荣耀，但另一方面这是个令人兴奋的时代——每一个被攻破的猜想都会打开七八个新想法，而我们穿过这些组合的路径将由有创造力、有好奇心的人类数学家决定。（他原本做了一个与国际象棋的类比，后来因为引发争议而删掉了。）
traes 是这条串里最激烈也最有信息量的反对者，他的反驳集中在「别再拿国际象棋类比」上：国际象棋是一项主要靠少数几个古怪亿万富翁资助的观赏性运动，选手在限时环境里人为地约束自己，明知永远下不出比一部智能手机更好的着法，只因为少数人觉得有意思；真正靠下棋赚到足以支撑职业生涯的顶级职业选手只有约 30 人，也许再多几百人能靠教棋维持清贫的生活。「我不敢想象如果数学走上国际象棋这条路，那成千上万不具备菲尔兹奖级别水准的数学家会怎么样。」anematode（既爱下棋又从事棋类引擎工作）完全赞同：这些与国际象棋的类比该停止了。jibal 从另一个角度补充：如果你只是想知道某个棋局问题的答案，交给引擎就行；国际象棋之所以延续，是因为它是人与人之间检验技艺的竞赛（就像自行车、汽车、火车没有消灭赛跑），计算机基本被排除在外——把这一点翻译到数学上，你得到的是数学竞赛，而不是作为职业的数学。traes 还指出了另一处不对称：从来没有人像今天付钱让人解数学题、写代码那样，付钱让人去找出好的棋着。
baq 给出了一个更中性的框架：在国际象棋、围棋以及过去一年的编程上，人分成两类——失落的和兴奋的。失落的人为自己失去优势、为磨砺多年的手艺迅速贬值而难过；兴奋的人则为未来、为计算机能给自己领域带来什么以及它将如何演化而激动。他说自己在编程上两者兼有，兴奋多于失落，但对这一切的节奏感到不止一点恐惧——他想这大概就是当年 Kasparov 的感受、Lee Sedol 的感受，以及现在陶哲轩的感受。
energy123 提出了一个被广泛认同的具体损失：建立职业可信度的旧方式正在被摧毁。曾经足以定义一个人职业生涯的成就，现在很难与 AI 的产出区分开，而且更多地与算力获取相关——「想想比尔·盖茨大学时写的那篇数学论文，那种作为可信度路径的东西现在没有了。」他补充说这对拥有 2025 年前可信成就的老人反而是一种竞争优势。traes 顺着追问：如果有天赋的人和有算力的无天赋者的成就无法区分，那还有必要去尝试吗？FranzFerdiNaN 给了一个部分的答案：有知识的人能确认 AI 产出是否正确——我能让 ChatGPT 就某个开放问题给出一个结果，但我完全没有办法验证它的正确性；这是不那么有趣的工作，而且你大概需要先亲手做完那些苦活才能发展出验证 AI 结果所需的技能和直觉，所以你不可能把一切外包给 AI 而不损失能力。
dash2 提出了一个尖锐的视角转换：整个看待方式很奇怪——数学存在的目的是为了娱乐和雇佣数学家吗？数学不是有用的东西吗？如果是，那数学家感觉如何在很大程度上是无关的，就像因为铁路可能让驿站客栈倒闭而抱怨铁路。MinimalAction 强烈反对：完全不一样，人需要工作来获得收入，我不相信从中获利的人会与世界分享；权力全部集中在少数几只手上，由它们决定其余人是否能得到任何形式的收入。争论一路升级到「对全人类的数学进步收益是否超过研究数学家失去的工作」这种表述上。
aabhay 提出了整场讨论中最被反复引用的方法论质疑：他的主要不满是整个实验和构造缺乏透明度。他怀疑他们不是简单地把模型指向这十个特定问题、给一次机会就完事，因此那个 2000 美元的数字可能完全具有误导性，类似于不披露完整实验设置的 p 值操纵。他想知道三件事：总共给了模型多少个问题，有多少在花掉多少成本后未能解决就放弃了？每个问题给了模型多少次尝试机会？这套 harness 有多贵，比如模型是否能访问一个作业集群？vector_spaces 把这个论点推进了一步：如果模型真的这么强，那么保持透明会轻易支撑这些主张、打消这些顾虑；说「AI 反证了一个长期猜想」当然比说「它做到了，而且花了该领域几位博士专家若干次尝试才写出能让模型吐出有用东西的提示词、若干轮迭代优化配置和提示词、若干次试验才解出来，全部加起来超过一个典型数学学者一辈子能挣的钱」更激动人心——但不透明本身就在邀请怀疑和犬儒的解读。uh_uh 则从另一侧开火：有些人就是无法接受 AI 真的交付了成果，正在用一切办法抹黑它。
成本争论独立成了一条长串。emil-lp 问的是总成本（包括数学家和工程师的薪水）。z7 引用了 OpenAI 研究员的推文重申「全部 10 项突破的证明生成成本按 Sol API 价格不到 2000 美元」，traes 立刻指出那显然只是 token 成本，并没有回答问题。kingstnap 认为把薪水算进去是荒谬的会计方式：现实的总成本应该是「写提示词的工时 + 检查结果的工时 + API 费用」，你不会把所有参与的工程师和数学家的年度总薪酬加起来扔进总成本；真正该做的比较，是一位大学研究者在「招一个研究生（数万美元）」和「敲一段提示词、向 OpenAI 发一个推理请求（文中提到的约 2000 美元 API 费用加几小时写提示词和 harness）」之间的权衡。emil-lp 解释了自己为什么在意：假如 Erdős 单位距离猜想那个证明的总成本原来是 5000 万美元，那问题就变成——这些模型确实能证明重要的数学结果，但代价极高，值得吗？如果一位数学家申请 5000 万美元的研究经费去证明同一件事，他会被银行笑出门；而且研究经费还会培养博士生和博士后、雇佣新人、扩散知识，也就是同样的钱能带来多得多的价值。dist-epoch 反过来说：就算这 10 个问题花了 100 万美元，那也不过是 10—20 名数学研究者一年的开销，你真的认为把这笔钱付给人类他们会交付同样的结果吗？mungaihaha 回击说「没有报酬的研究生每天都在解这种问题」，这句话引来了一连串要求举证的回复：gbnwl 问过去 10 天里有哪 10 个这种级别的问题是数学研究生解决的？r0uv3n 更具体地说，研究生不会每天解决像非 sofic 群存在性这样的问题。
Lean 到底保证了什么是本帖信息密度最高的一条技术分支。danielrmay 觉得「我们对其正确性负责」这句话有点好笑：为一个用 Lean 写的证明的正确性负责，感觉像是自愿在有人发现基本算术有缺陷时当替罪羊。emil-lp 澄清说，责任不是针对「Lean 证明内部」，而是针对从「人类语言的数学」到「形式化 Lean 变体」的翻译。traes 补充说他理解在 Lean 证明里有若干「作弊」的方式（比如 sorry 之类），OpenAI 是在为「彻底核实没有使用这些作弊手段，且定理陈述本身被正确形式化」负责。rencrisa 把这一点讲得最完整：很多人误解了 Lean 提供的保证——有能通过检查的 Lean 证明，并不意味着我们真正关心的那个定理成立；即便忽略 Lean 内核 bug，最终仍必须由人（不是 agent）去核实那些被 Lean 编码的定理陈述（规格）确实正确地编码了真实的定理。对这种量级的非平凡定理来说，这是一项艰巨且棘手的工作，一点小错误就可能是致命的；AI 生成的 Lean 编码定理可能非常庞大且难以理解——他想知道是否有信誉良好的人审计过这些规格。DroneBetter 提到上周有人通过一个 LLM 把自己和使用者都骗过、以为找到了非构造性的 Collatz 非平凡循环存在性证明，从而发现了 Lean 内核的一个 bug；traes 对这个说法的传播提出了相当克制的核查，指出目前能确认的只是「一位数学家给出了经 Lean 验证的 Collatz 反例，证明了内核存在 bug；他声称 LLM 有参与但拒绝说明如何参与；他承认在把反例发到仓库之前就已知道这个 bug」，认为即便不算玩笑，也被严重耸动化了。
simonw 提供了后续材料：Lean 形式化的 GitHub 仓库在帖子发出几小时后放出（openai/ten-proofs），同时链接了一篇由 LLM 撰写、基于未公开推理轨迹「重构证明是如何拼起来的」的论文。他补了一句：「不过我真希望他们把提示词也发出来。」
robinhouston 给出了一条很值得玩味的元观察：从某种意义上说，这件事最了不起的地方在于它甚至没有排在 HN 首页最上面——即便这比我们以前见过的更进一步，我们也不再因为「AI 能在数学和计算机科学上取得重大进展」这个想法而感到震惊。bryan0 补充了另一条元观察：这条新闻两天前曾被适度 flag 并触发了 HN 的骂战检测器，因而没能上首页——「我觉得人们在理性处理这条信息上有困难。」他问：我们能做什么让围绕这类既激动人心又重要的话题的讨论更有建设性？
kcexn 提出了一个非专家但很关键的问题：这些证明是否为数学语料贡献了新的思想，还是只是一种高效地穷举检索文献、找到现有工具正确组合的方法？换句话说，这些问题此前是否本来就有直觉上的答案、也可行，只是价值不够高到值得专家投入时间？还是说它们在此之前是根本性困难的，而 AI 做到的确实超出了「把问题扔进一个大求解器」？
plaidfuji 给出了一个偏冷静的技术框架：任何可计算的问题最终都会落入计算机手中。LLM 让数学证明变得更可计算了——计算机可以自己生成候选解并检验其有效性，且有合理的概率收敛到正确的东西；这与分子动力学、蛋白质折叠、有限元模拟类似，一些原本不可行的问题变得可行了，但绝大多数其他问题仍然无法被这些计算技术解决。他补了一个检验：如果这些东西真如宣传或恐惧的那样具有革命性，你应该立刻把它们指向价值最高的数学问题看进展——比如千禧年大奖难题，而我们还没看到解答。
另有几条代表了不同情绪：Chance-Device 认为 AI 的影响已经无可否认，「移动球门柱」的余地不多了，下一步只能把球门搬出体育场；sothatsit 关心的是「指数还会吞掉什么」——写作一直比较顽固，但他注意到 Fable 在这方面是一次不小的跃升，那么政治呢？生物学这类依赖实验的领域呢？kypro 走得最远，认为这是 AI 在数学和计算机科学问题上能力加速的又一证据，暗示我们正接近能把 AI 用于 AI 研究本身的临界点，并给出了一个相当激进的判断（他自称「对着云朵大喊的疯子」）：递归自我改进已经很近，而我们连最基本的 AI 安全问题都还没解决。ultimatefan1 则给出了相反方向的推理：过去关于 AI 起飞的一个早期前提是，能解决高等数学开放问题的系统也会发现直接解锁大幅软件性能提升的新进展；但他现在觉得这种显式联系比以前更不可能——当顶级科技公司雇数学博士时，通常让他们停下纯数学研究转做软件工程，而他们擅长软件工程并不是因为学术数学的新发现，而是因为通用智能；对他而言这是模型在变好的证据，但不让他觉得我们正处于由前沿数学革命驱动的快速起飞边缘。
zkmon 从署名问题切入反驳 OpenAI 的表述：AI 没有自我意识，它是工具。当你用螺丝刀装家具时，扭矩与金属内部的分子力相互作用，通过巧妙的几何设计奇迹般地把力传递给螺丝——你会把这次组装归功于工具吗？「系统的贡献」是由一路向下直到芯片、数据中心和发电的许多东西共同支撑的；如果作者身份要归给工具，那就该一路归到底。
macleginn 提了个刺人的小问题：我对这个无名内部 AI 的能力深感佩服，但为什么任何地方都没列出一位人类贡献者的名字？至少有人给这个模型冲过咖啡吧？
amazingamazing 代表了一种更朴素的不满：等不及要看这些东西给普通人带来生活质量的提升了——到目前为止我看到的只是 AI 让拥有一台电脑变得更贵、让一些工作变得多余、增加了垃圾信息和对内容真实性的不信任，当然还让一些美国人变得非常富有。christofosho 也希望这些公司把更多时间和金钱投入现实世界的问题：气候、粮食不安全、污染，以及真正提升人们生活质量的技术。