GPT-5.6用一段十页提示词，关闭凸优化30年的复杂性缺口

2026 年 7 月 10 日，OpenAI 在自己的 CDN 上放出一篇 PDF，声称 GPT-5.6 Sol Ultra 用 64 个并行子代理、不到一小时，证明了图论里悬挂了 50 年的 Cycle Double Cover 猜想。数学界在震动与质疑中展开了审阅。六天后，UC Berkeley IEOR 教授 Phillip Kerger 把 OpenAI 公开的「CDC prompt」拿来，改造成了针对另一个问题的十页提示词，喂给 GPT-5.6 Sol Pro。148 分钟后，模型返回了一个凸优化下界的完整证明——一个他自己琢磨了一年、和 GPT-5.4/5.5 反复试都没能拿下的结果。

更关键的是，这个证明随后在 Lean 4 / mathlib 里通过了形式化验证。机器查证、可复现——这把结果从「AI 写了一段看着像对的论证」拉到了「任何一台装了 Lean 的机器都能重新跑一遍确认无误」的级别。

一个 30 年的「数学天窗」

要理解这件事的分量，得先回到 1996 年。

凸优化里有一个基本问题：给定一个定义在 $d$ 维单位球 $B_d$ 上的凸的、1-Lipschitz 的函数 $f$，假设你只能查询函数值 $f(\boldsymbol{x})$——没有任何梯度信息——最少需要多少次查询才能找到一个 $\varepsilon$-最优解？

这就是所谓的确定性零阶凸优化的 oracle 复杂度，记作 $Q(d, \varepsilon)$。这种「只能拿到函数值、拿不到梯度」的场景在现实中非常普遍：把物理实验、数值仿真、人类反馈当目标函数做优化时，梯度通常不可得，每次「问一次」都很贵。1996 年，Protasov 给出了一个只需要 $O(d^2)$ 次函数求值就够的上界算法——也就是说 $Q(d, \varepsilon) = O(d^2)$。

但下界这边几乎是空的。最强的已知下界只有 $\Omega(d)$，而且这个 $\Omega(d)$ 其实是从一个更强的「一阶 oracle 模型」（算法同时能拿到函数值和梯度）那里继承过来的。也就是说，整整 30 年，我们并不知道梯度到底帮不帮得上忙——因为函数值 only 和函数值+梯度这两个模型在 $d$ 这个维度上有完全相同的已知下界，中间夹着一个 $d$ 到 $d^2$ 的线性 gap。

这听起来是个奇怪的状态。梯度包含的信息量显然多于函数值，直觉上应该让优化更快。但在复杂性证明的层面，没有人能把这个直觉变成定理。Philip Kerger 在 r/math 帖子里说得很直白：这个 gap 已经存在「since 1996」，他自己「sporadically worked on this problem for about a year」，还和 GPT-5.4、GPT-5.5 做过「long sessions」毫无进展。

GPT-5.6 Sol Pro 一次性把下界推到了 $\Omega!\left(\frac{d^2}{\log(d+1)}\right)$。和 Protasov 的上界 $O(d^2 \log^2 d)$ 之间只差 polylogarithmic 因子——在复杂性论的口径里，这个 gap 等于「关上了」。

GPT 到底证明了什么

要精确描述这个结果，得先看 Lean 仓库里两个独立的端点。

第一个端点是原始的 $\varepsilon \sim d^{-3}$ 精度版本。对于偶数维度 $d = 2m$、$m \geq 1000$、查询预算 $T \leq m^2/1000$ 的情况，证明对每一个确定性 exact-value 策略，都存在一个 admissible 的 max-affine 目标函数，使策略的最优性误差严格大于 $\frac{1}{25,000,000,d^3}$。Lean 里的顶层声明是 ZeroOrderBounds.fixedHorizonLowerBound_strict。

第二个端点是论文里更尖锐的 $d^{-1/2}$ 精度版本。设 $d = 2m$、$\varepsilon_m = \frac{10^{-7}}{\sqrt{2m}}$，对每一个正整数 $m$、每一个满足 $T \leq \frac{m^2}{100\log(em)}$ 的精确 horizon $T$、每一个确定性 exact-value 策略，Lean 构造出一个长度 $T$ 的 transcript 和一个 admissible max-affine 目标，使策略误差严格超过 $\varepsilon_m$。生产声明是 FullDMinusOneHalfAccuracy.fixedHorizonSqrtLowerBound_strict。

完整版本额外验证了一组组合定理：奇数维度通过投影到偶数子块提升硬目标（OddMain.lean），任意半径 $R$ 和 Lipschitz 常数 $L$ 通过缩放运输（ScaledMain.lean，gap 变为 $(LR)\varepsilon_m$），以及 transcript-dependent 的停止策略（StoppingStrategy.lean）。Lean 代码明确否决了每个精确 horizon 直到 floored 核心预算 $\lfloor m^2/(100\log(em))\rfloor$，并证明第一个不在已否决范围内的 horizon 大于 $d^2/(800\log(d+1))$（偶数维）或 $d^2/(1800\log(d+1))$（奇数维）。

预印本还把这个结果 lift 到了混合整数设置：$d$ 个连续变量加 $n$ 个离散变量的混合整数凸优化，如果只有函数值可用，需要 $\tilde{\Omega}(d^2 \cdot 2^n)$ 次查询。离散维度把复杂度推成指数——这是离散优化「原则上比连续优化难」的第一个函数值 oracle 下的形式化佐证之一。

十页提示词：「假设证明存在」

Kerger 在帖子末尾贴出了完整的十页 prompt，结构完全照搬 OpenAI CDC prompt 的方法论。他强调这是「built exactly in the style of OpenAI's CDC prompt」。

OpenAI 在 7 月 10 日公开的 CDC prompt 是一窥前沿模型如何被驱动解数学题的罕见材料。它的核心指令包括：

• 假设肯定证明存在：prompt 要求模型「Assume for purposes of this task that a complete affirmative proof exists」，禁止模型回答「这个问题还没解决」。
• multiagent v2 架构：用 OpenAI 自己的多代理编排，最多 64 个并行子代理同时探索不同方法。子代理之间被禁止知道彼此的方案，避免 groupthink；有一个「approach family registry」记录每一组在试什么；还有专门的对抗验证代理审视每个候选证明。
• 最少 8 小时计算预算：prompt 明确写「Spend at least 8 hours on this before even thinking of returning or giving up」。
• 禁止联网搜索。

这套方法论的核心假设是：对于已经有成熟技术的「中低悬果实」问题，给模型足够的计算预算、结构化的多代理探索、明确的方向引导，它就能找到正确的构造。Kerger 在 r/math 帖子里承认得很坦诚：「I wouldn't really say that this result is using or creating some fundamentally new techniques in convex geometry or optimization theory」。证明的 mechanics——max-affine 函数族、对抗 oracle 策略——一旦找到正确的构造，剩下的都是已有的凸几何结果。

但他点出了更重要的一层：

if a result is attainable with existing techniques, modern AI methods will be able to solve those problems. I don't think researchers in math/TCS will be made obsolete, but I think it will instead no longer make sense to work on any low-hanging, or even medium-hanging fruit.

换句话说，他判断的阈值不在「AI 能不能做数学」，而在「这颗果实是不是真的需要新方法」。需要新方法的硬骨头 AI 还啃不动；但所有「思路对、就是缺一块拼图」的问题，对前沿模型来说已经进入了可解区间。

Kerger 把自己的 prompt 给了 GPT-5.6 Sol Pro 一个相对小的误差要求（order $d^{-4}$），但模型返回的是更强的 $d^{-3}$ 精度版本。后续在另一个共享会话里，模型又把精度推进到了 $d^{-1/2}$。

Lean 验证：从「AI 说对了」到「机器查证」

形式化验证是这条链路上最硬的一环。自然语言证明可以被 AI 编造——这正是社区对 CDC 证明的最大质疑点。数学家 Thomas Bloom 在评价 CDC 时称赞了证明质量，同时批评它「缺乏引用」。GPT-5.6 Sol Ultra 产出的是自然语言证明，依赖人类审阅的可靠性。

Kerger 这次走的是另一条路：他自己先手工检查了 GPT 返回的证明，然后在 Lean 4 / mathlib 里完整形式化。Lean 是一种定理证明助手，它的 type theory 让任何通过检查的证明在逻辑上不可能错——不是「审阅者没发现问题」，是「类型系统能机械地保证每一步都成立」。

仓库里两个端点都「fully verified」：

• 原始 $d^{-3}$ 端点的 Lean 代码用一行 sensitivity 论证就能拿下，需要的凸几何机器比完整版少得多，作为一个更小的独立审计目标被保留。
• 完整 $d^{-1/2}$ 端点形式化了论文里整套「aggregate-width argument」：球面平均、有限 Haar 平均、intrinsic Urysohn 定理，外加一个用一维 Borell–Brascamp–Lieb 运输论证在所有正欧几里得维度上证明的 Brunn–Minkowski 定理。

仓库说明里特别划了一条 scope 边界：「fully verifies」仅指论文的确定性下界结果；上界和 transfer 结果不在形式化范围内。这条边界写得很清楚——不会让人误以为整篇论文都进了 Lean。

整个仓库允许策略对完整 exact-real transcript 有任意依赖，不施加任何连续性、有限精度、线性 span、时间或内存限制。换句话说，证明针对的是一个计算能力无限强的对手——这种情况下 d² 的下界仍然成立，说明难度来自信息论本身——即便算法计算力无限强，d² 次查询依然不够。

一个正在变化的研究分工

Kerger 在结尾给研究者的判断是这场讨论里最值得引用的一段。他没有把 AI 包装成数学家的替代品，而是把它定位成「中低悬果实的收割机」：

研究者仍然需要找那些真正需要新方法的问题。但所有「构造是对的、技术是现成的、就是没人把这两者拼起来」的问题，对会写 prompt 的研究者来说，已经变成了一个 148 分钟的工程任务。

这条链路说明：让前沿模型解硬数学题的关键输入是 prompt，而非算力。算力是现成的（8 小时、64 代理），模型权重是固定的（同一个 GPT-5.6 checkpoint），真正的变量是怎么把「这个问题有解」「该试哪些函数族」「对抗 oracle 应该怎么回答查询」「按什么顺序推进」这些信息结构化地喂给模型。Kerger 的十页 prompt 把这些全部写死了。

Sebastien Bubeck（微软研究院）在 X 上的反应颇具代表性：「This is actually crazy, many of us thought about this lower bound for many years」。一个被一群顶尖优化研究者琢磨多年的下界，被一段精心设计的提示词在两个半小时内击穿——Bubeck 的震惊不在于「AI 能做数学」，而在于「这个具体的问题、这个具体的 gap，原来已经落入了可解区间」。

需要补一层冷静：这是单一数据点。没有 benchmark 套件、没有 scaling 测试、没有跨问题族的可复现性证据。CDC 证明至今没有 Lean 形式化版本，还在社区审阅阶段。GPT-5.6 这条工作流能不能稳定地复制到其他 30 年未决问题，还需要更多案例。

但有一个事实已经成立：一段精心设计的十页提示词 + 一个现有模型 checkpoint + Lean 验证，这个组合产出了一篇 arXiv 预印本（arXiv:2607.13335）、一份可复现的 Lean 代码仓库、和一次对凸优化复杂性论 30 年 gap 的关闭。整条链路里没有新的训练、没有新的架构、没有新的算法——变量只有 prompt。

来源与延伸阅读

• 论文：Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization: A Near-Quadratic Lower Bound from Exact Function Values（arXiv:2607.13335，Phillip Kerger，2026-07-14 提交）
• Lean 代码仓库：github.com/PhillipKerger/zero-order-bounds-lean-verification
• 原始 148 分钟 ChatGPT 会话：chatgpt.com/share/6a55aa50-b484-83ea-85c0-c7e7b4bda41c
• OpenAI CDC prompt PDF：cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf
• r/math 原帖：reddit.com/r/math/comments/1uxj3cy