/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilThe Bing-Borsuk Conjecture
The Bing-Borsuk conjecture states that every $n$-dimensional homogeneous absolute neighborhood retract is a topological $n$-manifold.
The conjecture has been verified in dimensions $1$ and $2$ but remains open in higher dimensions. A notable consequence is that if the $3$-dimensional case is true, it implies the Poincaré conjecture.
[HR2008] Halverson, Denise M., and Dušan Repovš. "The Bing-Borsuk and the Busemann conjectures." Mathematical Communications 13.2 (2008): 163-184. https://arxiv.org/abs/0811.0886
namespace BingBorsuk
open scoped Manifoldopen TopologicalSpace
The Bing-Borsuk Conjecture: every $n$-dimensional homogeneous absolute neighborhood retract
is a topological $n$-manifold. A topological space $X$ is an $n$-dimensional manifold
when T2Space X ∧ Nonempty (ChartedSpace (Fin n → ℝ) X). The hypothesis [MetrizableSpace X]
implies T2Space X so this does not appear in the conclusion.
@[category research open, AMS 54 57]
theorem bing_borsuk_conjecture : ∀ n : ℕ, ∀ (X : Type) [TopologicalSpace X] [MetrizableSpace X] [HomogeneousSpace X] [IsAbsoluteNeighborhoodRetract X],
HasLebesgueCoveringDimensionEq X n → Nonempty (ChartedSpace (Fin n → ℝ) X) := ⊢ ∀ (n : ℕ) (X : Type) [inst : TopologicalSpace X] [MetrizableSpace X] [HomogeneousSpace X]
[IsAbsoluteNeighborhoodRetract X], HasLebesgueCoveringDimensionEq X n → Nonempty (ChartedSpace (Fin n → ℝ) X)
All goals completed! 🐙
end BingBorsuk