State of the art, September 2026

Hamilton’s theorem is no longer open. Chow, Liao and Qin (arXiv:2608.21502, 21 August 2026) give a Lean formalization of it: the endpoint hamilton_positive_ricci concludes constant positive sectional curvature and spherical space form from closed connected three-manifold and admits positive Ricci, with no auxiliary hypotheses, no sorry and no project axiom. Their library is roughly \(1.9\) million lines. It closes, in the language of this chart, Chapter 6’s short-time existence and maximal continuation, Shi’s estimates, both maximum principles, Theorem 100, Theorem 128 and Theorem 135 — that is, both of the analytic gaps this overview names above, together with the whole of Chapter 7.

So the frontier has moved, and it has moved past the two obstacles that were supposed to be the hard ones. What is left between here and Corollary 147 is no longer parabolic existence theory. It is, in dependency order:

• Theorem 129, the Hamilton–Ivey estimate — an ODE invariant set plus a time-dependent tensor maximum principle, with no new analysis in it at all, and absent from their library;

• Definition 126 and Theorem 127, Perelman’s \(\mathcal{L}\)-geometry — two chapters of comparison geometry built on the flow, needing Jacobi fields and the second variation but no parabolic theory, and likewise absent;

• Theorem 137 and Theorem 139, which consume the two above together with the compactness theory that now exists;

• Theorem 143 and Theorem 144, which carry the two remaining parabolic prerequisites — harmonic map flow and curve-shrinking flow.

The first two items are the ones reachable from what is proved here.