A new arXiv paper contains a sentence never seen before in an abstract: "The proof was developed by GPT-5.6 Sol Pro under the authors' guidance." The paper, *A lower bound for stepsize-based acceleration of gradient descent* (arXiv:2608.10418) by Jianhao Ma and Yuxin Chen, was submitted on August 11.
The Mathematical Result
The paper turns a long-standing question into a theorem. In smooth convex optimization, plain gradient descent (GD) converges at a rate of O(T⁻¹). Recent work showed that with no momentum, but with carefully designed stepsize schedules, GD can be accelerated to O(T^(-log2(1+√2))) ≈ T^(-1.2716) — the well-known silver stepsize. But whether pure stepsize schedules could reach the optimal O(T⁻²) was unknown.
This paper proves a lower bound of Ω(T^(-1.9319)), rigorously showing that pure stepsize schedules cannot achieve O(T⁻²). There is a ceiling above the silver stepsize. Ben Grimmer, who has studied this problem for years, stated after reading the paper that he "strongly believes" 1.2716 is the true ceiling.
How the Proof Was Made
The proof pipeline is the striking part:
1. GPT-5.6 Sol Pro constructed a natural-language proof under the authors' guidance
2. Codex translated it step by step into Lean 4 code
3. The Lean compiler verified every line — the final scorecard: zero sorry, zero admit, no skipped steps
The code is on GitHub (jianhaoma/gd-lower-bound-lean) with a TRACEABILITY.md mapping every theorem in the paper to the Lean code line by line. Skeptics can compile it themselves.
Why It Matters
The significance is that the pattern is replicable at a remarkably low barrier. Compare with other recent AI math achievements:
- OpenAI Astra solved 10 open problems, backed by a proprietary model and official compute
- Axiom Math verified 246 theorems, as a company team
- Ma and Chen were two people — no math team, no Lean experts, no dedicated compute budget, using a commercial GPT-5.6 Sol Pro anyone can call
The Caveats
A cold shower is warranted: the "AI writes proofs" battlefield here was a problem already scoped by the authors with a clear target. From "prove a given proposition" to "invent a proposition worth proving" lies the entire question of research taste. The "Reconstruction" benchmark released alongside ASTRA's ten-problem result reminds us of this: when asked to recover a paper's core ideas from just its reference list, frontier models succeed only 3%–15% of the time.
Generation plus formal verification is the entry ticket to AI mathematics' second half. But where the questions come from remains human territory.
When proofs can compile, the mathematical community needs to rethink its protocols for authorship, credit, and peer review — at least regarding AI involvement, the authors have chosen to show their hand upfront.