{"id":"arxiv/2608.21502","url":"https://arxiv.org/abs/2608.21502","tags":["math.DG","math.AP","math.GT"],"score":0,"title":"A Lean Formalization of Hamilton's Three-Manifold Theorem","domain":"math.DG","source":"arxiv","authors":["Bennett Chow","Yuan Liao","Ziyang Qin"],"reviews":0,"subject":"math.DG","summary":"We describe a Lean formalization of Hamilton's 1982 theorem on closed, connected three-manifolds with positive Ricci curvature. The development contains a short-time existence theorem for Ricci flow and substantial geometric-analysis infrastructure: Riemannian tensor calculus, the Levi--Civita connection, Ricci-flow evolution equations, scalar and tensor maximum principles, three-dimensional curvature algebra, preservation of Ricci pinching, and Hamilton's improved pinching estimate. The formalization follows an alternative blow-up route, rather than Hamilton's original normalized-flow…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-21","reactions":{}}