2026年7月15日，Reddit 数学板块出现了一条帖子，标题平淡无奇——大意是”看了 OpenAI 那个 CDC 猜想的证明方法后，我用 GPT-5.6 试了试，关掉了一个 30 年的缺口”。
三天后，这条帖子在 Hacker News 上拿到了 477 个赞、308 条评论。那些逐行读过 Lean 代码的数学家们，态度出奇一致：这次是一个真正的数学贡献。
笔者读完一圈讨论，发现这件事的冲击力在于：它碰了一个人类数学家都觉得格外棘手的任务——证明下界。而 GPT-5.6 用一条 prompt、148 分钟，把这件事做完了。
发生了什么：一条 prompt、148 分钟、一个 30 年的缺口
Phillip Kerger 是 UC Berkeley 的应用数学助理教授，在 Johns Hopkins 拿的优化理论博士，之前在 NASA 量子人工智能实验室做过研究。从去年开始，他断断续续在啃一个问题——凸优化领域中一个从 1996 年就悬而未决的复杂度缺口。
简单说：1996 年有人设计了一个算法，跑出来的复杂度是 \(O(d^2 \log^2 d)\)。大家都知道不可能比 \(O(d)\) 更好（因为至少得看一眼每个维度）。但 \(O(d)\) 到 \(O(d^2 \log^2 d)\) 之间的 30 年空白，没人能填上——到底是还能更快，还是那个老算法已经到头了？
Kerger 之前试过 GPT-5.4 和 GPT-5.5，都失败了。即便他手动把思路指向正确的函数族，模型也补不全最后几步。
然后 GPT-5.6 来了。
他参照 OpenAI 几周前发布的”循环双覆盖猜想”证明 prompt 的结构，写了一份大约 10 页的 prompt——里面指定了数学设定、列举了可行的证明路线、塞进了自己之前失败尝试的经验，还明确定义了什么结果不算有效解。他先用 GPT-5.6 帮忙整理了相关文献、完善了 prompt 中的论证框架，然后在一个连续的会话中把最终版本喂给模型。
148 分钟后，GPT-5.6 吐出了完整的证明构造。
图片来源：Unsplash / GuerrillaBuzz — 凸优化方法的收敛性图示。GPT-5.6 所证明的，正是下界曲线无法再被压低——1996 年的那个老算法已经踩在了理论极限上。
结果是：\(\Omega(d^2 / \log(d+1))\) 的下界，与已知上界 \(O(d^2 \log^2 d)\) 之间只差对数因子。这就排除了”存在比那个 30 年老算法快得多的方法”的可能性。
为什么”证明下界”难得多？用跑步打个比方
要理解这件事的分量，笔者先讲一个生活里的类比。
证明上界就像证明你能跑 100 米——你只需要跑一次，计时器一按，结论就成立了。
证明下界就像证明你不可能跑得更快——为此你必须排除所有可能的训练方法。换跑鞋？没用。改起跑姿势？没用。吃特殊食谱？还是没用。为了让”你不可能跑进 9 秒”这个结论成立，你需要穷尽一切可以想象的方式，逐一证明它们都帮不了你。
在数学里，证明上界（“我找到了一个方法，它至少能做到这个程度”）相对容易——你给出一个算法，算一下它的复杂度，完事。但证明下界（“不存在任何方法可以比这更快”）需要约束所有可能的算法。你得证明：不管别人怎么设计新算法，不管用什么技巧，不管绕多少弯路——统统没用，极限就在这里。
这就是为什么 HN 上那位叫 alternator 的评论者——一个自称”对这个领域略知一二”的人——会说：
“证明上界很容易，就是你的算法跑了多长时间。证明非平凡的下界要难得多，因为它要求你约束所有可能的算法。”
而 GPT-5.6 这次做到的事，恰好是后者。它不光证明了 Kerger 构造的那个算法效果好——它证明的是，那个 1996 年的老方法，已经碰到了理论天花板。30 年来没人能排除”也许还有更好的办法”这个可能性，GPT-5.6 148 分钟把它排除了。
两种 AI 做数学：别再混为一谈
讨论 AI 做数学的时候，有必要区分两件事。它们看起来差不多，实质上完全不同。
第一种：AI 辅助猜测。 这是已经发生好几年的事。研究者让模型在已知结果之间寻找模式，生成一些”看起来有希望”的猜想，然后人类去验证。模型说”我觉得这个不等式可能成立”，人类拿纸笔或者计算机去检查。这种场景里，AI 是个很聪明的助手，但最后的判断权在人手里。
第二种：AI 独立完成严格证明——并通过形式化验证。 这是 GPT-5.6 这次做的事。模型不光输出了一段”看似合理”的论证，而且这个论证被完整地翻译进了 Lean 4——一个数学证明助理系统——逐行编译通过。Lean 不接受”显然可得”、“容易看出”这类修辞。在 Lean 的世界里，要么每一步的逻辑都无懈可击，要么直接报错，没有中间地带。
Kerger 把整份证明的 Lean 代码放到了 GitHub 上。任何人只要装一个叫 elan 的版本管理器，把仓库克隆下来，跑一行 lake build，就能亲眼看到编译器从头到尾没有报错。再跑 #print axioms，确认没有 sorryAx（Lean 里表示”这一步我还没证”的占位符）——这意味着，整条逻辑链条上没有任何缺口。
Kerger 的 36 页预印本、完整的 prompt、模型对话记录、Lean 代码、构建说明——全部公开。这个披露标准，比那些只在致谢里提一句”感谢 AI 系统协助”的论文高了不止一个档次。
图片来源：Unsplash / Bozhin Karaivanov — Lean 证明助理的代码界面。GPT-5.6 的证明被完整翻译进 Lean 4 并编译通过，整条逻辑链条上没有任何 sorry（未证步骤）。
公平地说：质疑的声音同样值得听
笔者不打算把这篇文章写成一篇”AI 碾压人类”的爽文。r/math 和 HN 上都有不少理性的质疑，这些声音对理解这件事的全貌很重要。
第一，领域确实比较 niche。 多位评论者指出，这个凸优化的下界问题，知名度远不如 OpenAI 之前搞定的”循环双覆盖猜想”。后者是图论里挂了 50 年的名问题，而这个下界猜想主要活跃在一个相对小的优化理论圈子里。它的学术价值是真实的，但”破圈”的程度有限。
第二，迁移性存疑。 证明下界需要的推理模式——约束所有可能的算法——确实是一个难度很高的类别，GPT-5.6 在这上面展现了能力。但这个能力能从凸优化迁移到其他数学分支吗？目前没人知道。
第三，优先权争议。 r/math 的讨论中，有人在翻 1990 年代的俄文优化文献，怀疑 Kerger 证明中的核心引理可能已经被苏联数学家发表过，只是发表在不常被西方数据库收录的期刊上。如果这一点被确认，GPT-5.6 的贡献就是”从几乎被遗忘的文献中重建了一个论证，并用一种从未有人用过的方式把它形式化”。这两种贡献的分量是不同的。
第四，“148 分钟”不是全部。 Kerger 在这道题上已经断断续续花了一年。那 10 页 prompt 里塞进了他对问题的理解、失败的尝试、排除了的死胡同。GPT-5.6 之前，GPT-5.4 和 GPT-5.5 都在同一道题上失败了。148 分钟是最后一次无间断的证明搜索——而不是从零开始的魔术。正如 RuntimeWire 的报道所说：“prompt 里包裹着一年的领域工作。”
图片来源：RuntimeWire / Gemini — AI 生成的数学证明流程插图。值得记住的是：prompt 背后是一年的领域积累，148 分钟只是最后一步的搜索时间。
真正重要的是这个工作模式
把争议放一边，笔者觉得这件事里最值得关注的东西，反而不是那个具体的定理。
是人 + AI + 形式化验证这个三角工作流，被证明是可复制的。
Kerger 的做法很清楚：把大问题拆成小引理，先把每个引理翻译成 Lean 的严格语句，再让模型去填证明。哪个引理编译不过，就单独迭代哪个——不会因为一个地方的改动把整个证明推翻重来。这个流程不需要你是菲尔兹奖得主，门槛在于：你得能把你的问题精确地定义出来。
换句话说，AI 在吃掉”中等难度”的数学问题这条路上，已经有了可操作的配方。 这不会让数学家失业——定义问题、构造 prompt、判断输出是不是废话，这些事目前还是得人来。但它会改变数学研究的日常：研究者越来越像导演，AI 越来越像执行团队。
一位 HN 评论者说得直白：有时候看这种讨论就像看天书。但别被术语吓住——这件事的本质很简单。30 年来，人类知道一个算法能跑多快，但不敢说”这就是极限”。一个 AI，在一个人花了一年积累的引导下，用 148 分钟把”这就是极限”给证明了。 然后，另一台叫 Lean 的机器逐行检查了它的作业，确认没抄近路。
这才是 2026 年的数学前沿——人、AI 和证明编译器，开始在一个项目组里共事了。
参考链接：
- Reddit r/math: After OpenAI’s CDC proof announcement, GPT-5.6 used a prompt to close a 30-year gap in convex optimization
- HN 讨论 (item?id=48957779)
