Questions, not proof records
Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.
sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.Hilbert–Smith conjecture*: every locally compact topological group acting continuously and faithfully on a connected finite-dimensional topological manifold is a Lie group.
Equivalent p-adic formulation: the p-adic integers ℤ_[p] cannot act continuously and
faithfully on any connected finite-dimensional topological manifold. By the Gleason–Yamabe
theorem, this is equivalent to hilbert_smith_conjecture.
Let D be the diagonal group of SL_n(ℝ) where n ≥ 3.
Then any relatively compact D-orbit in SL_n(ℝ) / SL_n(ℤ) is closed.