伴随10大难题而来的62页失败记录
OpenAI Astra发布了解决10个数学与理论计算机科学难题的成果，并同步公开了一份整理失败尝试的62页文档。本文梳理了四种失败类型及该成果的实际有效范围。
AI与科技一份只记录失败尝试的62页文档同步公开
8月1日，OpenAI宣布其下一代模型Astra的内部版本解决了数学与理论计算机科学领域的10个难题。韩国国内报道关注的金额约为289万韩元。这是将OpenAI寻找解法所消耗的Token按Sol API费率换算出的约2,000美元折算成韩元后的数值，并不意味着包括模型研发与人工审查在内的总研究费用只有这些。
然而当天上传的文档并非只有一份。除了一篇梳理成果的249页论文、一个供机器验证的形式化证明代码库之外，还有一份长达62页的文档。标题为《How the Ideas Came Together》（思路是如何汇聚的）。
读者，打开这份文档会发现有些奇特。因为里面鲜少谈及正确答案，取而代之的，是通篇都在解释“为什么这种思路行不通”。
在这次发布中，真正具有突破性的并非AI找到了答案这一事实，而是他们将探寻答案过程中摒弃的所有思路单独整理成文档并予以公开。
首先，来看看这 10 个问题究竟是什么
没必要全部弄懂。只要大致感受一下它们属于哪类问题就足够了。
| # | 问题 | 通俗地说 |
|---|---|---|
| 1 | 高维球堆积 | 把球紧密堆积时，最多能填满多大空间 |
| 2 | 二进制与球面码 | 最多能构造出多少个具有容错能力的编码 |
| 3 | 非索菲克群 | 是否存在无法用有限置换来模拟的无限对称结构 |
| 4 | 康尼斯刚性猜想 | 能否仅凭一个结构的“影子”就将其复原 |
| 5 | 算术电路复杂度 | 完成特定计算最少需要多少次乘法 |
| 6 | 量子并行重复 | 如果让同一场博弈重复进行多次，获胜概率是否会骤降 |
| 7 | 最近向量问题 | 在格中寻找最近的点究竟有多难 |
| 8 | 埃尔哈特体积猜想 | 满足特定条件的几何体所能拥有的最大体积是多少 |
| 9 | 多色拉姆齐数 | 无论用多少种颜色，最终是否总会出现同色三角形 |
| 10 | 极值图论 | 在避开特定图形的前提下，最多能连出多少条线 |
第 3 题和第 4 题分别是从 1999 年和 20 世纪 80 年代起悬而未决的未解问题，而第 9 题和第 10 题则是埃尔德什留下的问题清单中的第 183 题、第 146 题和第 180 题。答案的形式也各不相同：有的给出了全新的证明，有的则给出了推翻长久以来被认为成立之猜想的反例。
cdn.openai.com这里顺便指出一个小细节。OpenAI 将成果算作 10 项，但其演练文档（walkthrough）却有 12 个章节。因为第 5 题被拆分成了电路和公式两部分，第 10 题则被拆分成了两篇极值图论的内容。形式化证明的代码仓库同样是将 12 个终点打包归纳为 10 项成果。这倒不是什么大问题，但了解“10 项”这个数字并非自然天成、而是经过编辑归并的单位，还是很有帮助的。
演练过程究竟展示了什么
在阅读这份 62 页的文档时，我统计了一下：12 个章节中有 10 个都是以失败的尝试开篇的。光看章节标题便可见一斑：“为什么第一个递推式是错的”、“漫长而有用的失败路径”、“为什么看似显而易见的归约行不通”。
失败的形式各不相同。我把它们归纳为四类。
类型 1：貌似合理的类比出了错
第 2 章，纠错码问题。
模型套用了在具有类似结构的其他问题中使用过的公式。因为形式看起来很契合。然而，它将这个公式代入了一个极小的特例中验证：长度为 8 的码。
公式给出的上限是 508 除以 7，约等于 72.6。但实际上，这样的码有 128 个。这等于指着 128 个的东西说“最多 72 个”。
这绝不能当作单纯的计算误差敷衍过去。因为上限比实际值还要小，说明计算的某处存在结构性错误。文档在这一节总结道：这指出的不是无伤大雅的归一化问题，而是结构性错误。
用修正后的公式重新计算，得出了约 261.8。比 128 大。这下合情合理了。
令人印象深刻的并不是修正了公式这一事实，而是它自主找出了能检验自己构想是否出错的极小特例并进行了代入。
类型 2：捷径破坏了目标条件本身
第 10 章，拉姆齐数问题。目标是给图着色，但不产生同色三角形。
模型想到了一条捷径。利用置换，可以用 k 种颜色构造出 k 的阶乘个点。如果有 10 种颜色，就是 360 万个点。效率极高。
但仔细核验后发现，在这种方式下，三个置换可能会将同一个位置移到三个不同的地方。而这三个置换构成的，恰恰就是一个同色三角形。它构成的结构，反而制造出了本想极力避免的东西。
类似的情况也发生在第 5 章。为了证明计算量的下界，模型给每一项都加入了修正项，但这些修正所消耗的乘法次数，偏偏等于试图通过证明省下的乘法次数。想要获得的收益被原封不动地重新耗尽，结果什么新结论也没能证明出来。
类型 3：证明了此路不通
第 1 章，球堆积问题。这里最引人入胜。
模型利用标准不等式向目标逼近，但在接近目标值一半的地方停滞不前。通常在这种情况下，人们会想：“只要把常数压得更紧一些就行了吧。”
但模型做了另一件事。它通过反例证明了：沿着这个方向根本无法达到期望的值。文档给出的诊断是：这并非未能充分优化的常数问题；仅衡量整体尺度的工具，会遗忘真正成问题的地方究竟在哪。
**它不仅仅是遇到了阻碍，而是证明了朝着那个方向根本无法达成目标。**因此，它没有继续硬抠常数，而是彻底更换了工具本身，从此进展顺利。
在实际业务中，这种差异同样意义重大。因为“还没做出来”和“这个方向行不通”，会导向截然不同的下一步行动。
类型 4：已然完成，却果断放弃
第 8 章，与格密码学相关的最近向量问题。在完整做完证明之后舍弃该路径的案例就发生在这里。
模型沿着在素数域上使用带符号直方图的路径展开探索，并且将证明完整地推导到了最后。文档明确指出，该路径提供了一个完备的构造。这意味着它是一个切实可行的证明。
然而最终稿中收录的却不是它。而是在特征为 2（即加法只剩奇偶计算的结构）中重构的版本。带符号直方图变成了奇偶表，复杂的抵消简化成了奇偶性检验。为了达到相同的结论，所需的构件少得多。
第 9 章甚至将一整节都留给了失败。那一节的标题就是“漫长而有用的失败路径”。该路径准确找到了作为答案的几何图形，却无法解释该图形体积中所带的阶乘项。也就是说，答案猜对了，却无法给出合理解释。文档将其归为失败，但也写道它依然极有价值——因为它揭示了为什么必须要有阶乘项。
同一章中还有更精彩的片段。途中模型这样写道：在这里，将两个函数视为相同的诱惑极其强烈。随后它立刻举出一个反例，阐明绝不能把这两个函数等同视之的原因，并补充说明：若真那么做了，就会基于错误的等同推导出一份伪证明。
第 12 章开篇就十分坦率。该节的第一句话就是“我们最初试图寻找证明”。而那一章最终却以一个反例收场。这意味着它在出发时，甚至连命题的真假都尚未可知。
那么这些成果，实际上究竟能应用到什么程度
我在看待成果声明时，往往会先去核实它的适用范围。因为结果究竟能在多大范围内成立，决定了它的实际意义。
韩国国内的不少报道将最近向量问题与抗量子密码联系在一起进行了报道。方向是对的。但如果看看该成果所涉及的维度，就会发现它是输入规模的401次方。401次方可能很难有直观概念，即使输入规模只有10，1后面也要跟上401个零。而全宇宙的原子总数，也就是1后面跟80个零左右。技术说明没有隐瞒这一点，而是直接写明：这一论断关乎多项式时间内的可计算性，而非实际运行效率。它并不是对目前所用密码体系的攻击。
第9项拉姆齐理论的结果也类似。新得出的下界要想具有意义，颜色数量必须达到342种以上。如果少于这个数字，以往已知的平凡下界反而更强。第5项电路下界则是在矩阵规模达到6.5万以上时才成立。
形式化验证也是如此。OpenAI表示所有成果均已在Lean1中完成形式化，不存在未竟目标，且仅使用了标准公理。这是非常有力的依据。不过代码仓库中标记的审核状态是“智能体已审查”。而且机器所验证的只是逻辑推演过程，并不是形式化命题与原始问题是否完全等价。这种对照核实仍然是人类的工作，并且目前尚未经过同行评审。
英国数学家托马斯·布卢姆（Thomas Bloom）对这次发布评价称这是“极其重磅的消息”。另一方面，陶哲轩此前就一直抱有另一种担忧：AI生成的证明正在飞速增加，而人类理解和接纳它们的速度却跟不上——也就是他所说的“证明消化不良”状态。
这两种反应并不矛盾。成果真实有效，与学术界理解并接纳它，是截然不同的两码事。6月2日国际数学联盟支持的《莱顿宣言》2所要求的也正是这一点：可验证性、来源标注，以及对谁完成了什么工作的诚实记录。
从这个角度来看，OpenAI在发布公告中写下的一句话格外值得玩味：在完全由AI生成的证明上署上人类作者的名字，是对系统贡献与人类智力劳动的双重扭曲。一家企业主动放弃本属于自己的署名权，这绝非寻常之举。
Oswarld视角
我认为这次发布中最有价值的产出，正是那份整理了失败尝试的 62 页文档。
在做 GTM（进入市场）策略项目时，我总能遇到这样一幕：最终交付物往往只有一张核心建议单页。然而在实际工作时间里，超过七成都是用来逐一排除那些没能写进那一页的候选方案。比如这个渠道为什么走不通、这种价格机制会在哪里崩盘、如果先打这个细分客群为什么会阻碍下一步的发展。
问题在于，这七成的心血并没有留在文档里。经过调研但最终放弃的方案，要么被草草塞进附录，要么干脆被直接删掉。因为在汇报会上根本没人会问起它们。于是就会发生这样的事：六个月后，另一个团队拿着一模一样的方案，当作全新的点子提了出来。整个组织不得不把早就排除过的方案从头到尾再重新推演一遍。我在很多家公司都见过这种场景，每一次也都会得出相同的结论：一个组织真正的资产，其实并非最终被采纳的方案，而是当初放弃那些方案的理由。
这次发布之所以耐人寻味，就在于它颠覆了只公开成功结果的惯例。如果只展示成功，你就无法回应外界关于“是不是碰巧蒙对”的质疑。但如果把放弃了哪些尝试、为什么放弃一并摆出来，读者便能按图索骥，看清系统究竟按照怎样的顺序做出了怎样的判断。这才是信任的基石。
还有一点。长期以来，我对那种只靠兜售成功案例的市场始终心存芥蒂。这类内容往往都是从既定结果倒推、拼凑出来的故事。而这份文档并非如此。因为被弃用的尝试被分门别类地记录在案，读者完全可以亲自去推敲那些判断是否站得住脚。我认为，这种形式理应成为未来所有宣称 AI 取得重大成果时的通用标准。
不过有一点需要明确：这份文档并非第一现场的真实思考过程记录，而是由另一个独立的 AI 模型在阅读了原始记录和最终论文后重新梳理出来的叙述。事后整理出来的故事，往往不可避免地会带上一种让过程显得比实际更加顺畅的偏见。因此，这份文档与其说是实操当下的实验笔记，不如说更接近于一份事后精心打磨的复盘。即便如此，有这样一份整理，也总比什么都没有要好得多。
结语
用三句话做个总结。
- 除了正解论文之外，团队还同时发布了一份长达 62 页的文档，专门整理了那些尝试过却最终放弃的路径。在全部 12 章中，有 10 章都是从失败的尝试切入的。
- 失败的类型主要有四种：看似合理的类比其实不成立；走捷径却破坏了目标条件本身；证明了“此路不通”；或者即便完成了证明，也依然选择了舍弃。
- 必须看清各项成果所针对的具体前提条件。最近向量问题的成果处理的是输入规模 401 次方的极高维度；而拉姆齐下界与电路下界的结论，则分别建立在颜色数量达到 342 种以上、矩阵规模达到 6.5 万以上的极端条件之下。解决问题的能力得到提升，与能否立即应用到当下的现成技术中，完全是两码事。
读完这篇文章，建议您不妨尝试做一件事：如果您这周做出了某项决定，请在最终采纳的方案旁，用两行字写下被舍弃的方案以及舍弃的理由。六个月后，正是这两行字，能为您省下一整小时的会议时间。
您所在的组织是否真的会把“经评估后不可行的理由”记录成文档？如果会，是以什么形式呈现的？如果不会，阻碍又在哪里？欢迎在评论区留言交流。如果征集到了足够多的案例，我会在下一期中整理出一套用于记录“排除路径”的实操模板。
💬 如果您有记录被废弃方案的方法，欢迎在评论区留言分享
📨 如果身边的同事正在对同一个结论进行重复评估，不妨将这篇文章转发给他们
参考资料与延伸阅读
核心来源
- OpenAI, “Ten advances in mathematics and theoretical computer science”，2026年8月1日。 链接 ··· 包含10项成果清单及关于署名权立场的原文。建议哪怕只读一下最后“对数学界的责任”这一段。
- OpenAI, How the Ideas Came Together, 62页，2026年8月1日。 链接 ··· 本文的核心依据。即使跳过公式，只浏览各章前两节的标题，也能立刻看清这份文件的性质。
- OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, 249页。 链接 ··· 成果正文。如果看一下第8章末尾的维数计算，关于有效范围的讨论会变得具体得多。
- OpenAI，“ten-proofs”形式化证明代码库，GitHub。 链接 ··· 10项成果被拆分为12个形式化终点。建议亲自去确认一下审查状态的标注。
背景知识
- Leiden Declaration on Artificial Intelligence and Mathematics，2026年6月2日。 链接 ··· 国际数学联盟支持的宣言。发布24小时内便有1000多人签署。建议将其作为阅读本次发布的背景资料先行了解。
- Henry Cohn and Noam Elkies, “New upper bounds on sphere packings. I,” Annals of Mathematics 157 (2003), 689–714. 链接 ··· 提出了成果1所触及门槛的2003年论文。读一下第1章和第2章，就能找准本次成果的定位。
