From Ricci Flow to a Checked Proof: The Poincaré conjecture, the Hamilton–Perelman proof and its Lean formalization, explained (JSP-000007)

Perelman proved the Poincaré conjecture in 2002–2003, completing Hamilton's Ricci-flow programme. In September 2026 Qin, Liao, Khaitan and Chow released a Lean 4 formalization of the Hamilton–Perelman proof (arXiv:2609.33842), and on 27 October 2026 MathDB's verifier labelled an adapted revision Lean verified.

This exposition explains both the mathematics and the formal artifact. It covers Ricci flow as a heat equation for the metric, Perelman's entropy and $\kappa$-noncollapsing, canonical neighbourhoods and surgery, and finite extinction through a topological width, with the width inequality integrated explicitly to an extinction time $T_*$. It then shows how extinction yields $S^3$ via connected sums, van Kampen and Moise smoothing. It maps proof steps to Lean names and reads the MathDB verification record. Every statement is tagged by provenance. All mathematics and formalization are due to the cited authors.

Submitted for the Exposition category of the MathDB × Justin Sun Prize pilot (JSP-000007). Essay + video, v1.0: https://github.com/Thanh-Van-2001/poincare-ricci-flow-exposition/releases/tag/v1.0