Skip to content
DraconiticResearch
Search Sources API
203,203 studies31 sourcesUpdated 57 min ago
PreprintCC BY 4.0arXiv

A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture

  • Ziyang Qin
  • Yuan Liao
  • Ayush Khaitan
  • Bennett Chow
Open at sourcePDFDOICite

Abstract

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.

Related

  1. A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
    Yuan Liao, Ziyang Qin, Jui-Hui Chung +7
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  2. An AI-Assisted Formalization of the Poincaré Conjecture
    Zhiyuan Zhang, Axel Delaval, Leheng Chen +6
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  3. Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean
    Weinan Wang
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsarXiv
  4. Poincaré compactifications of pullbacks of parallel vector fields under counterexamples to the real Jacobian conjecture
    Francisco Braun, Paulo Machado
    arXivPreprintCC BY 4.0Full textDynamical systemsarXiv
  5. The Generative Mechanism of Dimension: An Axiomatic Construction of Dimensional Conventions (Constructive Mathematics Series, Paper 6; Lean formalization, model-pair independence, numerical evidence)
    Chao Qin
    Zenodo (CERN European Organization for Nuclear Research)PreprintCC BY8 citedGeometry & topologyOpenAlex

Cite

BibTeXRIS
BibTeX
@misc{qin2026lean,
  title = {{A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture}},
  author = {Ziyang Qin and Yuan Liao and Ayush Khaitan and Bennett Chow},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.33842},
  eprint = {2609.33842},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.33842},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
AU  - Ziyang Qin
AU  - Yuan Liao
AU  - Ayush Khaitan
AU  - Bennett Chow
PY  - 2026
DA  - 2026/09/27
PB  - arXiv
DO  - 10.48550/arxiv.2609.33842
UR  - https://arxiv.org/abs/2609.33842
AB  - 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.
ER  -