清华与沃顿研究者借助 GPT 证明梯度下降步长存在理论上限

清华大学工业工程系研究者 Jianhao Ma 与宾大沃顿商学院教授 Yuxin Chen 发布论文，证明标准梯度下降仅靠预先设定步长序列，无法达到 Nesterov 动量方法的 O(1/T²) 收敛速度。论文给出的下界为 Ω(T^-1.9319)，核心证明由 GPT-5.6 Sol Pro 在研究者监督下完成，并通过 Lean 4 形式化验证，代码已在 GitHub 公开。