GPT 写的证明进了 arXiv：梯度下降 40 年悬案被商用模型拿下，Lean 零 sorry

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 参与度这件事上，作者已经选择先亮明底牌。