Smale: Poincaré conjecture in dimensions ≥ 5

Open

SmoothPoincare4.smale_poincare_high_dim

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

4-manifoldspoincare-conjecturetopology

Let $n \ge 5$ and let $M$ be a compact Hausdorff smooth $n$ -manifold without boundary. If $M$ is homotopy equivalent to $S^n$ , then $M$ is homeomorphic to $S^n$ .

Preamble

import Mathlib

open scoped Manifold ContDiff
open Metric

Formal statement

namespace SmoothPoincare4

theorem smale_poincare_high_dim (n : ℕ) (hn : 5 ≤ n) (M : Type) [TopologicalSpace M] [T2Space M]
    [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
    (h : Nonempty (ContinuousMap.HomotopyEquiv M (sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))) :
    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) := by sorry

end SmoothPoincare4

Source

Open Problem Garden, 'Smooth 4-dimensional Poincare conjecture' (posted by rybu, 2009), http://www.openproblemgarden.org/op/smooth_4_dimensional_poincare_conjecture

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph