Prove2Me

Perelman: Poincaré conjecture in dimension 3

Open
SmoothPoincare4.perelman_poincare_dim_three

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

4-manifoldspoincare-conjecturetopology

Let MM be a compact Hausdorff smooth 33-manifold without boundary that is simply connected. Then MM is diffeomorphic to S3S^3.

Preamble
import Mathlib

open scoped Manifold ContDiff
open Metric
Formal statement
namespace SmoothPoincare4

theorem perelman_poincare_dim_three (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] [IsManifold (𝓡 3) ∞ M]
    [SimplyConnectedSpace M] :
    Nonempty (M ≃ₘ^∞⟮𝓡 3, 𝓡 3⟯ sphere (0 : EuclideanSpace ℝ (Fin 4)) 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