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 114 and Theorem 121 — 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 133 is no longer parabolic existence theory. It is, in dependency order:

• Theorem 115, 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 112 and Theorem 113, 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 123 and Theorem 125, which consume the two above together with the compactness theory that now exists;

• Theorem 129 and Theorem 130, 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.