AI能证明数学猜想吗？GPT-5.6事件真相与大模型能力边界

一则轰动数学圈的传闻

近日，一份标题为《GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture》的PDF文档在Hacker News上引发热议，短时间内获得125个点赞和超过110条评论。文档声称，OpenAI某个版本的模型（GPT-5.6 Sol Ultra）成功给出了图论中著名的**循环双重覆盖猜想（Cycle Double Cover Conjecture，CDC）**的完整证明。

这一说法如果属实，将是AI在纯数学领域的里程碑式突破。然而，正如社区讨论所揭示的，事情远没有标题那样简单。本文将从这一事件出发，梳理其背后的技术真相，并探讨大语言模型在数学证明上的真实能力边界。

循环双重覆盖猜想究竟是什么

一个悬而未决的经典难题

循环双重覆盖猜想由Seymour和Szekeres在1970年代独立提出，是图论中最著名的未解问题之一。值得注意的是，Paul Seymour正是图论领域的巨擘，他与Robertson、Sanders、Thomas在1997年给出了四色定理的第二个计算机辅助证明，并深度参与了图子式理论（Graph Minor Theory）的奠基工作——Robertson-Seymour定理本身就是20世纪图论最深刻的成就之一。CDC猜想从一开始便诞生于顶级数学家的视野之中，其难度可见一斑。

其核心命题大致为：对于任何一个无桥连通图（bridgeless graph），都存在一族环（cycle），使得图中的每一条边恰好被这些环覆盖两次。

要理解这一命题的深意，需要理解图论中"环"与"覆盖"的含义。图论中的"环"（cycle）是指起点与终点相同、不重复经过节点的路径，而"覆盖"则要求图中每条边都被纳入至少一个环中。CDC猜想要求每条边恰好被覆盖两次，这个"恰好两次"的对称性要求使问题极为精妙。与四色定理类似，CDC猜想的表述极度简洁，却对应着深层的组合与拓扑约束，这类"易述难证"的性质正是图论顶级难题的共同特征。

表述看似简洁，却抵抗了数学家近半个世纪的攻克。CDC猜想的难点根植于图论的深层结构。所谓"无桥连通图"，是指删去任意一条边后图仍保持连通性的图，桥的存在会导致覆盖结构不可能满足对称性要求。

CDC猜想与彼得森图（Petersen Graph）、Snark图族的研究密切相关——这一关联值得深入说明。彼得森图是图论中最重要的"反例图"之一，构造于1898年，仅有10个顶点和15条边，却以极小的规模展现了图论中几乎所有"困难性质"的原型。Snark图族是彼得森图的推广：它们是三正则（每个节点恰好连接三条边）、边着色数为4（无法用三种颜色对所有边着色使相邻边颜色不同）的连通无桥图。数学家已证明，若CDC猜想对所有Snark图成立，则对所有无桥连通图自动成立。Snark图的存在正是CDC猜想难以被归纳法突破的关键原因——目前已知无限多的Snark图存在，使完全枚举验证成为不可能，而Snark图族因此构成了该猜想的"最难核心"。

此外，CDC猜想还与拓扑图论中的曲面嵌入理论有深刻联系，这一联系揭示了猜想更深层的数学意涵。任何嵌入在可定向曲面（如球面、环面）上的图，其面边界自然构成一个循环双重覆盖——每条边恰好属于两个面的边界。这一观察将CDC猜想转化为一个深刻的问题：是否每个无桥连通图都在结构上等价于某个可定向曲面嵌入图？这种等价性若成立，意味着离散组合结构可以被连续拓扑结构完全捕获，是数学中"离散与连续统一"这一宏大主题的具体体现。因此，猜想本质上在追问一种拓扑结构是否可以代数化地刻画。它与图论中诸多重要结构——Snark图、四色定理、嵌入理论——存在深刻关联，时至今日，它依然是公认的开放猜想，没有任何被数学界认可的完整证明。

为什么它如此难以被证明

正因CDC猜想至今未被人类数学家攻克，任何声称"给出完整证明"的成果都应接受最严格的审视。数学证明的验证门槛极高——不是逻辑"看起来通顺"就够了，每一步推导都必须经得起形式化检验。四色定理的计算机辅助证明（1976年）曾让人短暂乐观，但CDC迄今仍无类似突破。历史上不乏"外观严谨"却暗藏致命漏洞的证明尝试，最终在同行评审中落败。

一个著名的反面教材是1995年之前的费马大定理历史：怀尔斯在1993年提交的第一版证明即被发现包含一个关于欧拉系统（Euler systems）的严重漏洞，耗费一年多时间才与学生Taylor联合修补完成。这说明即便顶级数学家的证明也可能在看似严密的外表下隐藏致命缺陷，遑论LLM的输出。

社区的质疑与事件真相

大概率是恶搞或AI幻觉产物

从Hacker News的评论氛围来看，社区对这份文档的主流判断是高度怀疑，甚至直接认定为玩笑或AI幻觉的产物。几个关键疑点值得注意：

模型名称本身就是破绽。 "GPT-5.6 Sol Ultra"完全不符合OpenAI的任何官方命名规范，带有明显的调侃痕迹。传播方式也严重失格。 如果AI真的证明了半世纪未解的数学猜想，这将是需要顶级期刊同行评审、多位数学家反复验证的重大事件，绝不会以匿名PDF在论坛流传的形式首发。

更根本的问题在于：大语言模型生成的"数学证明"存在结构性缺陷，这一缺陷根植于LLM的统计学本质。大语言模型通过在海量文本上进行自监督预训练，学习的是token序列的条件概率分布，本质上是一个统计压缩模型。在数学推导场景中，模型学到的是"合法数学文本的语言模式"，而非"逻辑推导的有效性判断"。关键的错位在于：一个错误的证明可以在语言层面与正确证明的分布完全重叠，模型无法通过统计特征区分两者。这导致模型倾向于生成"在统计分布上最像正确证明"的输出，而非"在逻辑上真正成立"的证明。更深层的问题是：对于顶级未解猜想，训练语料中根本不存在正确证明的文本，模型只能依赖对相关数学子领域的"插值"与"外推"，而数学推理对于微小的逻辑错误极为敏感——一个错误的引理引用可能使整个证明结构崩塌，但在语言层面看起来依然流畅自洽。

这导致几类典型失效模式：一是**"引理捏造"——模型会援引实际不存在或内容被篡改的定理；二是"跳步幻觉"——在复杂推理链中省略关键步骤，却以"显然可得"等措辞掩盖；三是"结构模仿"**——生成的证明在排版和用语上高度专业，但逻辑关系实为循环论证。对于顶级未解猜想，训练数据中根本不存在正确证明的参照，模型只能在分布外进行高风险的"外推"，幻觉风险呈指数级上升。这正是AI幻觉在数学场景下的典型表现，也解释了为何模型可能编造引理、跳过关键步骤，或在形式上模仿证明结构却缺乏实质内容。

形式化验证的缺失是核心疑点

真正可信的AI数学证明，通常需要配合形式化证明系统（如Lean、Coq、Isabelle）进行机器验证。这类系统的底层基础是马丁-洛夫类型论（Martin-Löf Type Theory），其核心思想来自著名的Curry-Howard同构——每一个数学命题被表示为一个"类型"，而该命题的证明则是该类型的一个"值"。证明者需要将每一步推导写成形式化代码，系统在编译时自动检查类型是否匹配，任何逻辑漏洞都会导致类型检查失败，等价于编译错误，从根本上杜绝了幻觉。这一机制的可靠性已由历史验证：2005年Gonthier团队用Coq完成四色定理的完整形式化，将1976年原始计算机辅助证明中需要人工审查约1500种构型的不确定性彻底消除，把验证过程转化为完全机械化的计算。Lean的数学库Mathlib目前已收录超过15万条经过机器验证的定理，为AI提供了可靠的知识基础。

DeepMind的AlphaProof（2024年）正是以Lean 4作为验证环境，将大语言模型与形式化系统深度结合，其架构借鉴了AlphaGo的蒙特卡洛树搜索框架：模型将"证明状态"替代"棋盘状态"，每次选择一个证明策略（tactic），Lean立即返回该步骤是否合法的二值反馈，成功的步骤使证明树向目标推进，失败则触发回溯。这一"生成-验证"闭环的核心优势在于奖励信号的绝对可靠性：数学证明步骤的有效性如同围棋胜负一样客观，不存在模糊地带，从根本上避免了语言模型"听起来正确就被接受"的失效模式。近年来，这类工具才是AI辅助数学研究的严肃方向——它们生成的证明可以被计算机逐步检查，从根本上杜绝幻觉。

单纯由LLM输出的自然语言"证明"，若未经形式化验证，其可信度几乎为零。这也是本次GPT-5.6事件最核心的疑点所在。

AI真的能做数学证明吗

从辅助工具到自主推理的漫长道路

抛开这一具体事件，AI在数学领域的真实进展本身值得认真对待。DeepMind的AlphaProof和AlphaGeometry 2曾在国际数学奥林匹克（IMO）中达到银牌水平，能够解决相当有难度的竞赛题目。这类系统的共同特点是：将神经网络的直觉能力与符号推理引擎的严格性深度结合。

但需要清醒认识到，IMO竞赛题与未解的世界级猜想之间存在本质差距。IMO题目在设计上遵循严格约束：题目必须在中学数学框架内可解，解题所需的知识边界明确，且出题委员会已掌握标准解法。这意味着AI在IMO上的成功本质上是一个"有界搜索问题"——在已知工具集内寻找路径。更关键的是，IMO题目在出题时已经有了已知答案和验证路径，AI系统本质上是在一个"可达解空间"内搜索。

而世界级未解猜想（如CDC猜想、黎曼猜想、P vs NP）的特征恰恰相反——它们往往需要发明全新的数学对象或框架，需要创造性地扩展数学的表示空间本身，而非在已有空间内搜索。怀尔斯证明费马大定理（1995年）时引入了模形式与椭圆曲线的深刻联系，Perelman证明庞加莱猜想时发明了Ricci流手术技术——这些都是真正意义上的数学创造，而非现有工具的重新组合。怀尔斯的核心突破是证明了谷山-志村猜想的半稳定情形，而这一联系本身在费马大定理的历史研究中长期不可见，是真正意义上的数学创造。历史上许多突破耗费了数年乃至数十年，并调用了当时尚未与该猜想关联的数学工具。

当前AI系统在IMO上的成功，主要依赖对已有数学结构的高效搜索与组合，而非创造性地开拓新领域。这一能力距离独立攻克CDC级别猜想，仍存在本质性的方法论鸿沟。目前没有任何AI系统展现出独立攻克顶级未解猜想的能力。

值得一提的是，2023年DeepMind旗下另一项目发布了一个有趣的正面案例：AI系统在组合数学中发现了超越人类已知下界的Cap Set构造，被发表于《自然》杂志。但这一成果的性质是"在已知框架内发现人类遗漏的构造"，与"独立创造新数学框架来证明未解猜想"仍属于不同量级的挑战。

大模型的能力边界在哪里

通用大语言模型（如GPT系列）在数学场景中的真实强项包括：

归纳整理已有知识，帮助研究者快速消化文献
提供证明思路的初步灵感，充当头脑风暴伙伴
辅助形式化翻译，将自然语言证明草稿转化为Lean等语言

而其短板同样清晰：无法自我验证逻辑正确性、容易在长链推理中积累错误、缺乏对"什么是真正新颖数学思想"的判断能力。将LLM视为能"一键证明猜想"的黑箱，是对当前技术能力的严重误判。

事件背后的启示

这起GPT-5.6事件，无论是恶搞还是误传，都折射出当下AI讨论中的一种普遍浮躁。在AI能力快速演进的背景下，人们既容易过度神化，也容易在真假难辨的信息流中迷失方向。

对于技术从业者和普通读者而言，这一事件提醒我们坚守三条基本判断力：非凡的主张需要非凡的证据，尤其是在数学这样容不得半点含糊的领域；形式化验证是衡量AI数学成果可信度的分水岭；理性看待AI的能力边界，既不盲目吹捧，也不全盘否定。

真正值得持续关注的，是AlphaProof这类将AI与形式化系统深度结合的严肃研究方向。它们或许不会以"一夜证明世纪难题"的耸动标题出现，但正在踏实地推动AI辅助数学研究的真实进步。当有一天AI真的攻克重大猜想时，它一定是经过反复验证、被数学界共同认可的成果——而不是论坛上流传的一份匿名PDF。