Paper · Oct 9, 2026

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.DGarXiv:2610.13897
PDF Abstract page

As on arXiv

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.

Ricci flowGeometrization

Its neighbourhood

Connected papers

The 8 papers on this site closest to this one, judged by the topics they share, the words and phrases in their titles and abstracts, and their authors. They are not its citations, but a map of the work around it. Papers here go back to 2021, plus the canon.

Connected papers This paper in the centre and the 8 papers closest to it around it, in date order clockwise from the top. The closer a paper sits to the centre, the stronger the connection. This paper The entropy formula for the Ricci flow and its geometric applications (Grisha Perelman, 2002)5Perelman 2002 Hamilton-Perelman's Proof of the Poincaré Conjecture and the Geometrization Conjecture (Huai-Dong Cao and Xi-Ping Zhu, 2006)3Cao 2006 Completion of the Proof of the Geometrization Conjecture (John Morgan and Gang Tian, 2008)7Morgan 2008 Geometrization in Geometry (Izabella Muraro de Freitas and Álvaro Krüger Ramos, 2022)4de Freitas 2022 Large-scale geometry of the Universe (Yassir Awwad and Tomislav Prokopec, 2022)8Awwad 2022 Modifications of CMB Temperature and Polarization Quadrupole Signals in Thurston Spacetimes (Tanay Gupta, Sukanta Panda and Rajib Saha, 2026)6Gupta 2026 A Lean Formalization of Hamilton's Three-Manifold Theorem (Bennett Chow, Yuan Liao and Ziyang Qin, 2026)2Chow 2026 A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture (Ziyang Qin, Yuan Liao, Ayush Khaitan et al., 2026)1Qin 2026
Closer to the centre: more closely connected. Clockwise from the top: oldest to newest. Ricci flowWider flowsalso connected to each other
  1. A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture

    Ziyang Qin, Yuan Liao, Ayush Khaitan et al. PDF

    Topics Ricci flow · Same authors Yuan Liao, Ziyang Qin, Ayush Khaitan · Shared terms “Lean formalization”, “Perelman proof”, “Hamilton”

  2. A Lean Formalization of Hamilton's Three-Manifold Theorem

    Bennett Chow, Yuan Liao and Ziyang Qin PDF

    Topics Ricci flow · Same authors Yuan Liao, Ziyang Qin, Bennett Chow · Shared terms “Lean formalization”, “Hamilton”, “Lean declaration”

  3. Hamilton-Perelman's Proof of the Poincaré Conjecture and the Geometrization Conjecture

    Huai-Dong Cao and Xi-Ping ZhuThe canon PDF

    Topics Geometrization · Shared terms “geometrization conjecture”, “Perelman proof”, “Hamilton”

  4. Geometrization in Geometry

    Izabella Muraro de Freitas and Álvaro Krüger Ramos PDF

    Topics Geometrization · Shared terms “Thurston”, “Hamilton”, “Perelman”

  5. The entropy formula for the Ricci flow and its geometric applications

    Grisha PerelmanThe canon PDF

    Topics Geometrization · Shared terms “Thurston geometrization”, “geometrization conjecture”, “Hamilton”

  6. Modifications of CMB Temperature and Polarization Quadrupole Signals in Thurston Spacetimes

    Tanay Gupta, Sukanta Panda and Rajib Saha PDF

    Topics Geometrization · Shared terms “Thurston”, “geometrization conjecture”

  7. Completion of the Proof of the Geometrization Conjecture

    John Morgan and Gang TianThe canon PDF

    Topics Geometrization · Shared terms “geometrization conjecture”, “Perelman”

  8. Large-scale geometry of the Universe

    Yassir Awwad and Tomislav Prokopec PDF

    Topics Geometrization · Shared terms “Thurston geometrization”, “geometrization conjecture”, “Perelman”

Read around it

Background reading

The guides for the topics of this paper: what each idea is, why it matters, and the papers to read first.

Ricci flow Hamilton's Ricci flow evolves a Riemannian metric by minus twice its Ricci curvature. It is a nonlinear heat equation for geometry: it spreads… Start with: Three-manifolds with positive Ricci curvature (Hamilton, 1982) Geometrization Thurston's conjecture: every closed 3-manifold can be cut along spheres and tori into pieces that each carry one of eight model geometries. Start with: Three dimensional manifolds, Kleinian groups and hyperbolic geometry (Thurston, 1982)

In the guidebook

  1. 10A.2
    Finite Rotation Groups and Spherical Space FormsBook 10A · Three-Manifolds and Geometrization

    Klein's classification by counting poles, the binary groups, and every quotient of the round 3-sphere.

  2. 10A.8
    Thurston’s Eight GeometriesBook 10A · Three-Manifolds and Geometrization

    The model geometries, the geometrization conjecture, and why it implies Poincaré.

  3. 10A.9
    Hyperbolic Three-ManifoldsBook 10A · Three-Manifolds and Geometrization

    Ideal tetrahedra, Mostow rigidity, and the thick–thin decomposition.