GPT-5.6 Sol Ultra 1 小时证明 60 年未解的图论猜想
7 月 10 日 Hacker News 头条刷屏，OpenAI 旗下的 GPT-5.6 Sol Ultra 用不到 1 小时证明了一个困扰数学界 60 多年的猜想——Cycle Double Cover Conjecture（循环双覆盖猜想，简称 CDC）。343 分、278 条评论，是本周 AI × 数学赛道最大的新闻。(HN 讨论)
但看完整条帖子和评论区，你会发现这个"证明"的故事远比标题复杂得多。
什么是 CDC 猜想
Cycle Double Cover Conjecture 说的是：每一个无桥连通图（所谓"桥"就是删掉之后图就不连通的边），都存在一组边不相交的圈，让图里每条边都恰好被覆盖两次。
这个猜想是图论里出名的"群论等价形式"。如果成立，能直接推导出 Snark 无穷族不存在、双环覆盖图的强结构性质，是图论和代数组合学交叉地带的一个长期公开问题。1970 年代由 Seymour 等人开始系统研究，至今没有任何通用证明。
换句话说，60 年来数学家一直在尝试但没有给出一般情形的证明。Erdős 悬赏名单上常年有它的影子。
这次 GPT-5.6 干了什么
负责这次解谜的是 OpenAI 内部一位叫 Eknight 的研究员，他在 X 上公开了完整过程。(X 公告)
核心操作并不复杂：
- 64 个子 agent 并行启动。每个 agent 拿到同一个 prompt，独立尝试在图论的标准框架内构造满足 CDC 条件的圈覆盖。
- 每个 agent 被要求"假设完整肯定证明存在"。这是关键 prompt 技巧。它不是给数学条件，是给模型一个"心理前提"：当成它存在，你的工作就是把它找出来。
- 每个 agent 被要求"至少投入 8 小时思考再返回"。这是防放弃 prompt。模型有强烈的"快速收敛到结论"的倾向，告诉它"不许早放弃"能显著延长探索。
- 不到 1 小时（因为 64 路并行），所有 agent 中至少有 1 路返回了一个可读、简洁的证明文本。
OpenAI 同时把完整 prompt 公开成 PDF（cdc_prompt.pdf），让社区可以复现。这是相当透明的做法。
算力账
HN 评论区有人按 64 个 agent 跑满 1 小时做了估算（riknos314 的表格）：
- GPT-5.5 low：9.2M 输出 token，约 275 美元
- GPT-5.5 base：12.7M 输出 token，约 380 美元
- GPT-5.5 high：16.1M 输出 token，约 485 美元
- Sol Fast（Cerebras 加速）：172.8M 输出 token，约 13000 美元
如果走普通 GPT-5.5 high 跑满 1 小时，整件事的成本不到 500 美元。对一次可能的"世纪数学突破"来说，这价格便宜得像在便利店买咖啡。
真正的争议：完整输出没公开
但接下来就是数学界开始吵架的部分。
质疑 1：没有 Lean 机械化验证。 现在前沿数学圈对 LLM 证明的"金标准"是用 Lean、Coq、Isabelle 这类证明助手把每一步重写一遍，让机器确认无懈可击。这次 GPT-5.6 给出的证明完全没有走 Lean，只附了一句"the proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex"。
质疑 2：图论目前根本无成熟 Lean 库可用。 评论区 emil-lp 提了一个关键事实：Lean 里最强的图论库是 Graphlib，但它"真的还没准备好承接研究级图论定理"。换句话说，不是 OpenAI 不想做机械化验证，是目前 Lean 生态承载不了这个级别的图论证明。这是一个比 GPT-5.6 证明本身更值得讨论的问题。
质疑 3：证明很短、且没有用到 30 年内的新数学。 HN 用户 Jweb_Guru 提了一个尖锐观察："这份证明非常非常短，且没有用到过去 30 年发展的任何数学工具。" 这不必然意味着错误，很多经典证明就是简短的，但在缺乏机械化验证的当下，发布是冒险的。
质疑 4：完整推理过程没公开。 OpenAI 公开了 prompt，但没有公开 64 个 agent 的完整轨迹。HN 用户 edflsafoiewq 指出："我们只看到最终写好的、抛光过的证明，看不到它怎么被一步步构造出来的。讽刺的是，这种'藏在帽子里抽出来'的做法，恰恰是数学写作长期被批评的毛病。只不过这次从帽子里掏出来的是 LLM。"
质疑 5：survivorship bias。 这次 64 个 agent 里有 1 个跑通了，但没有人知道 63 个失败的 agent 各自卡在了哪一步。可能 OpenAI 之前还试过几百次、几千次其他图论猜想都没成，这次只是碰巧撞上了 CDC。也可能不是，但没有足够数据判断。
对比 1 年前的 Erdős 平面单位距离问题
去年，OpenAI 用类似的方式让 LLM 解开了 Erdős 平面单位距离问题（Erdős problem 90），证明满足"距离为 1 的点对"的最大值的渐近下界。(HN 旧帖)
那次 OpenAI 极其谨慎：先在 Lean 里跑通机械化验证，再发表，且对证明涉及的数学工具年代也做了详细交代。两次对比，这次的 CDC 公告明显更激进。
数学社区的疑问因此更尖锐：CDC 是更难的猜想（平面单位距离问题本质是渐近估计，CDC 是结构存在性），OpenAI 反而在更难的问题上采取了更弱的验证标准？
我的一些看法
把这件事说成"AI 已经能解数学猜想"和把它说成"AI 套话瞎编"都是错的。更准确的说法是：
- LLM 在 agent 框架下能做"启发式数学搜索"，它能比单个人类数学家更快尝试更多种构造方向。
- 这种搜索的产出可能有效也可能无效，目前的区分机制是人类专家复核 + Lean 验证。
- CDC 这次的产物很可能"大部分对"。简短、用了已知工具、没有显示"AI slop 证明"常见的循环论证或无中生有。但离被数学界接受还差 Lean 这一步。
- 真正的风险是：如果数学界以后被 LLM 证明"灌水"，而没有足够强的事后验证基础设施，整个领域会进入"高噪声时代"。
OpenAI 这次主动公开 prompt、选择较难的猜想、并且不把结论吹成"数学已死"，这些动作本身是负责任的。但社区没拿到完整输出这件事，下一步必须补齐。
几个值得记下来的事
- 防放弃 prompt（"假设完整证明存在 + 至少投入 N 小时"）是 LLM 数学任务的有效脚手架。这次它是核心设计，不只是细节。
- 64 路并行 × 1 小时 的成本结构意味着：未来每个数学猜想都可以被"廉价地扫一遍"。以前数学家没空去试的小猜想，机器可以扫。
- Lean 工具链对图论的不成熟是当下最被低估的瓶颈。等 Graphlib 或类似库成熟，会有一波"LLM 证明 × Lean 验证"的联合成果集中爆发。
- 公开 prompt + 隐瞒完整轨迹 的策略可能成为新的标准做法。它符合"可复现性"要求（别人可以用相同 prompt 重跑），但不利于事故分析。这一点值得未来建立新的规范。
如果你是做 LLM 应用的，这个 prompt 模式值得抄。"假设答案存在 + 投入时间 + 多路并行"三件套是当前 agent 在硬问题上的最佳实践。
如果你是做数学工具的，图论的 Lean 库是金矿。一旦把"边的圈覆盖""桥""块结构"这些基本概念在 Lean 里建好，验证 LLM 证明就会从"人工逐行对照"变成"一键编译"。
如果你是做学术的，短期内的判断标准还是"有没有 Lean 验证"，没有机械化的数学证明，目前请先存疑。
