发表机构
Cornell University; University of California San Diego; Princeton Language and Intelligence, DaIS, Princeton University; Department of Mathematics, University of California San Diego（康奈尔大学; 加州大学圣地亚哥分校; 普林斯顿语言智能与数据科学研究所，普林斯顿大学; 加州大学圣地亚哥分校数学系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文用 Lean 形式化证明了三维庞加莱猜想，结合 Moise 定理，采用 Ricci 流与手术及有限时间消没的 Hamilton–Perelman 方法。
AI 中文摘要
我们将光滑三维庞加莱猜想连同 Moise 光滑化定理一起形式化，从而得出拓扑三维庞加莱猜想。该光滑证明遵循 Hamilton–Perelman 路线，通过带手术的 Ricci 流和有限时间消没来实现。
英文摘要
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.
