数学家还在审稿，AI已经交卷了：64个GPT-5.6用1小时证明50年猜想|ethan|世纪|图论|定理|数学家

7月10日上午，OpenAI研究员Ethan Knight在X平台扔出一条推文，把AI圈和数学圈同时点着了：

"昨天，我们刚把GPT-5.6 Sol Ultra向所有用户全面开放。今天，我们要宣布：它用64个子智能体，在不到一小时内，给出了那道悬空近50年的'循环双覆盖猜想'（Cycle Double Cover Conjecture）的完整证明。"

发推的人是Ethan Knight，OpenAI研究员，之前在xAI做强化学习。他没藏也没掖，第二条推文直接甩出两份PDF：一份是证明全文，一份是生成这份证明的完整Prompt。几小时后，他又追加一条：证明的Lean形式化版本也已开源。，署名GPT-5.6 Sol。

证明、提示词、可机器核验的代码仓库三件套，把"AI解出数学难题"这件事第一次配齐了完整证据链。

这条推文很快在X上跑起来：5.3k点赞、404转发、176回复、约124.5万次浏览。还在韩国参加ICML的Noam Brown（o1模型核心贡献者）隔着太平洋第一时间赶来力挺：

"这次和此前的Erdős单位距离问题不一样，不靠什么内部特供模型，靠公开能用的GPT-5.6 Sol Ultra就把活儿干了。"

一道挂了50年的题

"循环双覆盖猜想"听起来拗口，其实不复杂。

把一张图想象成地铁图：站点是顶点，轨道是边。一条"圈"就是从某站出发、沿轨道绕一圈再回到起点的闭合路径。猜想问的是：能不能找出一批圈，让每一段轨道恰好被两个圈盖住？给每条轨道铺上两层环路，谁也不多，谁也不少。

这道题最早由匈牙利数学家George Szekeres在1973年提出，1979年由Paul Seymour独立重提。半个世纪以来，它一直挂在维基百科"未解决数学问题"列表上，是图论最重要的开放问题之一。Wolfram MathWorld直到2026年7月10日，标注的状态还只是"open"。

而GPT-5.6 Sol Ultra给出的，是一份三页的PDF证明。

比起"AI解出了难题"，我更感兴趣的是"AI怎么解的"。

它没有一头扎进图里去找圈——对一张组合爆炸级别的图来说那基本是无底洞。它换了个更聪明的思路：先把"找圈"转化成"贴标签"。

整个证明分四步：

• 归约。把任意无桥图归约成"三次图"（每个顶点恰好连三条边），战场瞬间缩小。
• 贴标签。用图论里大名鼎鼎的"无处为零的8-流定理"，给每条边贴上一个非零的"三位二进制标签"。这三位标签在每个顶点处必须能彼此抵消。
• 扩展标签。把每条边的一个标签扩展成两个标签，目标是让同一个标签在每个顶点附近要么不出现，要么恰好出现两次。这样一来，相同标签的边会自动组成圈。
• 全局协调。同一条边连接两个顶点，两端给的标签必须一致。GPT-5.6把这个协调问题转化成线性方程组，再用对偶空间和奇偶性证明方程组一定有解。

翻译成大白话：AI没有去硬找圈，而是设计了一种特殊的边标号方法，让圈自己从标号里"长出来"。

曼彻斯特大学数学家Thomas Bloom是第一批公开评价这份证明的人。他的原话很有意思：

"这是一个非常漂亮的证明，简洁、基础，没有用任何花哨工具。说实话，如果当年有人想到，20世纪80年代就能做出来。"

他随后解释了一个关键区别：人类数学家试一种自然方法失败，多半就放弃了；AI不会因此丧气，它会一直试各种细微变化。

但Bloom也泼了盆冷水：这份证明目前还没经过正式同行评审。历史上，循环双覆盖猜想已经出现过多次所谓"证明"，过去几年arXiv上也有不少宣称完成证明的论文，后来均被数学界发现存在漏洞。

更微妙的是，OpenAI公布的证明文档里，对F₃₂特征的描述有学者指出存在矛盾。这些都需要未来几周到几个月，由图论专家们一行一行审过。

所以我现在的态度是：先别急着下"AI解开50年数学难题"的定论，让子弹再飞一会儿。

比起证明本身，OpenAI这次公开的Prompt才让AI从业者集体坐不住。

整套提示词大约700个英文字符，核心思路不是"教AI怎么做"，而是"告诉AI什么叫做完了"。具体有四条原则值得抄作业：

不写解题步骤，但要写清楚"什么叫解完"。复杂任务的路径你事先根本不知道，硬写SOP反而是错的。

定义、范围、边界情况，一次性说清。什么是图、什么是桥、什么是圈、平行边是否允许、无边图怎么算，全部提前钉死。

不光说什么算答案，还要说什么不算答案。比如"只证明某些特殊图类不算"、"覆盖但部分边不是恰好出现两次也不算"，提前堵住模型偷懒的路径。

复杂任务不要固定分工，动态搜索加独立审查。最多调用64个智能体，但不是规定"10个走A路线、10个走B路线"，而是先建方法组合库，再根据实际进展动态调整。还专门安排了"对抗性智能体"负责找漏洞。

最让人拍案的设计是：每个子agent回来时必须带具体引理、方程、构造或反例，不能只汇报"有进展"。如果很多智能体都挤到同一种方法上，就把一部分重新分配；如果某条路线卡在同样难的引理上，就标记为"受阻"，除非出现新机制，否则不继续堆算力。

系统原本预留了8小时计算时间，最终只用了1小时就交卷了。

历史性的一刻，但不是"AI赢了"

很多媒体在用"AI击败数学家"这种标题，但更准确的描述应该是：这是大型语言模型第一次独立产出了一道维基百科收录的、悬空数十年的开放数学难题的完整证明。

注意关键词是"独立"。

此前AI在数学领域最出名的两次突破——DeepMind的"帽子集合问题"和Erdős单位距离问题，本质上都是人类数学家和AI协同完成，人类提供方向感，AI提供算力。GPT-5.6 Sol Ultra这次交出的PDF，署名只写了"GPT-5.6 Sol Ultra"。这是模型第一次被当成证明的"作者"，而不是工具。

但我们也得冷静。

一方面，OpenAI把PDF挂在公司CDN上，和正式发在期刊上、被同行评审接受的论文，是完全不同的事。历史上无数"漂亮证明"都倒在了这一步。

另一方面，整个证明用的数学工具——8-流定理、线性代数、归约——大多是几十年前就成熟的东西。AI的优势未必在于"提出全新概念"，而在于它拥有远超人类的计算耐心和持续尝试各种细微变化的能力。

某种意义上，这就像一台永远不会累的"超级研究生"。