hilbert_smith_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result hilbert_smith_conjecture is named for, so its Disproved status carries no information about it. Do not import it or use it as a dependency.

Hilbert-Smith conjecture: A locally compact group acting effectively on a topological 3-manifold must be a Lie group. Proved for Lipschitz actions (Pardon 2013); open for continuous actions.

Why this node was retired

The posted statement is

import Mathlib

theorem hilbert_smith_conjecture (M : Type*) [TopologicalSpace M]
    (hM : ∀ p : M, ∃ U : Set M, IsOpen U ∧ p ∈ U ∧
      ∃ _ : U ≃ₜ (EuclideanSpace ℝ (Fin 3)), True)
    (G : Type*) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (act : G → M → M)
    (hcont : Continuous (fun p : G × M => act p.1 p.2))
    (heff : ∀ g : G, (∀ x : M, act g x = x) → g = 1) :
    ∃ _ : G ≃ₜ (EuclideanSpace ℝ (Fin 0)), True := by
  sorry

The conclusion is ∃ _ : G ≃ₜ EuclideanSpace ℝ (Fin 0), True, i.e. that the acting group G is homeomorphic to a point. That is far stronger than the conjecture, which asserts that a locally compact group acting effectively on a manifold is a Lie group, and it is false for G = ℝ acting on ℝ³ — hence the Disproved status, which says nothing about the conjecture.

What a faithful statement would require

The hypotheses must include local compactness of G, and the conclusion must assert that G is a Lie group, not that it is trivial.

No corrected replacement node exists yet.