Paper · Sep 27, 2026

A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture

Ziyang Qin, Yuan Liao, Ayush Khaitan, Bennett Chow

math.DGarXiv:2609.33842
PDF Abstract page

As on arXiv

Abstract

We formalize the smooth three-dimensional Poincaré conjecture, together with the Moise smoothing theorem, yielding the topological three-dimensional Poincaré conjecture. The smooth proof follows the Hamilton–Perelman route through Ricci flow with surgery and finite-time extinction.

Ricci flowSingularitiesSurgeryPoincaré conjecture3-manifolds

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 Ricci Flow and the Poincare Conjecture (John W. Morgan and Gang Tian, 2006)5Morgan 2006 Hamilton-Perelman's Proof of the Poincaré Conjecture and the Geometrization Conjecture (Huai-Dong Cao and Xi-Ping Zhu, 2006)4Cao 2006 Completion of the Proof of the Geometrization Conjecture (John Morgan and Gang Tian, 2008)8Morgan 2008 On 4-dimensional smooth Poincare conjecture (Selman Akbulut, 2022)3Akbulut 2022 Moving Manifolds and the Poincare Conjecture (David V. Svintradze, 2025)6Svintradze 2025 Equations in Products of Free Groups and 3-Manifold Groups, I (Olga Kharlampovich and Alina Vdovina, 2026)7Kharlampovic 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 Thurston's Geometrization Conjecture (Yuan Liao, Ziyang Qin, Jui-Hui Chung et al., 2026)1Liao 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 Thurston's Geometrization Conjecture

    Yuan Liao, Ziyang Qin, Jui-Hui Chung et al. PDF

    Topics Ricci flow · Same authors Ziyang Qin, Yuan Liao, 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 3-manifolds, Singularities · Same authors Ziyang Qin, Yuan Liao, Bennett Chow · Shared terms “Lean formalization”, “Hamilton”

  3. On 4-dimensional smooth Poincare conjecture

    Selman Akbulut PDF

    Topics Poincaré conjecture

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

    Huai-Dong Cao and Xi-Ping ZhuThe canon PDF

    Topics Poincaré conjecture, 3-manifolds · Shared terms “Perelman proof”, “Hamilton”

  5. Ricci Flow and the Poincare Conjecture

    John W. Morgan and Gang TianThe canon PDF

    Topics Poincaré conjecture · Shared terms “Perelman”

  6. Moving Manifolds and the Poincare Conjecture

    David V. Svintradze PDF

    Topics Poincaré conjecture, Surgery

  7. Equations in Products of Free Groups and 3-Manifold Groups, I

    Olga Kharlampovich and Alina Vdovina PDF

    Topics Poincaré conjecture, 3-manifolds · Shared terms “Perelman proof”

  8. Completion of the Proof of the Geometrization Conjecture

    John Morgan and Gang TianThe canon PDF

    Topics Poincaré conjecture, Surgery, 3-manifolds · Shared terms “Perelman”, “together”

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) Singularities On a closed manifold the flow usually cannot run forever: curvature blows up in finite time, often because a neck pinches off. Start with: The formations of singularities in the Ricci Flow (Hamilton, 1993) Surgery Stop the flow just before a neck pinches, cut along the thin neck, glue standard caps onto the two ends, and restart. Start with: Four-manifolds with positive isotropic curvature (Hamilton, 1997) Poincaré conjecture Every closed, simply connected 3-manifold is homeomorphic to the 3-sphere. Poincaré posed the question in 1904, and Perelman proved it in 2002–03… Start with: Generalized Poincare's Conjecture in Dimensions Greater Than Four (Smale, 1961)

In the guidebook

  1. 11B.7
    Hamilton’s Program in 2002Book 11B · Solitons, Compactness and Singularities

    What was proved, what was missing, and where Perelman came in.

  2. 10A.4
    Homotopy Groups, Degree and the Hurewicz TheoremBook 10A · Three-Manifolds and Geometrization

    Spheres mapped into manifolds: the algebraic topology that finite extinction runs on.

  3. 10A.6
    Necks, Caps and Their TopologyBook 10A · Three-Manifolds and Geometrization

    What an ε-neck is, how necks overlap and chain into tubes, and which manifolds necks and caps can build.