汉密尔顿三维流形定理的精简形式化
A Lean Formalization of Hamilton's Three-Manifold Theorem
浏览论文内容
中文总结 AI 辅助
该研究完成了汉密尔顿三维流形定理的Lean形式化，采用替代爆破路径而非原始归一化流证明，形式化了里奇流相关关键基础设施及配套流程，为三维流形的里奇曲率研究提供了形式化验证支持。
中文摘要 AI 辅助
我们描述了汉密尔顿1982年关于具有正里奇曲率的闭连通三维流形定理的Lean形式化。该成果包含里奇流的短时间存在性定理及大量几何分析基础设施：黎曼张量演算、列维-奇维塔联络、里奇流演化方程、标量与张量最大值原理、三维曲率代数、里奇捏缩的保持，以及汉密尔顿改进的捏缩估计。该形式化采用替代爆破路径，而非汉密尔顿原始的归一化流证明。其时间一致的短时间存在性、极大延拓、无局部坍缩及Cheeger–Gromov–Hamilton紧性流程已被形式化并包含在产物中；我们仅简要介绍这些配套成果，记录汉密尔顿论证所用的接口与推论，其完整构造的详细阐述将推迟至第二作者即将发表的论文。我们穿插呈现代表性Lean声明及其数学含义，记录各主要组件的状态与来源，所有源代码级状态声明均关联至下文标识的源代码版本。
英文摘要
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 theorem for Ricci flow and substantial geometric-analysis infrastructure: Riemannian tensor calculus, the Levi--Civita connection, Ricci-flow evolution equations, scalar and tensor maximum principles, three-dimensional curvature algebra, preservation of Ricci pinching, and Hamilton's improved pinching estimate. The formalization follows an alternative blow-up route, rather than Hamilton's original normalized-flow proof. Its time-uniform short-time existence, maximal continuation, no-local-collapsing, and Cheeger--Gromov--Hamilton compactness pipelines have been formalized and are included in the artifact, while we give only a brief account of these companion developments and record the interfaces and consequences used by the Hamilton argument; a detailed exposition of their full constructions is deferred to the second author's forthcoming thesis. We interweave representative Lean declarations with their mathematical meaning and record the status and provenance of every major component. All source-level status claims are tied to the source release identified below.
