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

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.