夜雨聆风深夜刷推特的图论研究者们,大概都被这条帖子晃了一下神。
一个悬置了将近半个世纪的问题,一份三页纸的证明,一句轻描淡写的说明:64个子代理,不到一小时。
一条推文,宣布一个"解决"
2026年7月10日下午6点08分,OpenAI员工Ethan Knight(X账号@eknight)发出一条帖子。
前一天,GPT-5.6家族的旗舰模型Sol Ultra刚刚向公众开放。
Ethan说,他们用这个模型,64个子代理并行工作,不到一小时,生成了一份对图论中圈双重覆盖猜想(Cycle Double Cover Conjecture,简称CDC)的证明，这道题已经悬置了大约50年。
▲ Ethan Knight的公告帖,不到一天时间里获得五千多点赞、百万级浏览量。
"Yesterday Sol Ultra became generally available... today we're sharing a proof of the Cycle Double Cover Conjecture, a nearly 50 year old open problem in graph theory, generated with 64 subagents in under 1 hour."
“昨天Sol Ultra一般可用……今天我们分享一份圈双重覆盖猜想的证明,这是图论中一个近50年的开放问题,由64个子代理在不到一小时内生成。”
帖子发出不到一分钟,跟帖甩出两个OpenAI的CDN链接:一份证明PDF,一份提示词PDF。
证据和过程都摆在台面上,没有藏着掖着。
当天晚上7点55分,OpenAI总裁Greg Brockman转发放大:“50-year old math conjecture solved with Sol Ultra(用Sol Ultra解决了一个50年历史的数学猜想)”,还补了一句意味深长的评论，“能做什么的上限,越来越取决于野心与想象力”。
晚上10点37分,Ethan又发一条:Lean形式化仓库开源了,同样由GPT-5.6 Sol撰写。
短短几个小时,Hacker News挂上了热榜,评论数百条。
Wikipedia的Cycle double cover词条,已经默默加上了这句话:“2026年7月10日,OpenAI发布预印本,声称给出了肯定性解决方案。”
一条本该只在数学圈子里小范围流传的消息,就这样被推上了主流视野。
这个猜想,到底在问什么
想弄明白"64个子代理"到底干了什么,得先搞清楚它们要解决的问题有多难缠。
拿一个足球来想象。
足球表面由若干块五边形和六边形拼成,每一条棱,恰好是两块面片的公共边，不多不少,正好两次。
图论里把这种"点用线连起来"的结构叫做图。
如果把足球的棱边网络抽象成一张图,每一块面片的边界看作一个"圈",那么整个足球的棱边,就被这些圈"双重覆盖"了。
圈双重覆盖猜想问的是:换成任意一个更抽象、不一定是多面体、甚至不一定能画在平面上的图,只要它满足一个基本条件，没有"桥"(删掉这条边就会让图断成两半的那种要害边),是否总能找到一簇圈,让每条边都恰好被盖两次?
半个世纪以来,数学家们证明了不少特殊情况:平面图成立,能被三种颜色规规矩矩染色的立方图也成立。
但一般情况,始终悬而未决。
真正难啃的骨头,是一类叫snark的立方图，每个顶点恰好三条边,却怎么也没法用三种颜色把边染得干净利落。
教科书级的结论早就指出:只要snark成立,一般情况就跟着成立。
可snark偏偏是数学家们几十年绕不过去的礁石。
揭秘"64个子代理":一份写满禁令的作战手册
真正让技术圈兴奋(以及警惕)的,反倒是指挥这场攻坚战的提示词，比三页纸的证明本身透露出更多信息。
cdc_prompt.pdf公开了完整任务说明,读起来更像一份"自治数学研究团队作战手册"。
▲ 官方公开的提示词PDF首页,写明任务定义与多代理指令。
任务定义写得极严:不允许证明特殊情况就算完成,不允许归约到另一个尚未证明的猜想,不允许拿"计算验证了几个固定规模的案例"来交差。
半成品,一律不算数。
提示词里还埋了一句耐人寻味的心理暗示:“为了本任务,假定完整肯定证明存在”;以及一句近乎强迫的指令:“在哪怕考虑返回或放弃之前,至少花8小时”。
公告里说实际跑完不到一小时，这句"至少8小时",更像是防止模型半途而废的心理锚点,未必对应真实耗时。
真正对应"64"这个数字的,是一段被称为Multiagent v2的规则:
最多64个并发代理同时运作;不设固定角色表,不搞"N个专门负责策略X"这种流水线分工,而是激进、动态地管理搜索方向。
早期必须保持真正多样的方法组合，不同的形式化路径、不变量、代数视角、结构归纳、流理论、极值论证,一样都不能少。
更关键的是一条防止"集体想歪"的规则:不能把当前最被看好的思路提前告诉大多数代理,防止团队过早收敛到一条"看起来优雅但实际残缺"的死路上。
而且全程部署了对抗代理，专门挑刺的那一批,负责检查重数是否算对、有没有伪圈、图断不断连、约化过程有没有偷偷引入新的桥。
系统还被明令拒绝任何"进展顺利""全局相容是routine操作"之类的空话,必须交出具体的引理、构造或者反例。
根代理(root agent)则不断做一件事:综合、挑战、改道、发动新一轮搜索。
只有通过对抗审计的完整证明,才被允许最终提交。
有Hacker News网友评价,这套流程像是“Tree-of-Thoughts的工程化实现”;也有人半开玩笑地说,那一长串"不许这样不许那样"的禁令,几乎像是提前预判了模型会犯哪些历史上出现过的错误。
三页纸,缝出半个世纪的缺口
那份声称完成证明的PDF,标题是A Proof of the Cycle Double Cover Conjecture,署名OPENAI。
文中的AI使用声明毫不含糊:数学证明全部归功于GPT-5.6 Sol Ultra,文稿撰写则由Codex协助完成。
▲ 证明PDF首页,可见标题、摘要与Theorem 1.1。
证明的骨架,压缩下来大致是这样一条链路:先用经典的约化定理,把问题收窄到最难的snark情形;再借助上世纪80年代就已确立的流理论结果,证明每个无桥图都存在一种"处处非零的群流";接着把这种流,转化成一套关于顶点与边的线性方程组;最后证明这套方程组必有解，解出来,就是所求的圈双重覆盖。
全文大约三页。
Hacker News上有读者形容它“更像专家们几十年没想到、被随手拼起来的一个精巧线性代数接口,跟费马大定理那种漫长的理论建造完全是两回事”。
换句话说:所用的每一块材料,几乎都是数学界早就摆在桌面上的老工具。
真正的难点在于,把它们这样拼在一起的那一下巧劲。
Lean形式化:把"读起来像证明"变成"机器能查的证明"
发完证明PDF五个多小时后,Ethan又扔出一个仓库地址:openai/cdc-lean。
▲ 开源的Lean形式化仓库,README记录了终点定理与验证结果。
这是用Lean语言对整份证明做的机器可检查版本,同样由GPT-5.6 Sol撰写。
仓库里的VERIFICATION.md记录着:完整代码库构建成功,跑了1727个编译任务;源码扫描没有发现sorry、admit这类"先跳过、以后再补"的占位符;对最终定理执行公理检查,只报告了三个数学界公认无害的基础公理。
这一步的意义在于,它把一份"读起来很有道理"的自然语言证明,往前推进了一大截,变成了可以被计算机内核逐字逐句核验的形式化对象。
但要注意,这仍然不等于"全世界图论专家都已经读过并点头"。
机器验证的是逻辑链条内部没有断裂,验证不了的是，这套定义方式是否和经典文献完全对齐,约化步骤有没有漏掉某种边界情形。
这些问题,只能靠人一行一行地读。
转折:怀疑的声音从没停过
Greg Brockman转发之后,事件的热度冲上了一个高点。
但技术社区的反应,远没有社交媒体上那么一边倒。
▲ Hacker News讨论页,约489点赞、401条评论,首屏聚焦在提示词设计与验证问题上。
Hacker News的评论区,“claim不等于verified(主张不等于已验证)”成了反复出现的主旋律。
有人估计24小时内会有初步裁决,也有人认为真正的专家精读需要数天甚至数周。
更尖锐的追问指向方法论本身:“他们到底试了多少个开放问题,才刚好蒙中这一个?” 有图论从业者留言说,自己也用过5.3到5.6版本的模型去啃过几道"简单一点"的开放题,统统没有成功。
这条帖子火了,但没被攻克的那些,没人知道有多少。
还有一层容易被忽略的现实是成本。
第三方粗略估算,如果64个子代理同时满负荷跑上一小时,费用区间可能从两三百美元,到极端吞吐假设下的上万美元，这份数字来自民间估算,并非OpenAI官方账单,却点出一个简单的事实:模型对公众开放,不代表每个人都能以同样的并行规模,复现同一场搜索。
历史的阴影也没有被忘记。
CDC这道题,过去在arXiv上早就出现过"看起来像证明"的文本，此前有过后来被指出漏洞、最终撤回的尝试。
也正因为如此,OpenAI这次选择同时公开提示词、自然语言证明和Lean形式化三样东西,更像是提前把整个攻击面摊开在阳光下,而非只发一份新闻通稿了事。
Wikipedia的措辞也透着这份谨慎，用的是**claim(主张)和preprint(预印本)**这类词,始终没写"已解决"。
一小时之后,轮到谁来验证
把这件事放进更大的坐标系里看,它的分量才立得住。
2026年5月,OpenAI就曾公布过一次内部通用推理模型的成果:在离散几何领域,否定了一个与"单位距离"相关的长期猜想,给出无穷多族反例构造。
那一次,重点落在"找到反例"上。
这一次不同。
CDC事件里,模型名称可以指名道姓(GPT-5.6 Sol Ultra),能力档位可以指名道姓(Ultra),连过程配置都可以指名道姓(最多64个并发子代理)。
这是一次肯定性证明的尝试,产物完全可以下载核对。
如果这份证明真的经得起图论共同体逐行审查,它会是"公开可用的大模型,攻克Wikipedia级别未解问题"的一个强信号。
如果最终发现了缺口,它至少留下了一份异常完整的失败记录，因为提示词里,把模型被要求避免踩的每一个坑,都写得清清楚楚。
64个子代理,不设固定分工,互相不告知最看好的路线,全程有对抗代理挑刺,拒绝一切"routine"式的空话。
这套流程本身,或许比证明结果更值得记下来，它可能正在变成一种新的组织技术:怎么让一大群AI代理,像一个真正的科研团队那样各自摸索,谁也不抄谁的捷径。
至于圈双重覆盖猜想究竟有没有被真正解决,现在下结论还早。
球已经踢给了数学共同体。
