Escaping Nesterov flows and iterates below critical damping

Q: Is the proof formally verified?

The continuous-time and discrete Hilbert-space thresholds and the planar escape for 1 2 and existence of solutions for r ≤ 1 are conventional proofs, and the paper is an unrefereed preprint.

Dev D. Goyal

Escaping Nesterov flows and iterates below critical damping

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Selected result in this collection

Problem and result

Problem: Boundedness of Nesterov ODE trajectories and iterates below critical damping r < 3
Posed in: Recorded as open by Jang and Ryu, 'Point convergence of Nesterov's accelerated gradient method: an AI-assisted proof', arXiv:2510.23513 (version 2, 2026); the equation is due to Su, Boyd and Candès
Status: Partially resolved
Result: On ℓ²(ℕ;ℝ²), Nesterov flows from rest and iterates with momentum k/(k+r) stay bounded for all convex objectives with 1-Lipschitz gradient and attained minimum exactly when r ≥ 3; a planar potential escapes for 0 < r ≤ 2.

Abstract

For zero-velocity solutions of X″ + (r/t)X′ + ∇F(X) = 0 and for the Nesterov iteration with momentum k/(k+r), with F convex, its gradient 1-Lipschitz and its minimum attained, boundedness holds for r ≥ 3. On the Hilbert space ℓ²(ℕ;ℝ²) this threshold is sharp for both: for every 0 < r < 3 an explicit block sum of smoothed valleys has a trajectory, and another has iterates, with norms tending to infinity. In the plane, the potential h(√(x²+y²)) − x with the Huber function h has an escaping trajectory from (2,1) for every 0 < r ≤ 2 and bounded trajectories for r > 2. The finite-dimensional range 2 < r < 3 is open.

Details

Year: 2026
Discipline: Mathematics
Area: Convex optimization
Subject: Optimization
Result type: Sharp thresholds, explicit counterexamples and reproducible proof package
Formal proof: Standalone Lean package
Family: nesterov-subcritical
Keywords: Nesterov accelerated gradient, Nesterov ODE, vanishing damping, subcritical damping, unbounded trajectories, FISTA momentum, Su–Boyd–Candès

Statement and scope

Formal scope. The continuous-time Hilbert-space threshold, the discrete threshold and the planar escape for 1 < r ≤ 2, including actual gradients, global solutions from rest and norm divergence, are formalized. The planar escape of the same potential for 0 < r ≤ 1, its boundedness for r > 2 and existence of solutions for r ≤ 1 are conventional.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 385 KB
PDF on GitHub: papers/mathematics/nesterov-subcritical/manuscript.pdf
LaTeX source: papers/mathematics/nesterov-subcritical/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/nesterov-subcritical/

Lean project

papers/mathematics/nesterov-subcritical/lean/ 57 Lean files

Lakefile

papers/mathematics/nesterov-subcritical/lean/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/nesterov-subcritical/VERIFICATION.md, which gives their context and working directory.

lake exe cache get
python3 verify_release.py --lean-home "$(lean --print-prefix)" \
  --mathlib .lake/packages/mathlib --out ../verification-replay

README: papers/mathematics/nesterov-subcritical/README.md
Verification guide: papers/mathematics/nesterov-subcritical/verification/README.md
Verification record: papers/mathematics/nesterov-subcritical/VERIFICATION.md
Authorship: papers/mathematics/nesterov-subcritical/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Source. Su, Boyd and Candès introduced the equation; boundedness for r ≥ 3 is classical, and Jang and Ryu record the subcritical case as open. Related work and limits are stated in the manuscript. Historical priority is not certified.

Questions and answers

Are Nesterov ODE trajectories bounded when the damping parameter r is below 3?

Not in general: on the Hilbert space ℓ²(ℕ;ℝ²), for every 0 < r < 3 there are convex objectives with 1-Lipschitz gradient and attained minimum whose flow from rest, and others whose Nesterov iterates with momentum k/(k+r), have norm tending to infinity. In the plane, h(√(x²+y²)) − x with the Huber function h has an escaping trajectory from (2,1) for every 0 < r ≤ 2, and bounded trajectories for r > 2.

Is the finite-dimensional case settled?

No. Whether a finite-dimensional objective has an unbounded zero-velocity trajectory for some 2 < r < 3 is open, as is a finite-dimensional unbounded discrete orbit for 1 < r < 3. In every example the minimizer set is unbounded, which is necessary in finite dimension.

Is the proof formally verified?

The continuous-time and discrete Hilbert-space thresholds and the planar escape for 1 < r ≤ 2 are formalized in Lean 4. The planar escape for 0 < r ≤ 1, boundedness of the planar flows for r > 2 and existence of solutions for r ≤ 1 are conventional proofs, and the paper is an unrefereed preprint.

Cite

Citation file papers/mathematics/nesterov-subcritical/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026nesterovsubcritical,
  author = {Goyal, Dev D.},
  title = {Escaping {Nesterov} Flows and Iterates below Critical Damping},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/nesterov-subcritical}
}