解开10道难题的记录，竟是一本错题集
OpenAI的Astra放弃了已经完成的证明
开篇
8月1日，OpenAI宣布其下一代模型Astra的内部版本解开了10道数学与理论计算机科学难题。国内报道的标题大多聚焦在同一个数字上：289万韩元。
但那天发布的文件不止一份。有一篇整理结果的249页论文，有一个供机器验证的形式化证明仓库，还有一份62页的文件。标题是「How the Ideas Came Together」，意思是“这些想法是如何汇聚而成的”。
读者，如果你打开这份文件，会觉得有点奇怪。里面几乎没有讲“正确答案”，反倒不断出现“为什么这个方法不行”。
先说结论。这次发布真正新颖的地方，并不在于AI找到了答案。而是把通往答案途中被舍弃的路径，单独整理成文件公开了出来。
先来看看这10个问题是什么
不需要完全理解内容，只要大致感受一下问题的类型就足够了。
| # | 问题 | 通俗地说 |
|---|---|---|
| 1 | 高维球体填充 | 把球紧密堆叠时，最多能填充到多少 |
| 2 | 二元·球面码 | 能容忍错误的编码最多能造出多少个 |
| 3 | 非sofic群 | 是否存在无法用有限次“搬移”来模拟的无限对称结构 |
| 4 | Connes刚性猜想 | 能否仅凭某个结构的“影子”把它还原出来 |
| 5 | 算术电路复杂度 | 特定计算最少需要多少次乘法 |
| 6 | 量子并行重复 | 让同一个游戏重复多次，获胜概率会大幅下降吗 |
| 7 | 最近向量问题 | 在格中寻找最近的点有多难 |
| 8 | 埃尔哈特体积猜想 | 满足特定条件的图形能达到的最大体积是多少 |
| 9 | 多色拉姆齐数 | 无论用多少种颜色，最终都会出现同色三角形吗 |
| 10 | 极值图论 | 在避开特定形状的前提下，最多能画多少条线 |
第3题和第4题分别是1999年和1980年代起悬而未决的问题，第9题和第10题则是埃尔德什遗留问题列表中的第183号、第146号和第180号。答案的形态也各不相同：有的是新证明，有的则是推翻了长期被认为为真的猜想的反例。
cdn.openai.com有一个小事实值得留意。OpenAI把结果算作10项，但那份走读文件却分成了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章都是从失败的尝试开篇。
- 失败的形态有四种：类比错了、捷径摧毁了目的地、证明了“卡住本身”、完成了却放弃了。
- 实际适用范围很窄。能力上的跃升和应用上的跃升，是两个不同的维度。
读完之后，建议你做一件事：如果这周你做了什么决定，请在采纳的方案旁边，用两行字记下被舍弃的方案以及舍弃的理由。六个月后，这两行字能帮你省下一个小时的会议时间。
不知道你所在的组织，是否真的把“评估过但不可行的理由”记录成文件？如果有，是什么形式？如果没有，卡在哪一步？欢迎在评论区分享。如果案例积累得够多，我们下一期就来整理一套记录“淘汰理由”的实务格式。
💬 如果你有记录被舍弃方案的方式，欢迎在评论区分享
📨 如果身边有同事正在第二次评审同一个结论，欢迎把这篇文章转发给他
参考资料与延伸阅读
核心来源
- 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小时内就有超过1,000人签署。建议先读这份文件，作为理解本次发布的背景。
- Henry Cohn and Noam Elkies，《New upper bounds on sphere packings. I》，《Annals of Mathematics》157 (2003)，689–714。 链接 ··· 这是提出第1题所达到那个门槛的2003年论文。读完第1章和第2章，就能明白这次结果所处的位置。
📝 术语说明
