Papers With

← All papers
First page of A Lean Formalization of the Hamilton–Perelman Proof of Thurston's Geometrization Conjecture

A Lean Formalization of the Hamilton–Perelman Proof of Thurston's Geometrization Conjecture

Yuan Liao, Ziyang Qin, Jui-Hui Chung, Ayush Khaitan, Zhengyang Zhang, Hongzhou Lin, Zijian Zhang, Ligeng Zhu, Peng Lu, Bennett Chow

math.DG Oct 9, 2026 · v1
formalization ai-agents geometry topology
Read PDF arXiv abstract Code
TL;DR
Formalizes the Hamilton–Perelman Ricci-flow proof of geometrization in Lean 4 with Mathlib, using LLM agents for builder/reviewer roles, with a pinned repository.
Abstract
We formalize the Hamilton–Perelman Ricci-flow proof of Thurston's geometrization conjecture. The public Lean declaration is reproduced in this paper. Its geometric interpretation follows, and verification is recorded in 4.
Problem

Thurston's geometrization conjecture, proved by Hamilton and Perelman via Ricci flow with surgery, has not previously been machine-checked. The goal is a formal Lean statement and proof of the full decomposition of closed oriented 3-manifolds into geometric pieces.

Approach

The formalization follows Hamilton's Ricci-flow program and Perelman's completion, as organized by Morgan–Tian and Kleiner–Lott. It reuses components from a prior Lean Poincaré conjecture development, including long-time surgery flow, thick-region hyperbolic analysis, local collapse, and Seifert-fibered geometry. The Lean code was produced with the Humanize RLAR workflow, in which a builder LLM agent writes code and an independent reviewer agent checks it, under human oversight. Checks included kernel checking, statement-preservation checks, and independent proof verification.

Results

The public endpoint GC.Endpoint.geometrization states prime decomposition, incompressible torus decomposition, and a Thurston geometry on each piece, with finite volume for hyperbolic pieces. It builds with Lean/Mathlib v4.35.0-rc3 and depends only on the standard axioms propext, Classical.choice, and Quot.sound. The artifact is released as tag v0.1.5 (preview) at a pinned commit.