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

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.