GPT-5.6 Sol Ultra 一小时内证明循环双覆盖猜想，我读完了 OpenAI 的论文

7 月 10 号，OpenAI 研究员 Ethan Knight 在 X 上发了一条消息。他说，GPT-5.6 Sol Ultra 调用 64 个子智能体，在不到一小时里，证明了循环双覆盖猜想（Cycle Double Cover Conjecture）。这个猜想已经在图论界悬了 50 多年。

我当时就愣住了。

不是因为我不相信 AI 能做题。而是这个猜想，我上研究生时听过一次，教授讲完轻描淡写地说了一句，「这个问题还没人解决」。我当时觉得它离我太远，远到连尝试的念头都没有。现在突然告诉我，一台机器一小时搞定了。

我第一反应是，这新闻是不是又被夸张了？所以我下载了 OpenAI 发布的论文原文，把三页纸读了一遍，又把提示词 PDF 也翻了一遍。下面是我真实的想法。

先说人话，什么是循环双覆盖猜想

你可以把它理解成一道关于「图」的拼图题。

一张图由顶点和边组成。我们想知道，能不能找到一组环（cycle），让每条边恰好出现在两个环里。这里的环，允许只有两个顶点和两条平行边组成的长度为 2 的环。重复的环也算数，所以叫 multiset，不是集合。

这个要求非常精确。每条边必须是恰好两次，不能多，不能少。

1973 年 George Szekeres 提出这个想法，1979 年 Paul Seymour 也独立提出。更早的时候，Tutte 也有相关的直觉。几代数学家在上面花了很多年，只证明了平面、3 边可染色等特殊情况。最通用的版本，一直没人拿下来。

它为什么重要？坦白讲，它跟四色定理、 nowhere-zero flow、电路网络设计都有千丝万缕的关系。它看起来像个纯粹的图论练习，但背后是一个更宏大的问题，我们能不能用一组简单的局部结构，覆盖一个复杂网络的全局约束？

这个问题，AI 现在说它解出来了。

论文本身只有三页，但思路很精巧

我把论文原文读完后，最直接的感受是，它短得离谱。加上参考文献，一共才四页。

核心思路大概是这样。

第一步，把问题归约到三次图（cubic graph）。也就是说，只要证明每个无桥的三次图都有循环双覆盖，就足够了。这是图论里标准的简化技巧。

第二步，利用 8-流定理。Kilpatrick 和 Jaeger 证明，每个无桥图都存在一个 nowhere-zero 的 F_32 流。这里的 F_32 是 32 个元素的有限域，F_2 的五次扩域。通过 Tutte 的群流定理，这等价于存在一个 nowhere-zero 8-flow。

第三步，关键归约。作者想把这个流转化为一种边标记，每条边被标记成一个二元集合，使得在每个顶点处，每个元素都出现零次或两次。如果能做到这件事，根据 Lemma 2.1，立刻就能得到循环双覆盖。

第四步，也是最难的一步，是证明这种集合标记真的能构造出来。论文把它转化成了一个线性代数问题，定义了一个映射 L，然后用对偶空间论证 d 一定在 L 的像里。最后一行计算，在 F_2 上，2 乘以任何数都是 0，所以整个和归零，证明完成。

我读完这段时，说实话没有完全跟完所有线性代数细节。但我能看出它的结构是完整的，从流的存在性，到局部标记，再到全局兼容性，最后落到线性代数。

论文最后有一行特别刺眼的话。

「The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex.」

不是人类写的，是 AI 自己证的，人类只负责整理成论文。

提示词比证明更值得研究

OpenAI 同时公布了生成证明所用的提示词。我读完之后，反而觉得提示词比论文本身更有意思。

提示词一开始就把问题定义得死死的。什么是图，什么是桥，什么是环，什么是循环双覆盖，全部用形式化语言写清楚。它明确要求，只接受完整证明，不接受特殊情况、部分结果、计算验证、或者归约到另一个未证猜想。

真正厉害的是后面的多智能体策略。

最多同时调用 64 个智能体。早期阶段不要让它们知道哪个方向被看好，必须保持多样性，各自探索不同的代数视角、结构归纳、流形式化、嵌入方法、极值论证。有一个显式的「方法家族注册表」，按数学思想而不是措辞来分组。如果太多 agent 涌向同一个方向，就要把一部分 redirect 到未探索的方向。

对抗智能体全程在线。每个候选证明必须被检查，边的覆盖次数是否真的是恰好两次；有没有把闭合路径误当成环；有没有漏掉平行边形成的 2-环；有没有在归约中引入桥；有没有循环引用原猜想本身。

还有一个硬性约束。除了普通数学背景或标准命名定理，禁止公开搜索这个猜想的解法。不能回答「这个问题还是开放的」，也不能用网络搜索找思路。

最后一句更是狠，「Spend at least 8 hours on this before even thinking of returning or giving up.」

系统实际只跑了一小时。也就是说，它原本给自己留了 8 小时，结果提前很多就解决了。

作为一个经常折腾 LangGraph 和 multi-agent 系统的人，我真心觉得这个提示词是一份高质量的研究型 agent 设计文档。它展示的不是简单的「分任务给多个 agent」，而是一种动态搜索、对抗验证、持续重定向的研究闭环。

先别急着狂欢，问题还很多

读到这里，你可能会觉得我要开始吹了。但我反而想泼点冷水。

这份证明目前没有经过同行评审。OpenAI 把它上传到自家 CDN，和一篇发表在数学期刊上的正式论文，完全是两回事。历史上，循环双覆盖猜想已经出现过多次「证明」，后来都被发现漏洞，有些还撤稿了。AI 生成的内容并不天然免疫这种错误。

曼彻斯特大学的数学家 Thomas Bloom 是最早公开评论的人之一。他说这是一个非常漂亮的证明，简洁、基础，用的方法并不复杂，如果当年有人想到，80 年代就可能完成。但话锋一转，他指出了一个问题，论文没有引用 Bermond、Jackson 和 Jaeger 1983 年的经典论文。这是 AI 生成数学论文的通病，它不太知道什么该引用，什么属于人类数学共同体的常识。

另一个问题是，证明没有用 Lean 或 Coq 等形式化工具验证。论文里全是自然语言推导，任何一步都可能隐藏 subtle 的错误。图论相关的形式化数学库目前也还不够成熟，想完全形式化这个级别的定理，短期内也很难做到。

所以我的判断是，它很有可能是对的，但离「被数学界公认」还有一段距离。未来几周到几个月，专家们会逐行审查。如果它站住，那确实是个历史事件；如果被找到漏洞，也完全不奇怪。

AI 做数学，真正的变化在哪里

这件事最让我震撼的，不是它解了一个具体问题，而是它改变了「发现」的形态。

如果最终验证正确，这将是 AI 第一次独立完成一个被列入维基百科「未解决数学问题」列表的重要难题。在此之前，DeepMind 在帽子集合问题上取得过突破，AI 也在纽结理论中有贡献，但那些都是人机协作。这一次，论文白纸黑字写着 proof is entirely due to GPT 5.6 Sol Ultra。

Thomas Bloom 有一个观察特别打动我。他说，人类数学家通常会尝试一种自然的方法，如果失败了，很可能就放弃。AI 不会气馁，它能在无数细微变体中持续尝试。

这不是说 AI 比人类更聪明。事实上，论文里用的核心工具，8-流定理、有限域、线性代数，都是几十年前就存在的东西。AI 没有发明新的数学概念。它的优势是耐心和并行搜索。64 个智能体同时探索不同方向，对抗智能体不断找 bug，这其实是一种把人类数学家难以承受的试错过程，自动化了。

这让我想起自己写 Agent 时的一个痛点。我们总希望 agent 能像人一样「有灵感」，但真正的突破往往来自大量平庸尝试的累积。GPT-5.6 Sol Ultra 这次给出的，可能不是一个天才式的跳跃，而是一个被系统性地搜索出来的、人类因为时间和耐心限制而错过的证明。

如果这是对的，那数学研究的未来会变成什么样？我不好说。至少有一点很清楚，AI 不再只是辅助工具，它已经开始做原创性的、可以被独立发表的数学尝试。人类的角色，会从「证明者」慢慢变成「验证者」和「策展者」。