Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.13897

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
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

math.DG

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yuan Liao, Ziyang Qin, Jui-Hui Chung, Ayush Khaitan, Zhengyang Zhang, Hongzhou Lin, Zijian Zhang, Ligeng Zhu, Peng Lu, Bennett Chow. 2026-10-09. A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture. https://arxiv.org/abs/2610.13897

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Lojasiewicz inequalities for maps of the 2-sphere

We prove a Lojasiewicz-Simon inequality $$ \left| E(u) - 4πn \right| \leq C \| \mathcal{T}(u) \|^α$$ for maps $u \in W^{2,2}\left( S^2, S^2 \right).$ The inequality holds with $α= 1$ in general and with $α> 1$ unless $u$ is nearly constant on an open set. We obtain polynomial convergence of weak solutions of harmonic map flow $u(t) : S^2 \to S^2$ as $t \to \infty$ on compact domains away from the singular set, assuming that the body map is nonconstant. The proof uses Topping's repulsion estimates together with polynomial lower bounds on the energy density coming from a bubble-tree induction argument.

math.DG↗
arXiv2026

Butcher series for Hamiltonian Poisson integrators through symplectic groupoids

We exhibit a new pre-Lie algebra in the framework of symplectic groupoids and, in turn, use Butcher trees to compute the Taylor series of a solution of a Hamilton-Jacobi equation on any symplectic groupoid $\mathcal{G} \rightrightarrows M.$ The impact of this new algebraic approach is twofold. On the geometric side, it yields algebraic operations to approximate Lagrangian bisections of $\mathcal{G}$ using the Butcher-Connes-Kreimer Hopf algebra and, in turn, aims at a better understanding of the group of Hamiltonian diffeomorphisms of $M.$ On the computational side, we define a new class of Poisson integrators for Hamiltonian dynamics on Poisson manifolds.

math.DG↗
arXiv2026

Urysohn width of hypersurfaces and positive macroscopic scalar curvature

We prove that if a complete Riemannian $n$-manifold with non-trivial codimension 1 homology with $\mathbb{Z}_2$-coefficients or $\mathbb{Z}$-coefficients has positive macroscopic scalar curvature large enough, then it contains a non-nullhomologous hypersurface of small Urysohn $(n-2)$-width. This constitutes a macroscopic analogue of a theorem by Bray--Brendle--Neves on the area of non-contractible 2-spheres in a closed Riemannian 3-manifold with positive scalar curvature. Our proof is based on an adaptation of Guth's macroscopic version of the Schoen-Yau descent argument.

math.DG↗