# A Lean Formalization of Hamilton's Three-Manifold Theorem (Chow, Liao, Qin)

> Lean formally verifies Hamilton's 1982 theorem that closed 3-manifolds with positive Ricci curvature admit constant positive sectional curvature metrics, using 1.9 million lines of code.

- **Source:** [arXiv](https://arxiv.org/abs/2608.21502)
- **Published:** 2026-10-03
- **Permalink:** https://picx.dev/p/TaRE04
- **Whiteboard:** https://picx.dev/p/TaRE04/image

## Summary

# Summary of "A Lean Formalization of Hamilton's Three-Manifold Theorem"

## Summary (Overview)

- **Formal verification milestone**: The paper describes a complete Lean formalization of Hamilton's 1982 theorem establishing that closed connected three-manifolds with positive Ricci curvature admit metrics of constant positive sectional curvature (equivalently, are spherical space forms).

- **Scale of development**: The formal artifact contains **1,945,081 lines** of tracked Lean source code, built on Lean 4 v4.29.0 and mathlib v4.29.0, with the repository available at https://github.com/qinz1yang/differential-geometry.

- **Proof architecture**: Rather than following Hamilton's original normalized-flow proof, the formalization uses an alternative blow-up route requiring short-time existence, maximal continuation, no-local-collapsing, and Cheeger–Gromov–Hamilton compactness.

- **Audited trust boundary**: The endpoint theorem `hamilton_positive_ricci` has a transitive axiom report containing only `propext`, `Classical.choice`, and `Quot.sound` — no `sorryAx` or project-specific axioms.

- **Methodological innovation**: The project employed a novel top-down workflow with language-model agents for proof decomposition, while maintaining human responsibility for mathematical direction and statement correctness.

## Introduction and Theoretical Foundation

### The Mathematical Target

The paper formalizes **Theorem 1.1 (Hamilton 1982)**: If $M^3$ is a closed, connected smooth three-manifold admitting a metric $g_0$ with positive Ricci curvature, then $M^3$ admits a metric $g_\infty$ with constant positive sectional curvature.

The Ricci flow equation is:
$$\frac{\partial}{\partial t} g = -2 \text{Ric}$$

### Proof Route Selection

The authors chose a **blow-up route** over Hamilton's original normalized-flow proof because:
- The original route requires long-time normalized-flow theory and gradient estimates
- The blow-up route leverages Perelman's no-local-collapsing and Cheeger–Gromov–Hamilton compactness
- The finite-time blow-up approach is more modular and suitable for formalization

### Key Infrastructure Layers

The development builds on:
- mathlib's manifold, vector-bundle, and calculus infrastructure
- Project-local tensor bundle constructions (`Tensor0SSpace`, `TensorRSSpace`)
- A complete differential-geometric foundation including the Levi-Civita connection

## Methodology

### Tensor Bundles and Geometric Foundations

The formalization handles the subtle type-theoretic issues of tensor fields as sections of tensor bundles:

```lean
def Tensor0SSpace (s : Nat) (I : ModelWithCorners K E H)
[IsManifold I 1 M] (x : M) : Type _ :=
Bundle.continuousMultilinearMap K s E (TangentSpace I) x
```

### Levi-Civita Connection Construction

The connection is constructed directly from the Koszul formula rather than chosen as an object satisfying axioms:

$$2\langle\nabla_X Y, Z\rangle_g = K_g(X, Y, Z)$$

with key theorems:
- `LeviCivita_torsion_eq_zero`: torsion-freeness
- `LeviCivita_isMetricCompatible`: metric compatibility

### Short-Time Existence via DeTurck's Gauge Reduction

The formalization uses the Ricci–DeTurck flow:
$$\partial_t h = -2\text{Ric}(h) + \mathcal{L}_W h, \quad h(0) = g_0$$

with the key theorem:

```
theorem ricci_flow_short_time_existence ... :
∃ T > 0, ∃ g_fam : R → SmoothRiemannianMetric I M,
  g_fam 0 = g_0 ∧ ... 
```

The proof follows a **spectral Hilbert-space route** with:
- Compact self-adjoint tensor resolvent operators
- Spectral Sobolev scale (`tensorHs`)
- Maximal regularity theory
- Modewise evolution on eigenbasis

### Maximum Principles

**Scalar weak maximum principle**: If $\partial_t u \geq \Delta u + \langle X, \nabla u\rangle + F(u,t)$ and $u(\cdot,0) \geq c(0)$ where $c' = F(c,t)$, then $u(x,t) \geq c(t)$.

**Tensor maximum principle** (Hamilton's): For symmetric 2-tensors $S(t)$ satisfying
$$(\partial_t - \Delta)S_{ij} \geq X^k\nabla_k S_{ij} + N_{ij}(S,g,t)$$
with null-eigenvector condition, preservation of $S \geq 0$ follows.

### Three-Dimensional Curvature Algebra

In dimension 3, Riemann is determined by Ricci:
$$R_{ijkl} = \text{Ric}_{i\ell}g_{jk} - \text{Ric}_{jk}g_{i\ell} - \text{Ric}_{ik}g_{j\ell} + \text{Ric}_{j\ell}g_{ik} - \frac{R}{2}(g_{i\ell}g_{jk} - g_{j\ell}g_{ik})$$

## Empirical Validation / Results

### Key Formalized Theorems

**Theorem 4.1 (Short-time existence)**: For closed manifolds with smooth initial metric $g_0$, there exists $T > 0$ and a smooth Ricci flow $g(t)$ on $[0,T)$ with $g(0) = g_0$.

**Theorem 4.2 (Class-uniform existence)**: 
$$\exists \tau_0 > 0, \forall g_0 \in \mathcal{G}_3(\bar{g}, \Lambda), \text{ the Ricci flow from } g_0 \text{ exists on } [0, \tau_0).$$

**Theorem 6.8 (Preservation of nonnegative Ricci curvature in 3D)**: If $\text{Ric}(g(0)) \geq 0$, then $\text{Ric}(g(t)) \geq 0$ for all times.

**Theorem 6.9 (Preservation of Ricci pinching)**: For $0 < \delta < 1/3$, if $\text{Ric}(g(0)) \geq \delta R(g(0))g(0)$, then the inequality is preserved.

**Corollary 6.19 (Improved pinching estimate)**: There exist $\varepsilon > 0$, $C < \infty$ such that
$$\frac{|\text{Ric}^\circ|^2}{R^{2-\varepsilon}} \leq C$$

### Finite-Time Blow-Up

**Theorem 7.5**: For maximal Ricci flow on closed three-manifold with positive scalar curvature:
$$\forall K \in \mathbb{R}, \exists t \in [0,\omega), \exists x \in M, K < |\text{Rm}(S(t))|^2_x$$

The maximal time satisfies $T_{max} \leq \frac{3}{2c_0}$ where $c_0 = \min_M R(g_0) > 0$.

### Noncollapsing and Compactness

**Theorem 8.1 (Uniform noncollapsing)**: There exist $r > 0$, $\kappa > 0$ such that for the blow-up sequence:
- Curvature control: $|\text{Rm}_{g_i}| \leq r^{-2}$ on backward parabolic neighborhood
- Volume lower bound: $\text{Vol}_{g_i(0)} B_{g_i(0)}(x_i, r) \geq \kappa r^3$

**Theorem 8.2 (Compactness)**: Under curvature, injectivity, and completeness hypotheses, there exists a pointed Ricci flow limit with smooth Cheeger–Gromov–Hamilton convergence.

## Theoretical and Practical Implications

### Mathematical Significance

The formalization confirms the viability of formalizing deep results in geometric analysis using modern proof assistants. It provides:

1. **Reusable infrastructure**: Tensor calculus, Levi-Civita connections, and parabolic PDE machinery that can serve future formalization projects
2. **Precise statement verification**: Forces explicit formulation of hypotheses, conventions, and regularity conditions
3. **Path toward Poincaré conjecture**: Serves as the first milestone in formalizing the Hamilton–Perelman program

### Methodological Innovation

**AI-assisted formalization with human oversight**:
- Three-tier workflow: leader (mathematical direction), orchestrator (dependency management), workers (bounded proof tasks)
- Consumer-driven top-down descent: statements decomposed from headline theorem
- Adversarial statement review: refuters search for degenerate witnesses and overstrong statements
- Mechanical acceptance gates: axiom audits, dependency checks, placeholder scans

The trust boundary is precisely defined:
- The Lean kernel verifies proof terms
- Theorem-specific axiom reports show only `propext`, `Classical.choice`, `Quot.sound`
- Human responsibility: mathematical definitions, theorem statements, and semantic correctness

### Formal Verification Status

The short-time existence theorem, the Hamilton finite-time blow-up endpoint, and the final three-manifold theorem are all **closed** — meaning their proofs compile and have complete axiom reports without `sorryAx` or project-specific axioms.

## Conclusion

The paper presents a complete Lean formalization of Hamilton's three-manifold theorem, representing a significant milestone in formalized mathematics. The development includes:

- **Complete short-time existence theory** for Ricci flow via DeTurck's gauge reduction with spectral methods
- **Differential-geometric foundations**: tensor bundles, Levi-Civita connection, covariant derivatives
- **Analytic infrastructure**: maximum principles, evolution equations, three-dimensional curvature algebra
- **Global assembly**: maximal flows, noncollapsing, compactness, and the final blow-up argument

**Future directions** identified by the authors include:
- Generalizing the PDE infrastructure to arbitrary quasilinear systems
- Developing Schauder estimates and Hölder-space machinery
- Extending toward the full Hamilton–Perelman program and the Poincaré conjecture
- Improving library interfaces for broader geometric-analysis formalization projects

The project demonstrates that with appropriate methodology combining AI assistance and human oversight, deep results in geometric analysis can be formally verified, providing a model for future large-scale formalization efforts.

---

_Markdown view of https://picx.dev/p/TaRE04, served by PicX — AI-generated visual whiteboard summaries of research papers._