Thurston’s geometrization conjecture formalised in Lean

Your AI and this story

Key facts

• Paper: ‘A Lean Formalization of the Hamilton–Perelman Proof of Thurston’s Geometrization Conjecture’, arXiv 2610.13897 [math.DG], 9 Oct 2026; Yuan Liao and Ziyang Qin contributed equally. Affiliations: UC San Diego, Cornell, Princeton AI (Princeton University), Tsinghua University, Amazon AGI, NVIDIA Research, University of Oregon
• Theorem formalized: every connected, closed, oriented smooth three-manifold is a connected sum of prime manifolds; each prime factor contains finitely many disjoint, smoothly embedded incompressible tori, and the interior of every piece cut along them carries a complete metric locally isometric to one of the eight Thurston geometries (finite volume in the hyperbolic case)
• Scope stated by the authors: the statement ‘does not require the cutting tori to form the canonical JSJ family’, does not require the family to be minimal and makes ‘no uniqueness assertion’; the prime convention allows S³ as a factor
• Verification (paper): ‘successful endpoint and complete-library builds, a separate consumer of the expanded public statement, and transitive axiom checks’; the four public declarations yield the same axiom set ‘[propext, Classical.choice, Quot.sound]’ and ‘contain neither sorryAx nor a project-specific axiom’. The authors add that the ‘mathematical interpretation also requires review of the definitions and hypotheses’
• AI role (Section 3, ‘Agent-assisted formalization with Humanize’): the Humanize RLAR workflow (‘Ralph Loop with Agentic Review’) separates a builder agent from an independent reviewer. ‘We use GPT-6-Astra as the reviewer. For the builder, we choose among GPT-6-Luna, GPT-6-Sol, GPT-6-Astra, Claude-Opus-5.5, and DeepSeek-V4.1-Flash based on their observed generation speed in tokens per second (TPS).’ ‘Human authors remain responsible for the intended theorem statements, the mathematical interpretation of the formalization, and the final verification claims.’
• Mathematical route: Hamilton’s Ricci-flow program and Perelman’s completion, following Morgan–Tian and Kleiner–Lott; long-time surgery flow, thick-region hyperbolic pieces, the Kleiner–Lott local-collapse argument for graph-manifold pieces, and Hamilton’s incompressibility argument (with Mostow–Prasad rigidity). ‘A fuller account of the analytic and topological constructions will appear elsewhere.’
• Code: github.com/qinz1yang/differential-geometry, release v0.1.5 (preview), published 9 Oct 2026, Lean and Mathlib v4.35.0-rc3, Apache-2.0; the release ‘adds Thurston’s geometrization conjecture for closed, connected, oriented smooth three-manifolds, and three-dimensional Mostow–Prasad rigidity’. The repository had 74 stars on 12 Oct 2026
• Reused sources (paper): the group’s Poincaré development, parts of Armstrong and Kempe’s DeGiorgi library, Jordan–Schönflies, Classification of Compact Surfaces, Tau Ceti and a canonical-topology development