Thurston's geometrization conjecture gives a complete characterization of geometric structures on three-dimensional manifolds.
Before stating Thurston's geometrization conjecture in detail, some background information is useful. Three-dimensional manifolds possess what is known as a standard two-level decomposition. First, there is the connected sum decomposition, which says that every compact three-manifold is the connected sum of a unique collection of prime three-manifolds.
The second decomposition is the Jaco-Shalen-Johannson torus decomposition, which states that irreducible orientable compact 3-manifolds have a canonical (up to isotopy) minimal collection of disjointly embedded incompressible tori such that each component of the 3-manifold removed by the tori is either "atoroidal" or "Seifert-fibered."
Thurston's conjecture is that, after you split a three-manifold into its connected sum and the Jaco-Shalen-Johannson torus decomposition, the remaining components each admit exactly one of the following geometries:
4. The geometry of 
,
5. The geometry of 
,
6. The geometry of the universal cover 
of the Lie group 
,
7. Nil geometry, or
8. Sol geometry.
Here, 
is the 2-sphere (in a topologist's
sense) and 
is the hyperbolic plane.
The geometrization theorem implies the Poincaré
conjecture. Perelman (2002, 2003) completed Hamilton's Ricci
flow program to prove the result. Morgan and Tian (2014) give a detailed account
of the proof.
Liao et al. (2026) report a Lean formalization of the Hamilton-Perelman proof. Its endpoint gives a connected sum decomposition into prime manifolds and cuts along smooth incompressible tori, with complete geometric metrics on the piece interiors. It does not assert that the cutting tori form the canonical minimal Jaco-Shalen-Johannson torus decomposition. Liao et al. (2026) report successful library builds and only the standard Lean axioms in the endpoint's dependency closure. The formal artifact has not been independently rebuilt here. Liao et al. (2026) used AI builder and reviewer agents, while retaining human responsibility for the mathematical statements and their interpretation.
