Milnor: an exotic 7-sphere exists

Open

SmoothPoincare4.milnor_exotic_seven_sphere

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

4-manifoldspoincare-conjecturetopology

There is a smooth $7$ -manifold $M$ that is homeomorphic to $S^7$ but not diffeomorphic to $S^7$ .

Preamble

import Mathlib

open scoped Manifold ContDiff
open Metric

Formal statement

namespace SmoothPoincare4

theorem milnor_exotic_seven_sphere :
    ∃ (M : Type) (_ : TopologicalSpace M) (_ : ChartedSpace (EuclideanSpace ℝ (Fin 7)) M)
      (_ : IsManifold (𝓡 7) ∞ M),
      Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 8)) 1) ∧
      IsEmpty (M ≃ₘ^∞⟮𝓡 7, 𝓡 7⟯ sphere (0 : EuclideanSpace ℝ (Fin 8)) 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