Showing math.DGShow all
2 papers · 1 filter
math.DG2026
A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
Ziyang Qin, Yuan Liao, Ayush Khaitan +1
We formalize the smooth three-dimensional Poincaré conjecture, together with the Moise smoothing theorem, yielding the topological three-dimensional Poincaré conjecture. The smooth…
math.DG2026
A Lean Formalization of Hamilton's Three-Manifold Theorem
Bennett Chow, Yuan Liao, Ziyang Qin
We describe a Lean formalization of Hamilton's 1982 theorem on closed, connected three-manifolds with positive Ricci curvature. The development contains a short-time existence theo…