A continuum of exotic smooth structures on ℝ⁴

Open

SmoothPoincare4.continuum_exotic_R4

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

4-manifoldspoincare-conjecturetopology

There is a family $(X_t)_{t \in \mathbb{R}}$ of smooth $4$ -manifolds, each homeomorphic to $\mathbb{R}^4$ , such that $X_s$ and $X_t$ are not diffeomorphic whenever $s \ne t$ .

Preamble

import Mathlib

open scoped Manifold ContDiff
open Metric

Formal statement

namespace SmoothPoincare4

theorem continuum_exotic_R4 :
    ∃ (X : ℝ → Type) (_ : ∀ t, TopologicalSpace (X t))
      (_ : ∀ t, ChartedSpace (EuclideanSpace ℝ (Fin 4)) (X t))
      (_ : ∀ t, IsManifold (𝓡 4) ∞ (X t)),
      (∀ t, Nonempty (X t ≃ₜ EuclideanSpace ℝ (Fin 4))) ∧
      ∀ s t, s ≠ t → IsEmpty (X s ≃ₘ^∞⟮𝓡 4, 𝓡 4⟯ X t) := 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