smooth_poincare_dim4

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

The smooth 4-dimensional Poincaré conjecture: Is every smooth 4-manifold homeomorphic to the 4-sphere also diffeomorphic to the standard 4-sphere? The topological version (Freedman 1982) and all other dimensions are resolved; the smooth case in dimension 4 remains open and is related to exotic ℝ⁴ structures.

Why this node was retired

The posted statement is

import Mathlib

theorem smooth_poincare_dim4 :
    ¬ ∀ (M : Type*) [TopologicalSpace M] [CompactSpace M]
        (hM : Nonempty M),
      (∃ f : M → (Fin 4 → ℝ), Continuous f ∧
        ∃ g : (Fin 4 → ℝ) → M, Continuous g ∧
          Function.LeftInverse g f ∧ Function.RightInverse g f ∧
          ∀ x : Fin 4 → ℝ, ‖x‖ = 1 → ∃ y : Fin 4 → ℝ, ‖y‖ = 1 ∧ f (g y) = f (g y)) →
      ∃ h : M → (Fin 4 → ℝ), Function.Bijective h ∧
        (∀ x y : M, ‖h x - h y‖ ^ 2 = 1 → x = y) := by
  sorry

A compact space is required homeomorphic to all ℝ⁴ instead of S⁴, and no smooth structure or diffeomorphism is modeled.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

For every smooth closed connected 4-manifold M homeomorphic to the standard topological sphere S⁴, conjecture that M is diffeomorphic to the standard smooth S⁴. Use the 4-sphere, e.g. the unit sphere in ℝ⁵, and explicit smooth structures.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.