← All papers
First page of A Complete Resolution of Forsythe's Conjecture for Restarted Conjugate Gradients

A Complete Resolution of Forsythe's Conjecture for Restarted Conjugate Gradients

Matthew J. Colbrook, George Stepaniants, Alex Townsend

math.NA Sep 4, 2026 · v2 math.DS math.OC
The classification of restarted conjugate-gradient residual dynamics for all restart lengths s>=2 is formally verified in Lean.
Forsythe's conjecture, published in 1968, asserts that for each restart length $s$, every exact-arithmetic restarted conjugate-gradient iteration on a real symmetric positive definite problem either terminates or has normalised residuals that converge separately along the even and odd restart subsequences. Apart from the classical steepest-descent case, this asymptotic question remained unresolved in full generality for nearly six decades. We give a complete classification by restart length in the original finite-dimensional setting and identify a sharp threshold. For $s=2$ and $s=3$, every problem either terminates or has convergent even and odd residual directions. For every $s\ge4$, there is a diagonal positive definite counterexample of dimension $s+4$ which never terminates and whose even residual directions do not converge. Together with Akaike's theorem for $s=1$, this shows that the conjectured universal conclusion is true precisely for $s\in\{1,2,3\}$ and false for every $s\ge4$. The positive results follow from a degree-independent double-orthogonality identity and an analysis of the low-degree fixed-point sets. At restart length four, rational interval arithmetic and Sturm sequences certify a transverse Hopf point of the leading vector field of the rescaled squared-weight map. Analytic periodic-orbit and shadowing arguments yield the counterexample at restart length four, and degree elevation extends the construction to every larger restart length. The classification for all $s\ge2$ is also formally verified in Lean.

Forsythe's 1968 conjecture asserts that exact-arithmetic restarted conjugate gradients on SPD problems either terminate or have residual directions converging separately along even and odd restart subsequences. The classification by restart length s remained unresolved in general for nearly six decades.

The authors reduce the iteration to a nonlinear map on a probability simplex over active spectral nodes using a degree-independent double-orthogonality identity. Low-degree fixed-point sets are analyzed for s=2 and s=3 to prove convergence. For s=4, rational interval arithmetic and Sturm sequences certify a transverse Hopf point, yielding a periodic-orbit and shadowing counterexample, extended to larger s by degree elevation. The full classification for all s>=2 is formally verified in Lean.

Convergence holds for s in {2,3}; for every s>=4 there is a diagonal positive-definite counterexample of dimension s+4 that never terminates and whose even residual directions do not converge. With Akaike's s=1 result, the conjectured conclusion is true exactly for s in {1,2,3} and false for all s>=4.