Poincaré conjecture

TheoremSmooth Poincaré conjecture in dimension 3#●ready to prove

Let \(M\) be a nonempty, compact, simply connected Hausdorff space with a smooth (\(C^\infty\)) manifold structure modelled on \(\mathbb{R}^3\), without boundary. Then \(M\) is \(C^\infty\)-diffeomorphic to the unit sphere \(S^3 = \{x \in \mathbb{R}^4 : \|x\| = 1\}\) with its standard smooth structure.

public theorem_wanted poincare_3d_smooth
    {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] [IsManifold (𝓡 3) ∞ M]
    [SimplyConnectedSpace M] [CompactSpace M] [Nonempty M] :
    Nonempty (M ≃ₘ⟮𝓡 3, 𝓡 3⟯ sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)

Sources

• G. Perelman, three arXiv preprints 2002-2003 (math/0211159, math/0303109, math/0307245). In dim 3, Smooth ⇔ PL ⇔ Topological via Moise (1952) / Bing (1959). Problem poincare_3d_smooth of the lean-eval benchmark.

TheoremTopological Poincaré conjecture in dimension 3#●ready to prove

Let \(M\) be a nonempty, compact, simply connected Hausdorff space with an atlas of charts to \(\mathbb{R}^3\), that is, a topological 3-manifold without boundary. Then \(M\) is homeomorphic to the unit sphere \(S^3 = \{x \in \mathbb{R}^4 : \|x\| = 1\}\).

public theorem_wanted poincare_3d_topological
    {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
    [SimplyConnectedSpace M] [CompactSpace M] [Nonempty M] :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)

Sources

• G. Perelman, The entropy formula for the Ricci flow and its geometric applications (arXiv:math/0211159, 2002); Ricci flow with surgery on three-manifolds (arXiv:math/0303109, 2003); Finite extinction time for the solutions to the Ricci flow on certain three-manifolds (arXiv:math/0307245, 2003). Originally conjectured by Henri Poincaré in 1904. Problem poincare_3d_topological of the lean-eval benchmark.

TheoremTopological Poincaré conjecture in dimension 4#●ready to prove

Let \(M\) be a Hausdorff space with an atlas of charts to \(\mathbb{R}^4\) (a topological 4-manifold without boundary, not assumed second countable). If \(M\) is homotopy equivalent to the unit sphere \(S^4 = \{x \in \mathbb{R}^5 : \|x\| = 1\}\), then \(M\) is homeomorphic to \(S^4\).

public theorem_wanted poincare_4d_topological
    {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M]
    (_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1)

Sources

• M. H. Freedman, The topology of four-dimensional manifolds, J. Differential Geom. 17 (1982), 357-453. Problem poincare_4d_topological of the lean-eval benchmark.

TheoremTopological Poincaré conjecture in dimensions at least 5#●ready to prove

Let \(n \ge 5\) and let \(M\) be a Hausdorff space with an atlas of charts to \(\mathbb{R}^n\) (a topological \(n\)-manifold without boundary, not assumed second countable). If \(M\) is homotopy equivalent to the unit sphere \(S^n = \{x \in \mathbb{R}^{n+1} : \|x\| = 1\}\), then \(M\) is homeomorphic to \(S^n\).

public theorem_wanted poincare_high_dim_topological
    {n : ℕ} (_h5 : 5 ≤ n)
    {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M]
    (_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)

Sources

• S. Smale, Generalized Poincaré's conjecture in dimensions greater than four, Ann. of Math. 74 (1961), 391-406. Topological case: M. H. A. Newman, The engulfing theorem for topological manifolds, Ann. of Math. 84 (1966) and E. H. Connell, A topological h-cobordism theorem for n ≥ 5, Illinois J. Math. 11 (1967). Problem poincare_high_dim_topological of the lean-eval benchmark.

4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.