{"id":"arxiv/2609.33842","url":"https://arxiv.org/abs/2609.33842","tags":["math.DG"],"score":0,"title":"A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture","domain":"math.DG","source":"arxiv","authors":["Ziyang Qin","Yuan Liao","Ayush Khaitan","Bennett Chow"],"reviews":0,"subject":"math.DG","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-27","reactions":{}}