GPT-5.6 Sol Ultra 用不到一小时给出循环双覆盖猜想完整证明

OpenAI 宣布，旗下 GPT-5.6 Sol Ultra 模型在不到 1 小时内生成了循环双覆盖猜想的完整证明。循环双覆盖猜想由 George Szekeres 和 Paul Seymour 分别于 1973 年和 1979 年提出，核心问题是：任意无桥图中，是否都存在一组循环，使得每条边恰好属于两个循环。该问题长期被视为图论最重要的公开难题之一。

据 OpenAI 研究员 Ethan Knight 介绍，模型在执行过程中最多同时调用了 64 个并行子智能体，由主智能体动态调度。系统要求早期阶段保持路线多样性，让不同智能体分别尝试不同数学表示方法、代数思路与结构归纳。同时还设置了对抗智能体，专门负责寻找漏洞、边界情况与常见错误。提示词明确禁止联网搜索资料，并要求拒绝仅证明特殊情况或不完整证明。整个过程原本预留了 8 小时计算时间，最终只用了大约 1 小时。

OpenAI 公布的证明分为三步：首先将原猜想归约为三次图问题，随后借助 8-流定理进行处理，最后在 GF(3) 三元有限域上通过线性代数构造边标记，证明每条边能够恰好属于两个环。OpenAI 已将证明全文与提示词以 PDF 形式发布到自家 CDN，并强调整套证明由 AI 独立完成。

英国曼彻斯特大学数学家 Thomas Bloom 是最早公开评价的学者之一，称赞这份证明简洁、基础、方法并不复杂，甚至认为如果当年有人想到，20 世纪 80 年代就有可能完成。他指出，AI 最大的优势并非提出全新数学思想，而是拥有远超人类的计算耐心，会不断尝试各种细微变化，而人类数学家在一种方法失败后往往选择放弃。

不过 Bloom 也指出了明显问题：整篇证明没有引用任何已有文献，1983 年 Bermond、Jackson 和 Jaeger 的经典论文本应被引用却完全缺失。此外，证明尚未经过正式同行评审。历史上该猜想已经出现过多次所谓证明，其中部分在 arXiv 上发表的论文后来被发现存在漏洞甚至被撤稿。该证明也没有使用 Lean 等形式化证明工具进行机器验证，目前图论领域的形式化数学库也不足以支撑此类研究级定理。

据业内人士估算，按照 OpenAI 官方 Sol 定价，完成这次推理的成本约为 275 至 485 美元；若使用 Cerebras 平台运行，成本最高可能达到 1.3 万美元。如果最终通过验证，这将是大型语言模型首次独立解决一个被列入维基百科未解决数学问题列表的重要难题。此前 AI 在数学领域取得的重要成果，例如 DeepMind 在帽子集合问题上的研究以及 AI 在纽结理论方面的突破，都属于人类与 AI 协同完成，而非 AI 独立完成完整证明。图论专家预计将在未来数天至数周内对证明的每一个推导步骤进行严格审查。

要点

• GPT-5.6 Sol Ultra 在不到 1 小时内生成循环双覆盖猜想的完整证明，全程调用 64 个并行子智能体
• 证明将问题归约为三次图，借助 8-流定理与 GF(3) 有限域上的线性代数完成论证
• 证明尚未通过同行评审，历史上该猜想曾出现多次被证伪的证明尝试，数学界保持谨慎
• 学者 Thomas Bloom 认为证明简洁漂亮，但指出整篇证明没有引用任何已有文献
• 若最终通过验证，这将是 AI 首次独立解决一个被列入维基百科未解决数学问题列表的重要难题