夜雨聆风一道被数学家搁置了整整半个世纪的猜想,昨天被人叫来64个“AI分身”,不到一小时就摁了下去。
五十年的老问题再次浮上台面
2026年7月10日,OpenAI工程师Ethan Knight在X上敲下一段话。
"Yesterday, we made GPT-5.6 Sol Ultra generally available. Today, we're sharing that it produced a proof of the 50-year-old Cycle Double Cover Conjecture using 64 subagents in just under one hour."
“昨天,我们让GPT-5.6 Sol Ultra全面上线。今天,我们要公布:它用64个子代理,在不到一小时内,给出了那道悬而未决五十年的『圈双重覆盖猜想』的证明。”
Sol Ultra昨天才刚刚对所有人开放。
第二天,它就把图论里一道跨越半个世纪的开放猜想给解了。
这条推文的互动数据很快跑起来:5.3k点赞、404转发、176回复、约124.5万次浏览。
Ethan紧接着在同一线程里贴出两份PDF的下载链接，一份是证明本身,一份是完整的提示词。
他没有藏着掖着。
证明怎么来的、prompt怎么写的,全部摆在桌面上。
▲ Ethan Knight的正式公告,约124.5万次查看,是这件事最权威的一手信息
这道猜想到底是什么来头,得先从一张地铁图讲起。
一张地铁图,五十年没人走通
把一张无向图想象成地铁线路图:站点是顶点,轨道是边。
一条“圈”就是从某站出发,沿着轨道绕一圈回到起点,中途不重复走同一段轨道。
“圈双重覆盖猜想”问的是:能不能找出一批圈,让每一段轨道恰好被两个圈盖住?就像给每条轨道铺上两层环路,谁也不多,谁也不少。
这个问题由Tutte、Itai与Rodeh、Szekeres(1973年)、Seymour(1979年)在不同表述下先后提出。
前提是图必须“无桥”，桥是那种一旦拆掉就会让整张图断成两半的轨道,它天生不在任何圈上,自然没法被覆盖。
对平面图,取每个“面”的边界圈就够用了,因为每条边天然属于两个相邻的面。
对能做“三色染色”的三次图,数学家也早有构造方法。
麻烦全部堆在了一类特殊图形上，snark,一种三次、无桥、却怎么染色都染不出三种颜色的“刺头图”。
五十年里,数学家证明了大量特殊情形、排除了很多小尺寸的反例,却始终缺一个通用的肯定性证明。
这次,Sol Ultra宣称给出了那个缺了五十年的通用证明。
拆开证明:重活是1970年代干的
OpenAI公开的证明文档只有大约三页,标题是《A PROOF OF THE CYCLE DOUBLE COVER CONJECTURE》,署名OPENAI。
文档开篇写明:
“证明内容完全由GPT 5.6 Sol Ultra给出,成文借助Codex(配合GPT 5.6 Sol)完成。”
证明的核心思路可以拆成三步“翻译”。
第一步,把“找圈”翻译成“找流”。
数学家早就证明,任何无桥图上都存在一种叫nowhere-zero 8-flow的标签系统，给每条边贴上非零标签,保证每个顶点“流入等于流出”。
这套定理属于1970年代图论的标准库存,AI没有重新发明它。
第二步,把“一个标签”翻译成“两个标签的组合”。
如果在每个顶点处,每种颜色标记出现的次数是0或2,那这种颜色标记自己就能拼成一堆圈。
第三步,也是最巧的一步:局部在每个顶点都能写出这种标记,但一条边有两个端点,两端算出来的标记可能对不上。
于是引入顶点上的“平移参数”和边上的“二进制开关”,把粘合问题写成一套线性方程组,再用对偶空间论证，证明这套方程组永远有解。
换句话说,重体力活早在半个世纪前就由8-flow定理干完了,AI补上的是最后一步“怎么把两端粘合到一起”的线性代数论证。
这也是Wikipedia“Cycle double cover”词条在证明公布当天就更新的原因，词条写入,OpenAI于2026年7月10日发布预印本,声称对猜想给出了肯定性解决。
▲ 英文维基词条当天即更新,记录了OpenAI的预印本声明
社区里读过全文的人普遍有个共同感受:这篇证明短得不像话。
三页纸,靠的是把已有的标准工具用一次精巧的线性代数缝合起来,谈不上从零开始的理论建设。
这既让人觉得优雅可核查,也让人忍不住追问:这一步,人类专家五十年里为什么没写出来?
扒开prompt:AI没那么神,是人“逼”出来的
真正让这件事变得耐人寻味的,是那份同样公开的提示词文档。
任务定义写得极其形式化,要求“完整解决:每个有限无桥无环多重图都有圈双重覆盖”,而且明确排除一切取巧路径，部分结果、只解特殊图类、归约到另一个未证猜想、固定规模的计算验证,一律不算完成。
最耐人寻味的一句藏在任务定义里:
"Assume for purposes of this task that a complete affirmative proof exists."
“就本任务而言,请假设一个完整的肯定性证明是存在的。”
这句话在Hacker News上被反复讨论。
它更像一种动机设定,目的是防止模型半途觉得“这题可能无解”就提前放弃。
紧接着,prompt里还压上了一句苛刻的时限要求:
"Spend at least 8 hours on this before even thinking of returning or giving up."
“在你考虑返回结果或放弃之前,至少要花8个小时。”
这句话和“不到一小时”的实际耗时摆在一起,读起来颇为反讽，8小时更像是对系统设定的心理底线,和这次运行实际花掉的时间对不上号。
真正的技术核心是这一句:
"Use multiagent v2 aggressively and dynamically. You have up to 64 concurrent agents available."
“大胆而动态地使用multiagent v2系统。你最多可以调用64个并发代理。”
prompt里详细列出了一套启发式策略:早期要保持路线多样性,不能让大多数代理都盯着当前最受青睐的那条路;登记进展要按数学思路的“家族”分类,不能只看表面措辞;对“归约到另一个同样难的引理”要保持警惕;还要专门安排对抗性代理,去检查“exact-two覆盖”“平行边构成的2-圈”“割点”“归约是否偷偷引入了桥”“论证是否循环”这类容易出错的地方。
根代理不断综合各路结果、发起挑战、重新分派方向,不允许在第一波尝试失败后就停手。
这套设定揭示的东西,比“AI解出了猜想”这句话本身更值得琢磨:即便是当下最强的模型,也需要一整套外部的搜索控制程序去推着它广搜、防止早停。
把这些控制程序沉淀进未来的训练,正是实验室打磨模型的路径之一，也是外部观众从一次成功结果里,还原不出来的“冰山以下”部分。
至于成本,Hacker News与Codeforces上的粗略估算认为:64个代理跑满一小时,按API输出吞吐上限来算,大概率是数百美元量级;如果换算成吞吐更高的Sol Fast配置,估算能到约1.3万美元。
这些数字都是社区推算,OpenAI没有在公告里公布真实账单。
高层下场:措辞从“猜想”跳到了“解决”
公告发出后不到两小时,OpenAI总裁兼联合创始人Greg Brockman亲自引用转发:
“50-year old math conjecture solved with Sol Ultra.”
“用Sol Ultra解决了一道50年的数学猜想。”
他还补了一句评论:能力的边界,越来越取决于人的野心和想象力。
▲ Greg Brockman公开背书,措辞用上了“solved”这个词
十几分钟后,OpenAI推理方向研究者Noam Brown补上了一个关键区分。
他把这次事件和此前的Erdős单位距离问题成果做了对比:
"Unlike the Erdős Unit Distance Problem, this was done with a model publicly available today."
“和Erdős单位距离问题不同,这次用的是今天就对公众开放的模型。”
▲ Noam Brown划出关键区别:这次调用的,是任何人登录账号就能用的公开版本
这句话之所以重要,是因为它把整件事从“OpenAI内部又出了个厉害东西”,悄悄挪到了“你我今天登录账号也能用的模型,干出了这件事”。
想象空间一下子被撑开了。
冷水泼过来:验证还没完,风向已经先转了
热闹归热闹,冷静的声音也没缺席。
在社区账号@kimmonismus放大这套解读的帖子下面,@EdgeCaseBriefs留言泼了盆冷水:验证工作根本还没开始,“新时代”的说法已经跑在了前头。
▲ 社区里的降温声音:审稿远没结束,标题已经先喊出了“时代”二字
Hacker News上,那条链向cdn.openai.com上证明PDF的帖子迅速冲到约489分、400余条评论。
技术圈的讨论比社交媒体上冷静得多,焦点也更扎实:
选择偏差问题，OpenAI到底往这套harness里喂了多少个开放猜想,才撞中这一个?如果尝试了成百上千个只成功一次,故事的解读方式会完全不同。
是否存在人为注入，有图论背景的评论者提到,自己用5.x系列模型试过若干开放问题都没跑通,忍不住质疑这次是否存在未公开的人工干预。
证明的分量该怎么算，有人认为,真正改写数学结构的证明,应该像费马大定理那样催生出一整套新理论;组合数学历来更“取巧导向”,AI恰好可能擅长这种打法,但这不等同于开创新领域。
▲ HN上的技术讨论迅速冲到近500分,焦点集中在prompt设计与验证进度上
入口帖子下面的普通网友评论则更接地气。
有人只回了一句“Real?”;还有人调侃自己也试过类似的多代理配置,“光是思考就花掉了我一个月工资”。
拉远一点看:AI证明数学的这条曲线
把这件事放进更长的时间线里看,会发现它有一串前情。
近年来,前沿模型在IMO风格、AIME这类竞赛数学基准上的分数一路飙升;专门面向Lean的定理证明模型,在miniF2F之类的数据集上也逼近满分。
这次CDC证明选择用正面构造去啃一道Wikipedia级别的开放猜想,跳出了刷基准分数的老路子,分量摆在那里。
同一天22点37分左右,Ethan又追加宣布,开源了一份Lean形式化仓库openai/cdc-lean,同样声称由GPT-5.6 Sol撰写。
仓库的VERIFICATION.md记录显示:完整的Lake构建成功,源码扫描没有发现sorry、admit这类“跳过证明”的标记,终点定理的公理列表也只剩下Lean标准的三条基础公理。
但这里有个容易被新闻标题模糊掉的分层:自然语言PDF证明、Lean仓库的类型检查、数学共同体的独立同行评审,是三件不同的事。
前两件已经完成,第三件才刚刚开始。
有意思的是另一层反直觉信号。
业界常说新模型“更懂意图、越来越不需要写复杂prompt”,但这次公开的提示词恰恰相反，冗长、充满禁令、写满了搜索策略。
这提醒人们:在极端困难的任务上,人类目前仍然在用自然语言,给AI编写一套完整的“搜索控制程序”。
里程碑,还是带瑕疵的插曲?
数学史上早有过“猜想开放很久,证明却出奇短”的先例，往往是因为某个后来才成熟的中间工具,提前把重活干完了。
这次的8-flow定理正是如此,它诞生于1970到80年代,在那套语言就位之前,同样的线性代数粘合根本无法表述。
有播客曾经区分过两类数学家:创造语法的人,和操作已有语法的人。
Hacker News上不少人引用这个区分,认为眼下的AI更接近后者，它极其擅长在正确的工具库里,找到人类没有先写下来的那种组合。
独立数学家的详细审稿意见会不会挑出漏洞?Lean形式化能不能与PDF逐字逐句对上?第三方复现构建顺不顺利?OpenAI内部到底拿这套harness试了多少道悬而未决的猜想,成功率和失败模式又是什么样?
这些问题目前都还没有答案。
它们不会改变“公告与全部材料已经公开”这个事实,但会决定这件事最终被写进数学史的方式，是一座里程碑,还是一段带着瑕疵的插曲。
答案要等审稿的人翻完那三页纸,才会揭晓。
