A new paper from Jianhao Ma of Tsinghua University and Yuxin Chen of the University of Pennsylvania’s Wharton School argues that standard gradient descent hits a hard mathematical ceiling if researchers only tune its step-size sequence and do not change the algorithm’s structure.
The headline result is a lower bound of Ω(T^-1.9319) for gradient descent with any pre-specified nonnegative step-size sequence. In the framing given by the report, that closes off a long-running hope in optimization theory: that carefully crafted step sizes alone might let plain gradient descent catch the O(1/T²) convergence rate of Nesterov acceleration.
A 40-year question in optimization
The report describes gradient descent as the basic optimization engine behind a wide range of AI systems, including GPT, Stable Diffusion, and autonomous driving workloads. In its standard form, gradient descent converges at O(1/T), meaning the error falls to roughly the scale of 1/T after T iterations.
That changed in 1983, when Nesterov introduced momentum and pushed the rate to O(1/T²). The article illustrates the difference with a simple comparison: after 1,000 steps, the error scale moves from about one-thousandth to about one-millionth, a three-order-of-magnitude improvement. According to the report, that accelerated rate remains theoretically optimal.
This set up a natural problem that stayed open for decades: if one does not add momentum and does not alter the algorithm itself, can a sufficiently clever step-size schedule alone reach the same speed?
The question tightened in 2023 when MIT researchers Altschuler and Parrilo introduced the “silver stepsize.” Instead of a conventional monotone decay, that sequence varies in a fractal, self-similar pattern. The reported gain was O(T^-1.2716), which left the field with a sharper question: is 1.2716 merely an early milestone, or is it the real endpoint for step-size scheduling alone?
The researchers and the AI system
The paper was taken up by Ma and Chen. The report says Ma joined Tsinghua University’s Department of Industrial Engineering in July this year after earning his PhD at the University of Michigan and completing postdoctoral work at Penn. Chen is identified as an endowed professor at Wharton, with a Stanford doctorate, a prior move from Princeton to Penn, and a SIAM best paper award.
Earlier work had largely followed an additive path: design smarter and smarter step-size sequences and test how much speed they could extract. Ma and Chen went in the opposite direction. Their aim was to prove the existence of a line that no step-size schedule could cross.
According to the report, they then handed the problem to GPT-5.6 Sol Pro. The model was given two things: the research target — prove that step-size scheduling alone cannot achieve O(1/T²) — and a high-level plan called a “resisting oracle.”
The idea behind that strategy is to build an adversarial trajectory along which gradient descent moves as slowly as possible, then identify a real smooth convex function whose gradient descent path matches that slow trajectory exactly.
How the proof is built
The core construction produced by GPT-5.6 Sol Pro was geometric. For any given step-size sequence, the proof first isolates the “long steps,” defined in the report as those larger than the standard safe value 1/L. It then places a family of mutually orthogonal anchor points in a high-dimensional space, one for each long step.
That setup forces gradient descent to keep moving in the same direction between two long steps, then jump to a completely orthogonal direction when a long step arrives. The report says the entire path can be realized exactly by a smooth convex function built through the Moreau envelope, making the geometric construction and the actual optimization instance strictly equivalent.
The force of the argument lies in its customization. It is tailored to the specific step-size sequence under examination. In other words, no matter how the steps are arranged, the construction can produce a matching function that traps the method.
But the proof still had another hurdle. The final lower bound could not depend on the order in which the long steps appear. If it did, then simply permuting the same multiset of step sizes might evade the conclusion.
To remove that dependency, the report says GPT-5.6 Sol Pro introduced a matching technique: sort the long steps by size, build a path, split the construction into odd and even pairings, and eliminate the timing dependence that way. A Lyapunov potential then controls global growth, while a truncation argument aggregates local constraints into a full lower bound.
The article says this argument did not appear in one pass. Ma and Chen repeatedly interacted with GPT-5.6 Sol Pro, pointed out flaws when they found them, and let the model continue after revisions. Ma’s description, as quoted in the report, was that there was “no nontrivial mathematical component” in the core proof that came from humans.
Why the exponent stops at 1.9319
The proof contains a key parameter constrained by two conditions at once. In the report’s summary, one comes from the matching bound and supplies a lower limit, while the other comes from growth control and supplies an upper limit. As the convergence exponent p moves downward, the feasible region narrows.
At p = √(2+√3) ≈ 1.9319, the two constraints meet and the remaining room disappears. Past that point, the proof can no longer be pushed. The resulting theorem is that for any pre-determined nonnegative step-size sequence, gradient descent has convergence-rate lower bound Ω(T^-1.9319).
Put plainly in the language of the report, plain gradient descent cannot outrun that line through step-size design alone. If one wants the fastest rate, the algorithm itself has to change.
Formal verification in Lean 4
A proof written with AI raises the obvious question of reliability. Ma and Chen addressed that by using the Lean 4 theorem prover. The report says Codex was used to translate GPT-5.6 Sol Pro’s natural-language proof into Lean 4 code step by step, after which the system checked every line.
If a step cannot yet be completed in Lean 4, users can insert “sorry” or “admit” as placeholders and return later. The reported outcome here was “zero sorry, zero admit,” meaning no step was skipped.
The code is public on GitHub and includes a TRACEABILITY.md file that maps each theorem in the paper to the corresponding Lean proof. The repository listed in the report is: https://github.com/jianhaoma/gd-lower-bound-lean.
The verification chain is described as a three-part relay: GPT-5.6 Sol Pro constructed the proof, Codex translated it into Lean 4, and the compiler served as the final line-by-line checker, with humans supervising throughout.
The gap that remains
What is settled so far is a range. The silver stepsize pushes gradient descent to T^-1.2716. Ma and Chen’s lower bound says it cannot beat T^-1.9319. That leaves a gap of about 0.66, and the actual limit for step-size scheduling alone remains open.
The report cites optimization researcher Ben Grimmer, who said after reading the paper that he “strongly believes” 1.2716 is the true ceiling. If that view is right, then silver stepsize may already sit at the endpoint, while Ma and Chen’s lower bound still has room to tighten.
Even without resolving that final gap, the paper changes the status of the problem. A claim that had remained conjectural is now a theorem: tuning the step sizes alone is not enough to make standard gradient descent fully accelerated.
Paper and source details
The report presents the work as a result produced by two researchers without a larger mathematics team, without Lean specialists, and without a dedicated compute budget, using a commercial version of GPT-5.6 Sol Pro that others can also access.
The paper referenced in the article is available at https://arxiv.org/abs/2608.10418.
The MarsBit post credits the original piece to the WeChat public account “新智元,” with “ASI启示录” as author and “摩西” as editor. MarsBit lists the publication time as Aug. 24, 2026.