作者：Lei阅读 --

短视频说"AI 一小时证明了 50 年数学悬案"——我把 OpenAI 那两份 PDF 读了，真实故事更精彩

2026 年 7 月，"GPT-5.6 一小时证明循环双覆盖猜想"刷屏短视频。事实核查：事件为真，但"证明了"三个字说早了——现在的准确状态是"机器生成了一份证明，人类正在核验"。这篇先用能手画的小例子讲透这个 50 年悬案本身（圈、桥、snark），再逐页拆 OpenAI 发布的两份一手 PDF：3 页的证明走了哪四步，那份比证明更值得读的 2 页提示词里藏着哪些多代理工程设计。结尾是一张"视频说法 vs 核实结果"对照表，以及一个漂亮的对偶：费马大定理是人类已证、等机器核验；这次是机器生成、等人类核验。

数学AI图论事实核查LLM

抖音上一条视频这样开场：“7 月 11 日，GPT-5.6 仅用 1 小时，就证明了困扰数学界 50 年的’循环双覆盖猜想’！“然后配上 y=f(Wx+b)y = f(Wx+b) 和 Φ=PCA(X)\Phi = \mathrm{PCA}(X) 两条公式，解释说 AI 是”把数学问题转化为向量、通过多层网络提取特征”。这条视频一半是真的：事件确实发生了，而且是 AI×数学这几年最值得记住的事件之一。但两处关键的地方它讲错了：第一，“证明了”三个字目前还不能说——准确的状态是”生成了一份正在被人类核验的证明”；第二，那两条公式与这次事件的机制毫无关系。真实的故事全部写在 OpenAI 公开的两份 PDF 里——一份 3 页的证明，和一份比证明更值得读的 2 页提示词。这篇把它们拆开讲。

一、先把这个 50 年悬案装进脑子——用能手画的例子

循环双覆盖猜想（Cycle Double Cover Conjecture，下称 CDC）的陈述只有一句话：

每个有限的、无桥的图，都存在一族圈，使得每条边恰好被覆盖两次。

逐词拆开。图：一堆点（顶点）和连接点的线（边）。圈：从一个点出发沿边走、不重复经过顶点、最后回到起点的闭合路线。桥：删掉之后图会断成两块的边。比如下面这个图，中间那条边就是桥：

graph LR
    A((A)) --- B((B))
    B --- C((C))
    C --- A
    C ---|桥| D((D))
    D --- E((E))
    E --- F((F))
    F --- D

为什么必须”无桥”：圈是闭合路线，走出去还得走回来——而桥是两块区域之间唯一的通道，任何闭合路线要么不过桥，要么过了就回不来。所以桥不在任何圈上，永远不可能被圈覆盖。“无桥”不是附加条件，是这个问题能成立的最低门槛。

两个手算例子，钉死”双覆盖”的感觉：

例 1：三角形。 三个点两两相连，本身就是一个圈。把这个圈用两次——猜想允许同一个圈重复计入（多重集）——每条边恰好被盖两次 ✓。

例 2：立方体。 把立方体看成图（8 个顶点、12 条棱），它的 6 个面各是一个四边形圈。数一数：每条棱恰好属于 2 个面。所以”6 个面的边界圈”就是一份现成的双覆盖 ✓。这不是巧合——所有能画在平面上不交叉的图（平面图），其”面的边界”天然构成 CDC。这正是猜想已被解决的第一类情形（Jaeger 观察到的，写在这次证明 PDF 的引言里）。

那难在哪？ 难在画不进平面的图。图论里有一类叫 snark 的捣蛋鬼：每个顶点恰好连 3 条边（立方图）、无桥、但无法用 3 种颜色给边染色使同顶点的边异色。最有名的是 Petersen 图（10 个顶点，画出来像五角星套五边形）。证明 PDF 引用的 Jaeger 定理说：如果 CDC 有反例，最小的反例必然是 snark——而 snark 恰好把”面边界”、“3-边染色拆圈”这些简单套路全部废掉。从 Szekeres 1973 年、Itai–Rodeh 1978 年、Seymour 1979 年各自独立提出（Tutte 也在通信中提过——这次证明的参考文献里有一条罕见的”[Tutte] personal correspondence with H. Fleischner, July 22, 1987”），到 2026 年，Open Problem Garden 一直把它列为图论最重要的开放问题之一。

二、7 月 10 日实际发生了什么——事实版时间线

2026 年 7 月 10 日，OpenAI 在其 CDN 上发布两份文档（报道见 The Decoder，短视频里的”7 月 11 日”是时差内的转述）：

  1. 证明本体（cdc_proof.pdf）：标题《A Proof of the Cycle Double Cover Conjecture》，署名”OPENAI”，正文加参考文献一共 3 页。文中的 AI 使用声明原文：“The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol).”（证明完全出自 GPT 5.6 Sol Ultra，成文由 Codex 完成。）
  2. 完整提示词（cdc_prompt.pdf）：喂给模型的原始任务书，2 页。

据 OpenAI 的说法与各方报道，模型动用了 64 个并行子代理，在约 1 小时内产出证明。消息发布后一小时内冲上 Hacker News 首页。

那 3 页证明走了四步（这里只给骨架，感受一下它的”人类风格”）：

  1. 约化：标准手法，把一般无桥图约化到”每个顶点恰 3 条边”的立方图（引 Jaeger）；
  2. 借力人类定理：由 Kilpatrick（1975）与 Jaeger（1976）独立证明的结果——每个无桥图都有取值于 Γ=F23\Gamma = \mathbb{F}_2^3 的处处非零流（等价于 Tutte 群流理论中的”无零 8-流”）——拿到每条边一个非零向量标签，且每个顶点处三条边的标签之和为零；
  3. 关键新步骤：把”每边一个向量”改造成”每边一个二元集合 PeP_e“，使得任何向量在每个顶点周围出现 0 次或 2 次（文中 Lemma 2.1——作者自己点明这是”3-边染色的松弛版”：染色做不到没关系，松弛版够用）。出现 0 或 2 次意味着什么？意味着每个向量对应的边集在每点的度数是 0 或 2——这正是”一堆不相交的圈”，双覆盖随之成立；
  4. 收尾：这个改造归结为一个 F2\mathbb{F}_2 上的线性方程组是否有解，用对偶性论证——最后一步的杀招朴素得动人：任何一条边在求和中恰好出现两次，而在 F2\mathbb{F}_2 里 2=02 = 0。“每条边算两次”这个猜想主题，在证明最深处以模 2 的形式又出现了一次。

值得注意的是：第 2 步的积木全是人类几十年前造好的（8-流定理是 1970 年代的成果），新意集中在第 3、4 步的组装。这既是它可信的理由（站在被反复检验过的定理上），也是数学家审查的焦点（组装处最容易藏错）。

三、那份提示词，比证明更值得读

对 AI 工程感兴趣的读者，真正的金矿是第二份 PDF。这不是”请证明 XX 猜想”一句话，而是一份精密的作战手册。六个设计点：

1. 把任务定义到零歧义。 开篇先用精确语言定义图、桥、圈、双覆盖——精确到”两条平行边构成长度为 2 的圈”、“多重集按重数计每条边恰出现两次”。不给模型任何在定义上打滑的空间。

2. 那句被热议的指令：“Assume for purposes of this task that a complete affirmative proof exists.”（就本任务而言，假设完整的肯定性证明存在。）这不是让模型作弊，而是关闭一条退路：不许花算力怀疑”这题是不是根本无解”，也不许上网查到”这是开放问题”就摊手放弃——提示词后文明确禁止”以’CDC 是开放问题’作为回答”。

3. 反”部分学分”条款。 明确列出什么不算数：特殊图类的证明、有些边盖两次以外的覆盖、归约到另一个未证猜想、有限规模的计算验证……全部不收。只收完整证明。

4. 64 个子代理的调度启发式。 不许静态分工（“N 个代理做策略 X”是被点名禁止的），而是：初期保持路线多样且互相独立、防止代理集体涌向”优雅但不完整”的约化；按数学思想而非表面措辞给路线分组；停滞的路线标记封锁，除非出现实质新机制不再投人；多条互不相容的路线并行养到足够成熟再交叉授粉。

5. 对抗代理与”routine 禁令”。 全程有专职找茬的代理，携带一张具体的审计清单：检查”恰好两次”的重数、伪装成圈的重复边闭迹、约化过程偷偷引入的桥、对等价表述的循环论证……并且明文规定：不接受”这一步是 routine（例行公事）“这种糊弄，每个子命题必须给出具体引理、构造或反例。

6. 最有戏剧性的一条：“Spend at least 8 hours on this before even thinking of returning or giving up.”（至少干满 8 小时再考虑返回或放弃。）——结果按报道，它 1 小时内就带着证明回来了。

现在可以回头给短视频勘误了：视频里的 y=f(Wx+b)y = f(Wx+b)（神经网络前向传播）、Φ=PCA(X)\Phi = \mathrm{PCA}(X)（主成分分析），是”AI 科普”的万能模板公式，与这次事件的机制无关。GPT-5.6 不是”把猜想转化为向量提取特征”，而是在语言层面做多路线证明搜索 + 对抗式审计——上面那六条就是它的真实”原理图”。视频提出的问题（“真理解还是超级模式匹配？“）是个好问题，但它给出的原理是错的；而讽刺的是，真实机制比模板公式有意思得多。

四、“证明了”什么时候才能说？——核验方向的一次反转

短视频最需要修正的就是”证明了”这个完成时。三个事实：

  1. CDC 历史上已经”被证明”过不止一次——多份声称的证明（包括发在 arXiv 上的）后来被发现有漏洞或被撤回。所以数学社区对任何 CDC 证明的默认态度是先怀疑。
  2. 这份证明未经同行评审，是以”公开 PDF + 全网围观”的方式接受检验的：HN 首页、数学家逐行读、维基百科的猜想词条已把它作为”claimed proof”收录。
  3. 终审标准其实已经备好了：形式化验证。把这 3 页证明翻译进 Lean 或 Rocq，让机器逐步核验每一个推理——通过了，才是板上钉钉。

这里有一个漂亮到值得单独记住的对偶。上一篇《种子公式全录（下）》里写过：Wiedijk 百定理清单 99/100 已被机器核验，唯一的空格是费马大定理——人类已证、机器核验中（Buzzard 团队的五年 Lean 项目）。而 CDC 这次恰好相反：机器已证（声称）、人类核验中。两支箭方向相反，跨的是同一道鸿沟：

生成方核验方状态
费马大定理人类（Wiles 1995）机器（Lean，进行中）人类共识已定，机器背书未完
循环双覆盖猜想机器（GPT-5.6，声称）人类（数学界，进行中）机器已交卷，人类批改未完

一个怀疑的读者还会追问：就算证明成立，功劳算 AI 的还是提示工程的？ 这个问题没有便宜的答案。提示词确实喂了框架（流的形式化视角、审计清单、调度策略），HN 上就有人拿它类比 GPT-4 时代的”think step by step”——今天要手把手喂的脚手架，往往是下一代模型的内置能力。但提示词没有喂证明本身：Lemma 2.1 的松弛染色和最后的对偶论证不在任务书里。“喂到什么程度算 AI 自己证的”——这条界线本身，就是这次事件留给整个行业的新题目。

五、视频说法 vs 核实结果对照表

视频说法核实结果判定
”7 月 11 日”两份 PDF 发布于 2026 年 7 月 10 日（美国时间）基本准确（时差）
“GPT-5.6”GPT-5.6 Sol Ultra 出证明，Codex（配 GPT-5.6 Sol）成文准确，缺细节
”仅用 1 小时”报道称约 1 小时内、64 个并行子代理（提示词还要求”至少干 8 小时”）基本准确
”困扰数学界 50 年”Szekeres 1973 年提出，至今 53 年准确
”证明了”给出了一份正在被核验的证明；该猜想历史上有多份翻车前科，终审待形式化验证说早了
”y=f(Wx+b)y=f(Wx+b)、PCA 提取特征发现规律”实际机制是多代理证明搜索 + 对抗审计，与前向传播/降维公式无关不成立

一句话带走：这次事件真正的里程碑，不在”AI 快过人类”，而在角色互换——五十年来第一次，是机器交卷、人类批改。至于卷子能不能批过，答案不会来自热搜，会来自某一天一行绿色的 Lean 编译通过提示。到那天，这个猜想就该从”猜想”改叫”定理”了——不管署名栏里写的是谁。

参考来源

一手材料

报道与讨论

猜想背景

本站相关