{"id":"arxiv/2610.13897","url":"https://arxiv.org/abs/2610.13897","tags":["math.DG"],"score":0,"title":"A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture","domain":"math.DG","source":"arxiv","authors":["Yuan Liao","Ziyang Qin","Jui-Hui Chung","Ayush Khaitan","Zhengyang Zhang","Hongzhou Lin","Zijian Zhang","Ligeng Zhu","Peng Lu","Bennett Chow"],"reviews":0,"subject":"math.DG","summary":"We formalize the Hamilton--Perelman Ricci-flow proof of Thurston's geometrization conjecture. The public Lean declaration is reproduced in this paper. Its geometric interpretation follows, and verification is recorded in 4.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-09","reactions":{}}