GPT-5.6 Sol Pro Co-Authors an arXiv Proof: A 40-Year Gradient Descent Lower Bound, Verified in Lean with Zero sorry

Forum topic · QianXun · 2026-08-23

Summary

An arXiv paper (2608.10418) titled 'A lower bound for stepsize-based acceleration of gradient descent,' submitted August 11 by Jianhao Ma and Yuxin Chen, establishes the lower bound Ω(T^(-1.9319)), proving that stepsize-only scheduling in smooth convex gradient descent cannot reach the optimal O(T⁻²) rate, leaving the famous silver stepsize rate O(T^(-log2(1+√2)))≈T^(-1.2716) as a likely ceiling. Unusually, the paper's abstract states the proof was written by OpenAI's GPT-5.6 Sol Pro under the authors' guidance: the model produced a natural-language proof, OpenAI Codex translated it into Lean 4, and the Lean compiler accepted it with zero `sorry` and zero `admit`. Companion artifacts (a GitHub repository jianhaoma/gd-lower-bound-lean and a TRACEABILITY.md mapping every theorem to Lean lines) let anyone reproduce the verification. The authors note the workflow uses only a commercial API, no math team, and no Lean experts, suggesting a replicable pattern, while cautioning that identifying which problems are worth proving remains a human responsibility. The explicit AI disclosure also reopens questions about authorship and peer review in mathematics.

Background: a 40-year-old gradient descent question

In smooth convex optimization, the textbook rate of plain gradient descent (GD) is O(T⁻¹). Recent work showed that a carefully designed stepsize schedule alone, without momentum, can already accelerate GD to

O(T^(-log2(1+√2))) ≈ T^(-1.2716),

the well-known *silver stepsize* result. Whether pure stepsize schedules can ever be pushed all the way to the optimal O(T⁻²) had remained open for decades.

What the new paper proves

The paper *A lower bound for stepsize-based acceleration of gradient descent* (arXiv:2608.10418), authored by Jianhao Ma and Yuxin Chen and submitted August 11, closes the question from below. Its main result is the lower bound

\Omega(T^{-1.9319})

which strictly rules out reaching O(T⁻²) via stepsize-only schedules and places a hard ceiling above the silver rate. Long-time specialist Ben Grimmer reacted by saying he "strongly believes" that 1.2716 is in fact the true ceiling.

How the proof was produced

The unusual line in the abstract — *"The proof was developed by GPT-5.6 Sol Pro under the authors' guidance"* — describes the full pipeline:

1. GPT-5.6 Sol Pro (an OpenAI commercial model) drafts a natural-language proof under the authors' direction. 2. OpenAI Codex translates the draft into Lean 4 step by step. 3. The Lean 4 compiler audits the output line by line.

The final tally: 0 sorry, 0 admit — no gaps were left in the formalization.

Reproducibility artifacts

GitHub: jianhaoma/gd-lower-bound-lean — the Lean 4 source.
TRACEABILITY.md — a theorem-by-theorem, line-by-line map from the paper to the Lean code, so any skeptic can recompile and verify.

Why this matters

The pipeline is striking because of its low barrier to entry:

| Effort | Other recent AI-math projects | Ma & Chen | | --- | --- | --- | | Models | Bespoke/flagship models with official compute | Commercial GPT-5.6 Sol Pro via API | | Team | Company teams (e.g., Axiom Math verifying 246 theorems) | Two researchers | | Lean expertise | Dedicated Lean engineers | None on the team | | Compute budget | Dedicated | Standard API access |

Compared with OpenAI Astra solving 10 open problems with custom models and Axiom Math verifying 246 theorems with a company team, Ma and Chen did it with two people, a commercial model, and a public verifier. If this template generalizes, any researcher with a well-posed problem can offload the mechanical part of proving it.

The honest caveats

The AI is operating inside a problem the authors already framed. Moving from "prove this stated proposition" to "decide which propositions are worth stating" is a different, still-human skill.
The same week's Reconstruction benchmark from Astra reports that frontier models recover the core ideas of a paper from its reference list only 3%–15% of the time.

So generation + formal verification may be the ticket to the second half of AI-driven mathematics, but problem selection remains human territory.

Open question for the community

When proofs can be compiled, mathematics has to rethink authorship, attribution, and peer-review conventions for AI involvement. The authors here have chosen to disclose that involvement up front.