夜雨聆风2026年7月10日上午11点08分，一条推文把AI圈和数学圈同时炸醒：一个五十年没人啃得动的图论猜想，被一个模型用64个“分身”在不到一小时里拿下了。
一条推文，两份PDF
发推的人叫Ethan Knight，X账号@eknight，现在在OpenAI，之前在xAI做强化学习。
他的帖子分两层：前一天，GPT-5.6 Sol Ultra刚面向更多用户开放；
今天，这个模型用64个子代理，花了不到一小时，为悬空近五十年的圈双重覆盖猜想（Cycle Double Cover Conjecture，下称CDC）产出了一份完整证明。
"We're excited to see what you all do with Ultra!"
“我们很期待看到大家用Ultra还能做出什么。”
帖子收尾轻描淡写，信息量却拉满：证明全文、任务提示词全都要公开。
▲ Ethan Knight的主帖：Sol Ultra一般可用的第二天，就丢出一个五十年猜想的证明
紧跟的第二条推文只有两个链接：cdc_proof.pdf和cdc_prompt.pdf。
数小时后，Knight又追加一条：证明的Lean形式化版本也开源了，仓库叫openai/cdc-lean，同样署名GPT-5.6 Sol撰写。
证明、提示词、可机器核验的代码仓库，三件套一起把“AI解出数学难题”这个说法第一次配上了完整证据链。
选题源头是账号@Hesamation当晚的转发，正文压成一句口号：“GPT-5.6 Sol Ultra provided a proof for a 50 year old conjecture using 64 subagents, in UNDER 1 HOUR.”互动量远不如源头帖，却把“64个子代理”“不到一小时”“50年猜想”焊在了一起。
评论区里，有人调侃自己试了一下“结果把一个月工资烧没了”，也有人只回两个字：“Real?”
猜想到底在问什么
把图想象成一座城市：路口是顶点，道路是边。
“桥”是那种一拆就让城市断成两半的关键道路，显然不可能被任何环线覆盖，所以“无桥”是必要前提。
圈双重覆盖猜想要求的，是给整座路网铺两层环线公交，每条路都恰好被两条线路经过，不多也不少。
听起来像小学应用题，可半个世纪里数学家只啃下了几类特殊情况：平面图、能被三种颜色染边的三次图、少数几类特殊结构。
真正难啃的部分压缩进一类叫snark的图里，三次、无桥、却怎么染都染不成三种颜色。
数学家Jaeger早就指出，只要CDC在snark上成立，就在所有图上成立；
过去五十年，大量精力都耗在snark、流、覆盖之间的相互转化上，谁也没能钉死最后一块拼图。
CDC还不止一次在arXiv上出现过后来被发现有漏洞、悄悄撤回的“证明”，官方这次的措辞因此格外谨慎，用词只到"claim"（声称）、"produced a proof"（产出了一份证明），远没有到“已解决”的地步。
三页纸，和一份不加掩饰的署名
cdc_proof.pdf只有约三页，标题是A PROOF OF THE CYCLE DOUBLE COVER CONJECTURE，作者栏写着OPENAI。
摘要即定理：
每个有限无桥无向图都有圈双重覆盖。
文末那句AI使用声明才是最让人愣住的部分，证明的数学内容完全归功于GPT-5.6 Sol Ultra，文稿整理靠Codex辅助。
没有“团队协作完成”这类模糊表述，坦坦荡荡摆出来：这道题是模型自己想出来的。
▲ cdc_proof.pdf首页：定理、摘要与那句不加掩饰的AI使用声明
证明骨架并不玄乎：先把问题化简到snark，再祭出一个经典结论，每个无桥图都存在处处非零的Γ-流（Γ取三个二元域的乘积空间），等价于Tutte群流定理里的8-流。
关键一步，是给每条边贴上Γ的一个子集标签，只要在每个顶点处，任意元素在相邻边的标签里出现0次或2次，就能反推出一族圈，每条边恰好落在两条圈里，这正是CDC要的东西。
最后一步是线性代数，证明这套标记方程组一定有解。
全篇像一份短小的研究通讯，没有花篇幅梳理这条技术路线的思想史，这一点后来成了数学家评论时揪住不放的焦点。
真正的主角：一份不许“假装做完”的军令状
比证明本身更值得细看的，是同时公开的cdc_prompt.pdf。
读完才明白，这次真正的技术活儿，是把64个子代理管理成一支不许摸鱼的科研团队，“让AI证明一道题”这几个字，根本盖不住这份任务说明的分量。
提示词先把边界画死：图的定义、桥圈的定义精确到“两条平行边算长度为2的圈”。
然后是一整段明确禁止的“假进度”清单，只对特殊图类成立不算，覆盖次数凑不够恰好两次的不算，靠计算机跑有限规模验证不算，绕到另一个未解决猜想上兜圈子也不算。
多智能体调度的部分更值得逐条细看：
最多64个并发代理同时跑； - 不预设分工
，不许“N个代理专攻策略A”式呆板编制，要求“aggressive and dynamic（激进且动态）”管理搜索； 早期必须保持路线多样性，防止代理一窝蜂扑向同一条看似漂亮、实则走不通的化简方向； 全程配备对抗代理专门挑刺，逐条核对重数、闭合性、平行边、连通性； 拒绝“全局相容性是routine（常规操作）”这类空话，必须给出具体引理或反例； - 在通过对抗审计的完整证明出现之前不许返回结果
，哪怕要放弃，也得先扛满至少8小时。
▲ cdc_prompt.pdf首页：任务陈述与“最多64个并发代理”的调度指令
这里有个有意思的错位：OpenAI在GPT-5.6产品文案里写得清楚，ultra档位默认只协调四个并行代理，评测图里出现过的上限也就16个。
CDC这次把并发数拉到64，说明新闻标题里的“64个子代理”首先是这一次科研级任务给自己开的资源上限，不等于普通用户点一下Ultra就能复现的默认体验。
Hacker News上高赞评论真正较真的，是这份提示词本身，公式反倒没那么多人深究，即便是号称最强的模型，想让它老实做完一道难题，还是得大段写“拒绝模糊乐观”“不许把没证的引理当常规操作”，像在给一个能力极强、却也擅长“表演完成”的合作者立军令状。
大佬转发，狂欢开始
OpenAI总裁兼联合创始人Greg Brockman（@gdb）转发时写道：
"50-year old math conjecture solved with Sol Ultra"
“一个五十年的数学猜想，被Sol Ultra解决了。”
他补了一句：一个人能做到什么的天花板，正越来越取决于野心和想象力。
▲ Greg Brockman的转发：把这件事读成能力边界的迁移
OpenAI推理研究者Noam Brown（@polynoamial）点出一个更冷静的差异：和今年5月“内部模型攻克Erdős单位距离问题”不同，这次用的是今天任何人都能付费用到的公开模型。
沃顿商学院教授Ethan Mollick（@emollick）说得更利落：这是公开档位模型第一次产出新颖数学证明。
三条评论拼出同一个潜台词，门槛在往下移。
数学家读完：漂亮，但没那么神
真正让这件事有厚度的，是数学家Thomas Bloom的介入。
他是曼彻斯特大学皇家学会研究员，维护着数论开放问题网站erdosproblems.com。
7月11日，他发了一条长线程，开场是“A very nice proof!”，“一份很漂亮的证明！”接下来的拆解，泼的冷水比夸奖更多。
▲ Thomas Bloom的线程开场：先肯定，再拆解
他指出，证明背后的思路并不新：把圈覆盖和三次图上的Fano流（取值在F₂³空间的处处非零流）联系起来，至少能追溯到1983年Bermond、Jackson、Jaeger等人的工作。
只读三页纸的摘要，很容易误以为这是全新发明，它其实是四十多年前就有的经典工具。
更让人在意的是，AI生成的论文常有引用缺失的老毛病：哪怕模型独立想到了相似思路，训练有素的研究者第一反应通常是先查文献，动笔之前先把前人的脚印摸一遍。
最有意思的一点是，Bloom认为这个证明本质上很短、很初等，放到1980年代原则上就有可能被发现。
一旦连到Fano流，剩下的主要工作是“写出合适的边标记，再用一段不长的线性代数检查相容”。
标记方式几乎水到渠成，唯独有一步，把某条边的权重强行指定成特殊值，其余置零，显得突兀，却恰恰是撑起整个证明的关键。
Bloom猜，人类当年大概率试过更自然的标记方式，失败后很少有人会想到反过来“扭”一下这个设定。
真正戳中要害的，是他对人和AI搜索心理的对比：人遇到自然思路走不通，容易耸耸肩，认定题目本来就难，转身去找更重的工具；
AI不会有这种情绪性放弃。
64个代理里随便挑一个，只要被要求“找到满足条件的标记，再用初等线性代数验证相容”，在路径真实存在的前提下，Bloom说他反而会预期它能成功。
他把CDC和5月那次Erdős反例放在一起看，得出一个更大的判断：一些顶着“重大开放问题”名号的题目，答案未必需要全新理论。
AI公司同时向许多开放问题砸算力、只公布成功的那批，会让外界更快知道哪些题目其实一直够得着，但这终究只是所有开放问题里的一小撮，事先谁也不知道是哪几道。
肯定证明漂亮，又把“五十年惊天难题被AI秒杀”的情绪值按回了理性区间，这条线程同时做到了两件事。
Lean仓库：另一条可以自己核验的路
自然语言写的证明需要专业读者花时间消化，openai/cdc-lean则提供了一条扎扎实实的机械核验通道。
README写明：项目对“有限无环无桥多重图”的圈双重覆盖定理做了kernel-check，终点定理叫CDCLean.cycleDoubleCover_of_bridgeless，技术路线与PDF证明完全对应。
▲ openai/cdc-lean仓库：Lean形式化的可核验版本
配套的VERIFICATION.md给出更扎实的数据：lake build跑通，1727个编译任务全部成功；
源码里搜不到sorry、admit这类占坑标记，也没有自定义的可疑公理；#print axioms查最终定理，只依赖propext、Classical.choice、Quot.sound三条Lean标准基础公理。
这不等于数学共同体已经读懂并接受了自然语言叙述，机器检查的是逻辑链条是否闭合，不检查这条链条讲得漂不漂亮、贴不贴近既有文献。
但它确实提供了一条独立于PDF、任何人都能在本地跑一遍的验证轨道。
放进更大的坐标系里看
今年5月，OpenAI一款内部推理模型给出Erdős单位距离问题的反例，推翻了“方格点构造本质最优”这条流传已久的猜测，结果经外部数学家核实；
官方当时特别强调，那个模型并未针对数学问题专门搭建脚手架训练。
七月这次不一样的地方，恰恰是Noam Brown点出的那个词，今天就能用。
先用内部前沿模型证明“能碰开放问题”，再用公开档位在多智能体编排下产出可核验证明，两步棋走得相当连贯，很难说只是巧合。
ultra默认协调四个代理并行，评测演示出现过16个代理的配置，CDC这次拉到64，是把调度旋钮拧到了科研演示的极限值。
Hacker News那条讨论帖（约489分、402条评论）里流传一句调侃：我们会不会正在从数学家变成“矩阵心理学家”，工作从推导公式变成琢磨怎么跟AI提要求。
价值的落点，正从“一个答案”挪向“一整套被管理好的搜索过程”。
还没写完的部分
同行评议怎么走完，证明会不会被重写成更贴近已有文献的版本，64个代理这套打法放到普通用户手里成本和成功率如何，还有哪些看着古老、其实存在短证明的猜想正排在下一轮多智能体搜索的队列里，这些问题眼下都没有答案。
维基百科词条最新增补的这段文字，或许是目前最准确的定性：OpenAI发布了预印本，声称对猜想给出了肯定解决，证明由GPT-5.6大语言模型生成。
“声称”两个字本身就是一种态度：记录下事情发生过，没有替数学共同体盖棺定论。
64个子代理确实在不到一小时里跑出了一份三页纸的证明，这件事真实发生了。
至于它究竟打开了一扇门，还是把一道其实一直够得着的题目提前几年摘了下来，五十年都等过来了，不差这一轮同行评议的时间。
