一、起因
2026-07-18 HN 顶帖「GPT-5.6 used a prompt to close a 30-year gap in convex optimization」(475 分 / 305 条评论)指向 arXiv 2607.13335 —— Phillip Kerger(UC Berkeley IEOR 应用数学 Teaching Prof)在 148 分钟单次会话里用 GPT-5.6 Sol Pro 生成对零阶凸优化 oracle 复杂度下界的证明,把 1996 年 Protasov 给出 d² 上界以来悬而未决的 Ω(d) 与 O(d² log²d) 间隙,首次收紧到 Ω(d² / log(d+1)) 量级,Lean 验证通过。
跟 OpenAI 自家「Cycle Double Cover Conjecture(CDC)证明」相比,这次不是 OpenAI 内部团队亲自跑出来的,而是一位外部数学教授在自己 chat session 里借 GPT-5.6 Sol Pro 的能力补上 30 年没解出来的题。Lean 验证仓库 PhillipKerger/zero-order-bounds-lean-verification 41 stars / Lean 100%(2026-07-14 建仓,4 天后上 HN front page)。
博客园工程读者关心:这条证明从哪条 prompt 路径走出来?Sol Pro 跟 Sol Ultra 工程差别?Lean 验证在「AI 写证明」上边界? 下面是我读 arXiv 2607.13335 + Lean repo + Medium 全文 + HN 305 条评论 length-sorted top-10 之后整理的工程笔记。
二、1996 凸优化 gap 卡在哪
零阶凸优化核心问题:只能拿 f(x) 函数值、看不到梯度,要在 d 维欧氏球凸 Lipschitz 函数上找最小值,至少要多少次函数求值(oracle calls)? 1996 年 Protasov 上界 O(d² log²d) 次求值;30 年来已知下界只有 Ω(d) —— 从一阶 oracle 设定"继承"的,零阶下没人能证出比 d 更强。
Kerger 把 gap 完全关上,给出 Ω(d² / log(d+1)) 零阶下界(polylog 因子)。直接含义:Protasov 的 d² 算法本质上最优。进一步提升到 mixed-integer 设置:d 个连续 + n 个离散变量的混合整数凸优化需要 Ω̃(d² · 2ⁿ) 次函数求值,扩展到工程上常见的组合 + 凸混合场景。来源:arXiv 2607.13335 abstract 第 1-3 段。
三、我做了什么
3.1 抓 arXiv + Lean repo metadata
curl -s --noproxy '*' -A "Mozilla/5.0" --max-time 30 -L "https://arxiv.org/abs/2607.13335" -o /tmp/arxiv_abs.htmlcurl -s --noproxy '*' -A "Mozilla/5.0" --max-time 30 -H "Accept: application/vnd.github+json" "https://api.github.com/repos/PhillipKerger/zero-order-bounds-lean-verification" -o /tmp/repo_meta.json
arXiv <blockquote class="abstract"> 节点直接给 abstract + <meta name="citation_author" content="Kerger, Phillip">,本地正则抽出来够用。Lean repo 41 stars 低于 Pitfall #20 的 100 star 阈值,但只是验证仓库引用,不卡。
3.2 Lean repo 目录树 + CDC 对照
curl -s --noproxy '*' -A "Mozilla/5.0" --max-time 30 -H "Accept: application/vnd.github.raw+json" "https://api.github.com/repos/PhillipKerger/zero-order-bounds-lean-verification/contents/" -o /tmp/lean_tree.json
对照 OpenAI CDC 证明(cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf,3 页 PDF),同样 GPT-5 系列 + Lean 验证:
| 维度 | OpenAI CDC(2026 H1) | Kerger 凸优化(2026-07) |
|---|---|---|
| 题目 | 图论猜想 | 凸优化 oracle 复杂度 |
| 跑者 | OpenAI 内部 | 外部学者独立 |
| Prompt | 未公开 | 10 页 |
| 模型 | 未指明 | GPT-5.6 Sol Pro |
| Lean | 通过 | 通过 |
四、148 分钟 prompt 路径长什么样
Kerger 给出的 prompt 工程细节:
"I wrote a much more elaborate prompt following the same general methodology [as OpenAI's CDC prompt]. My prompt is about ten pages long ... After 148 minutes, GPT-5.6 Sol Pro returned a proposed proof ... I formally verified the proof in Lean, and it passed the formal verification check."
10 页 prompt 是前置研究结论 + 假设清单 + 应当尝试的路线 + 判定模型走偏的纠错条件整套 SOP 串接。工程读者会联想到 agent 的 SOP 模式 —— 跟 Claude Code CLAUDE.md / Hermes ~/.hermes/AGENTS.md 是同类:结构化长 prompt 把任务边界、决策点、回退路径预先编码,让模型 148 分钟内"对照 SOP 自走"而不是"自由生成"。
HN @ck2 把这条工程意义挑准(2026-07-18T17:29):
"could machine-learning even handle a TEN PAGE PROMPT just a year ago? ... After 148 minutes, GPT-5.6 Sol Pro returned a proposed proof ... I formally verified the proof in Lean, and it passed the formal verification check."
一年前模型吃不下 10 页结构化 prompt;GPT-5.6 Sol Pro 在 148 分钟里"读 prompt → 多轮自洽 → 提交 proof → 作者核验"全程无人工介入。这是 context window 扩张 + 多轮内部一致性的工程指标。
@alternator 讲清数学含义(2026-07-18T14:33,1111 字符):
"showing upper bounds on time complexity is 'easy' because it's just the runtime of your algorithm. showing (nontrivial) lower bounds is usually much harder because it requires constraining all algorithms."
lower bound 在算法复杂度里更难 —— upper bound 给算法就行,lower bound 要"约束所有可能算法"。GPT-5.6 Sol Pro 在 lower bound 上给出 30 年来首次实质收紧,是数学贡献级别的判定。
五、Sol Pro 跟 Sol Ultra 的工程差别
HN @d4rkp4ttern 提了关键问题(2026-07-18T15:39,617 字符):
"this was done with Sol Pro not Ultra ... ChatGPT Pro is effectively a multi agent system, or somehow uses multiple LLMs in parallel and selects a best answer. And Ultra is more similar to Claude-Code UltraCode where the main agent can choose to create a dynamic JS workflow that deterministically orchestrates multiple agents."
这是工程读者关心的核心点:Sol Pro 跟 Sol Ultra 不是"模型版本号"差别,是"工作流编排模式"差别。从 Kerger run + OpenAI 公开材料推断:
- Sol Pro:多 LLM 并行 + 选最佳答案(类似 ensemble + verifier),148 分钟单 session 跑完。
- Sol Ultra:主 agent 动态生成 JS workflow,deterministic 编排多个 sub-agent + 对抗性 checker(类似 Claude Code UltraCode 的 DAG-of-agents 模式)。
- 共同点:都跑 148 分钟级长 session,都吃 10 页级结构化 prompt,都依赖 Lean 终验。
下次给团队选模型,按任务形态(SOP 静态 vs DAG 动态)选 Pro/Ultra,而不是按 benchmark 分选。
六、Lean 验证在「AI 写证明」上的真实边界
Kerger 强调 Lean 验证是唯一可信判据:
"AI models are 'fantastic at bullsh*tting, and producing things that pass the eye test for being correct while being utter nonsense.' The Lean formal verification passed, confirming the proof's validity."
工程含义:Lean 不是"看起来对",是 kernel 逐 tactic 检查,跟人眼 review 是两个完全不同的可信度等级;Lean 4 + Mathlib 是当前 AI 证明验证的事实标准,trusted base 边界外(LLM 生成部分)不能自动信,必须进 Lean 重写。Kerger 自陈"Part of me still hopes I have missed something important" —— 作者自己都对 AI 跑出来的东西不放心,Lean 通过才敢下结论。Lean 通过 = 证明对;Lean 不通过 = "模型可能瞎说",不代表模型一定错。
Lean 仓库 41 stars / Lean 100% / description=null / license=null。不是"成型开源项目",是单次证明验证的一次性 repo,fork 二开直接读 .lean 源文件 —— README 没有,topic 空。
七、目前还没完全搞清楚的几个点(局限与待验证项)
- peer review 是否完成(待验证) —— HN @applfanboysbgon 2026-07-18T13:38 直接点名:"Hasn't been peer reviewed yet, so take with a grain of salt. ... Even humans hallucinate proofs too!" arXiv 2607.13335 是 2026-07-14 提交的预印本,到 2026-07-18 上 HN 时尚未同行评议。Lean 通过 ≠ 数学界公认。
- 10 页 prompt 完整结构未完全公开(待验证) —— Kerger 只说"attached at the end of the preprint",2607.13335 的 PDF 抓到 abstract + Lean 链接,完整 prompt 可能在 Lean repo 深层目录,需要继续
curl api.github.com/.../contents/抓更深。 - Sol Pro 跟 Sol Ultra 在单 session 长度上的真实吞吐(待验证) —— 148 分钟跑完不代表两种变体都能跑 148 分钟;公开材料只有 Sol Pro 这条 run,没横向对照。
- Lean repo 41 stars 意味着社区验证还早(不足) —— Pitfall #20 实证 100 star 阈值才适合当主选题。41 star + 1 fork + description=null + license=null,没有任何第三方数学家完整复现 Lean proof;Lean 通过是 Kerger 自己跑的,不是社区跑的。
- Kerger 自陈"我给方向不多,大部分 prompt 是 GPT-5.6 自己写的"(不足) —— HN @sashank_1509 2026-07-18T15:43(1548c)引用:"the author used GPT5.6 to write most of the prompt. He just gave some mild direction." 这条直接挑战"作者主导"叙事 —— 真实情况可能是 GPT-5.6 自己写 10 页 prompt 草稿,作者给方向。整个"AI 协助"程度可能比 Medium 全文暗示的更高。
- 跟其它「AI 写证明」事件横向对照缺失(坑点) —— OpenAI CDC(2026 H1) + Kerger 凸优化(2026-07) + Google DeepMind FunSearch / AlphaProof / AlphaGeometry 都属于「AI 生成数学证明」,目前没有统一 benchmark 表横向对比 prompt 长度 / 验证工具 / session 时长 / 难度等级。博客园读者想拿这条当"AI 4 阶段"叙事还差最后一公里数据汇总。
- Mixed-integer 部分 proof 是否在 Lean 里完整覆盖(还在调研) —— Abstract 里 Ω̃(d² · 2ⁿ) 是论文亮点,但 Lean repo 是否包含这部分的 formalization 没看到完整文件列表;也许只 formalize 了连续部分的 d² 下界,mixed-integer 那段还停在 paper proof。
八、适用场景与不适用场景
| 场景 | 是否适用 | 备注 |
|---|---|---|
| 团队试 GPT-5.6 Sol 系列跑数学证明 | ✅ | Lean 验证是基线门槛,不能省 |
| 复现 10 页结构化 prompt 模式 | ✅ | 不限数学,工程 SOP 也套 |
| 用 Sol Pro / Sol Ultra 编排 agent | ✅ | 按"任务 SOP 静态 vs DAG 动态"选 Pro/Ultra |
| 拿这条当"AI 取代数学家"宣传 | ❌ | peer review 没过,Lean 通过 ≠ 公认 |
| 把 Lean repo fork 当长期维护项目 | ❌ | 41 star / 一次性证明验证 repo,desc/license 都空 |
| 拿 Kerger 自陈当客观技术评价 | ❌ | 他自陈"我给的方向不多",Medium 叙事偏乐观 |
九、参考链接
- arXiv 2607.13335(Phillip Kerger, 2026-07-14):https://arxiv.org/abs/2607.13335
- Lean verification repo:https://github.com/PhillipKerger/zero-order-bounds-lean-verification
- Kerger Medium 全文:https://medium.com/@kerger.p/an-ai-assisted-breakthrough-in-convex-optimization-an-optimization-problem-dating-back-30-years-a-db5c631119de
- HN 原帖(HN 48957779):https://news.ycombinator.com/item?id=48957779
- OpenAI CDC 证明(对照):https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf
 agent和组件)