Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 1 h ago
PreprintCC BY 4.0arXiv

A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture

  • Yuan Liao
  • Ziyang Qin
  • Jui-Hui Chung
  • Ayush Khaitan
  • Zhengyang Zhang
  • Hongzhou Lin
  • Zijian Zhang
  • Ligeng Zhu
  • Peng Lu
  • Bennett Chow
Open at sourcePDFDOICite

Abstract

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.

Related

  1. A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
    Ziyang Qin, Yuan Liao, Ayush Khaitan +1
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  2. Geometrization of Kottwitz-Shelstad transfer and Vogan's conjecture on local Arthur packets
    Clifton Cunningham, Alexander Hazeltine, Baiying Liu +4
    arXivPreprintCC BY 4.0Full textAlgebra & number theoryarXiv
  3. An AI-Assisted Formalization of the Poincaré Conjecture
    Zhiyuan Zhang, Axel Delaval, Leheng Chen +6
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  4. Perelman's entropy and Gromov-Hausdorff versus dynamical stability of round spheres
    Reto Buzano, Shengwen Wang
    arXivPreprintarXiv licenceFull textGeometry & topologyarXiv
  5. Thurston equivalence of topological polynomials
    Laurent Bartholdi, Volodymyr V. Nekrashevych
    Acta Math.Peer-reviewedLicence not statedFull text84 citedDynamical systemsHAL

Cite

BibTeXRIS
BibTeX
@misc{liao2026lean,
  title = {{A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture}},
  author = {Yuan Liao and Ziyang Qin and Jui-Hui Chung and Ayush Khaitan and Zhengyang Zhang and Hongzhou Lin and Zijian Zhang and Ligeng Zhu and Peng Lu and Bennett Chow},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.13897},
  eprint = {2610.13897},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.13897},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
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
DA  - 2026/10/09
PB  - arXiv
DO  - 10.48550/arxiv.2610.13897
UR  - https://arxiv.org/abs/2610.13897
AB  - 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.
ER  -