1 Overview

The first milestone is Hamilton’s 1982 theorem: a closed \(3\)-manifold admitting a metric of strictly positive Ricci curvature admits a metric of constant positive sectional curvature. The terminal node is the spherical space form theorem — a closed \(3\)-manifold with finite fundamental group is \(S^3/\Gamma \) — which Perelman proved in 2003 and which contains the Poincaré conjecture as the case \(\Gamma = 1\). Mathlib states that corollary, unproved, in Mathlib/Geometry/Manifold/PoincareConjecture.lean.

The road is charted to the space form theorem rather than to geometrization on purpose. Finite extinction time makes the long-time behaviour of the flow irrelevant, which removes collapsing theory, graph manifolds, and the JSJ decomposition from the dependency graph entirely — see the end of Chapter 12.

The obstacle is usually said to be analysis, and eventually it is — but not first. When this blueprint began, Riemannian curvature did not exist in Mathlib at all: the library had manifolds, vector bundles, and covariant derivatives, but no Riemann tensor, no \(\operatorname {Ric}\), and not one occurrence of the string sectional. A project planning around the parabolic gap therefore stalls long before reaching it. Chapters 2 and 3 close that first gap: \(R\), \(\operatorname {Ric}\) and \(K\) are now defined, and Hamilton’s theorem is stated in Lean.

Since then the Levi-Civita connection has landed in Mathlib, and this blueprint proves it is smooth (Theorem 12), so \(\operatorname {Ric}\) is now a function of the metric and the flow is the textbook equation \(\partial _t g= -2\operatorname {Ric}(g)\) (Lemma 42).

The analysis gap itself is real and unmoved. Mathlib has no parabolic PDE theory, no elliptic regularity, and no Sobolev spaces of bundle sections, so short-time existence has nothing to stand on; Chapter 6 marks that region explicitly. It is also wider than usually described: the road needs three distinct parabolic theories — Ricci flow, harmonic map flow, and curve-shrinking flow — and a second independent gap at Cheeger–Gromov compactness (Chapter 10).

Two branches are nevertheless closed end to end, both free of PDE: Chapter 4, where the flow on left-invariant metrics is an ODE, and Chapter 5, Milnor’s curvature formulas.