Papers With

← All papers
First page of A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture

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

Ziyang Qin, Yuan Liao, Ayush Khaitan, Bennett Chow

math.DG Sep 27, 2026 · v1
formalization geometry topology
Read PDF arXiv abstract Code
TL;DR
Formalizes the smooth and topological three-dimensional Poincaré conjecture via the Hamilton–Perelman Ricci flow route in Lean 4 with Mathlib.
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.
Problem

The three-dimensional Poincaré conjecture, that every simply-connected closed three-manifold is homeomorphic to the 3-sphere, had a proof via Hamilton–Perelman Ricci flow but no formal verification.

Approach

The smooth Poincaré conjecture is formalized in Lean 4 with Mathlib following the Hamilton–Perelman route through Ricci flow with surgery and finite-time extinction. Key components include short-time existence via DeTurck's method, Hamilton–Ivey pinching, Perelman noncollapsing, canonical neighborhood and surgery interfaces, and a least-area width argument for extinction. The Moise smoothing theorem is formalized to transfer the smooth result to the topological statement, adapting developments from several external Lean projects.

Results

The endpoints smoothPoincareConjecture_holds and poincare_conjecture are proven, matching statements marked proof_wanted in Mathlib v4.33.1, with no additional hypotheses, and axiom closures reducing to propext, Classical.choice, and Quot.sound.