A Lean Formalization of Hamilton's Three-Manifold Theorem
Bennett Chow, Yuan Liao, Ziyang Qin
math.DG
Aug 21, 2026 · v1
math.AP math.GT
TL;DR
Formalizes Hamilton's 1982 three-manifold theorem in Lean/Mathlib, building Ricci-flow, tensor calculus, maximum principles, and pinching infrastructure.
Abstract
We describe a Lean formalization of Hamilton's 1982 theorem on closed, connected three-manifolds with positive Ricci curvature. The development contains a short-time existence theorem for Ricci flow and substantial geometric-analysis infrastructure: Riemannian tensor calculus, the Levi–Civita connection, Ricci-flow evolution equations, scalar and tensor maximum principles, three-dimensional curvature algebra, preservation of Ricci pinching, and Hamilton's improved pinching estimate. The formalization follows an alternative blow-up route, rather than Hamilton's original normalized-flow proof. Its time-uniform short-time existence, maximal continuation, no-local-collapsing, and Cheeger–Gromov–Hamilton compactness pipelines have been formalized and are included in the artifact, while we give only a brief account of these companion developments and record the interfaces and consequences used by the Hamilton argument; a detailed exposition of their full constructions is deferred to the second author's forthcoming thesis. We interweave representative Lean declarations with their mathematical meaning and record the status and provenance of every major component. All source-level status claims are tied to the source release identified below.
Problem
Hamilton's 1982 theorem states that a closed connected smooth three-manifold admitting a metric of positive Ricci curvature admits a metric of constant positive sectional curvature. Formalizing this requires substantial geometric-analysis infrastructure not present in existing proof-assistant libraries.
Approach
The development builds a Ricci-flow-oriented Lean layer over Mathlib's manifold and differential-calculus framework, including Riemannian tensor calculus, the Levi-Civita connection, tensor bundles, and Ricci-flow evolution equations. Short-time existence is constructed via a fixed-background Ricci-DeTurck spectral-resolvent and fixed-point method rather than a black-box parabolic theorem. Scalar and tensor maximum principles, three-dimensional curvature algebra, and preservation of Ricci pinching are formalized, and the proof follows a blow-up route with no-local-collapsing and Cheeger-Gromov-Hamilton compactness pipelines.
Results
A checked Lean endpoint hamilton_positive_ricci is established whose transitive axiom audit contains only standard Lean/Mathlib classical and quotient axioms. Companion developments (noncollapsing, injectivity control, compactness) are included in the release, with full expositions deferred to forthcoming work.
