TY  - RPRT
TI  - A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
AU  - Yuan Liao
AU  - Ziyang Qin
AU  - Jui-Hui Chung
AU  - Ayush Khaitan
AU  - Zhengyang Zhang
AU  - Hongzhou Lin
AU  - Zijian Zhang
AU  - Ligeng Zhu
AU  - Peng Lu
AU  - Bennett Chow
PY  - 2026
UR  - https://arxiv.org/abs/2610.13897
ID  - 2610.13897
ER  -