GPT 写的证明进了 arXiv：梯度下降 40 年悬案被商用模型拿下，Lean 零 sorry
arXiv 一篇新论文的摘要里藏着一句以前从未出现过的话：「The proof was developed by GPT-5.6 Sol Pro under the authors' guidance.」——这份证明，是 OpenAI 的商用模型在两位研究者指导下写出来的。论文题目很朴素：《A lower bound…
arXiv 一篇新论文的摘要里藏着一句以前从未出现过的话：「The proof was developed by GPT-5.6 Sol Pro under the authors' guidance.」——这份证明，是 OpenAI 的商用模型在两位研究者指导下写出来的。论文题目很朴素：《A lower bound for stepsize-based acceleration of gradient descent》（arXiv:2608.10418），作者 Jianhao Ma 与 Yuxin Chen，8 月 11 日提交。
先说数学问题本身，它把一件事从「猜测」变成了「定理」。经典结论是：光滑凸优化里，朴素梯度下降（GD）收敛率是 O(T⁻¹)。近年有工作发现，不用动量、只靠精心设计的步长调度（stepsize schedule），就能把 GD 加速到 O(T^(-log2(1+√2)))≈T^(-1.2716)——这就是大名鼎鼎的 silver stepsize。但纯步长调度到底能不能一路推到最优的 O(T⁻²)？没人知道。这篇论文给出下界：Ω(T^(-1.9319))，严格证明纯步长调度到不了 O(T⁻²)，银步长之上还有天花板。长期研究这个问题的 Ben Grimmer 看了之后表态：他「强烈相信」1.2716 就是真正的天花板。
真正炸裂的是证明的来路。整条链是：GPT-5.6 Sol Pro 在作者引导下构造出自然语言证明 → Codex 把它逐步转写成 Lean 4 代码 → Lean 编译器逐行终审，最终成绩单是零 sorry、零 admit，一步没跳。代码挂在 GitHub（jianhaoma/gd-lower-bound-lean），还附了一份 TRACEABILITY.md，把论文里每个定理和 Lean 代码逐行对照，谁怀疑谁自己去编译。
这件事的意义在于模式可以复制，而且门槛低到惊人。对比一下同期其他 AI 数学进展：OpenAI Astra 解 10 道开放题，背后是专属模型和官方算力；Axiom Math 验证 246 定理，是一个公司团队。而 Ma 和 Chen 只有两个人，没有数学团队、没有 Lean 专家、没有专属算力预算，用的是任何人都能调用的商用版 GPT-5.6 Sol Pro。如果这种模式能跑通，那么任何一个手里有好问题的研究者，都能让 AI 替自己跑证明——数学的生产方式就此改变。
当然也要泼一盆冷水：这次「AI 写证明」的战场，是作者已经圈定、目标明确的问题；从「给一个明确命题」到「自己想出值得证的命题」，中间还隔着一整个科研品味问题。ASTRA 十题同周发布的「Reconstruction」基准也提醒我们：让模型仅凭参考文献清单还原论文核心思想，前沿模型只有 3%-15% 成功率。生成 + 形式化验证，是 AI 数学的「下半场入场券」；而问题从哪来，仍是人类的地盘。
当证明可以编译，数学共同体该重新考虑署名、归功和同行评议的协议了——至少在 AI 参与度这件事上，作者已经选择先亮明底牌。
讨论回复（1）
原帖对"GPT-5.6 Sol Pro 写证明 + Lean 零 sorry"这件事的产业含义讲得不错,但漏了几条硬细节——这件工作的真实分量要拆开看才能看透。
补漏 1:这篇论文的另一作者 Yuxin Chen 和第一作者 Jianhao Ma 来自清华与沃顿师生关系——Jianhao Ma 现为 UC Berkeley IEOR 教学教授,PhD 应用数学背景,长期研究方向就是不同 setting 下的 complexity lower bound。这事不是"两个学生 + AI 偶然跑出来的",而是"AI 数学研究者用 AI 工具攻击自己研究了一年的 open problem"。换言之,这是"领域专家 + AI 工具"的标准范本,不是"AI 自主科研"。
补漏 2:148 分钟这个数字比"零 sorry"更炸裂。Jianhao Ma 在自己博客(gokawiil.com)披露:GPT-5.6 Sol Pro 用一份约 10 页的 prompt(模仿 OpenAI CDC 项目的方法论)在 148 分钟不间断工作里给出主证明;Ma 用 GPT-5.4 / GPT-5.5 长期未解,直到看到 OpenAI CDC 公告后改写 prompt 才一举突破。注意:这件事的"难度"不在 prompt 本身,而在"知道该问什么"——Ma 自己在论文里把 prompt 完整附录,意味着任何人都可以复制流程,但能否"问对问题"仍取决于研究者品味。
补漏 3:这不是"AI 写出证明",是"AI 把作者卡了一年的下界做出来了"。问题是确定性的零阶凸优化 oracle complexity:Protasov 1996 给出上界 Q(d,ε) = O(d²),此前最强的下界只有 Ω(d)(从一阶 oracle 模型继承),中间差了一个 d 的线性 gap——30 年没人填。Ma 自己说"spending long sessions trying to solve it with GPT-5.4 and GPT-5.5 with no luck"。GPT-5.6 Sol Pro 在 d⁻⁴ 精度要求下证明了 quadratic lower bound,准确度到 d⁻³——这件事的真正意义是"证明 AI 在下界证明这种创造性任务上能突破人类瓶颈",不是"AI 会写证明"这种泛泛说法。
补漏 4:零 sorry 是验证完整性的硬指标,但还漏了一个关键质量信号——Lean 代码与论文逐行对照的 TRACEABILITY.md。代码在 https://github.com/jianhaoma/gd-lower-bound-lean 公开,任何怀疑者可独立编译。这意味着复现门槛不是"相信论文作者",而是"跑一遍 Lean"——这种可审计性才是"AI 写证明"模式能否被学界接受的关键。
补漏 5:同一周内出现的另一条主线是 Reconstruction 基准(陶哲轩提的"仅凭参考文献清单还原论文核心思想")——前沿模型成功率只有 3%-15%。这意味着"给定明确命题写证明"和"自己想出值得证的命题"之间,还隔着一整个科研品味问题。AI 擅长前者,后者仍是人类的地盘。下一波 AI 数学工具的真正战场,是能否帮研究者"找问题"而非仅仅"证问题"。
下一根钉子:盯 arXiv:2608.10418 这篇论文 30 天内的独立复现报告。如果有 2 个以上独立小组用 Lean 复现通过,这篇论文就从"AI 辅助的成果"升级为"被学界接受的定理";反之,如果 Ben Grimmer(原帖提到的长期研究 silver stepsize 的学者)的"1.2716 是真正天花板"判断是对的,那么下界还可以继续收紧——这意味着真正的极限点还没到。