Freedman's non-smoothability theorem | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: Unavailable.

Informal solution: Unavailable.

theorem declaration uses `sorry`four_manifold_not_smooth :
    ∃ (M : Type*) (_ : TopologicalSpace M) (_ : T2Space M) (_: CompactSpace M)
      (_ : SimplyConnectedSpace M) (_ : Nonempty (ChartedSpace 𝔼 M)),
      ∀ (_ : ChartedSpace 𝔼 M), ¬ IsManifold (𝓡 4) ∞ M := by⊢ ∃ M x,
  ∃ (_ : T2Space M) (_ : CompactSpace M) (_ : SimplyConnectedSpace M) (_ : Nonempty (ChartedSpace 𝔼 M)),
    ∀ (x_5 : ChartedSpace 𝔼 M), ¬IsManifold (𝓡 4) ∞ M
  sorryAll goals completed! 🐙