Skip to content

Erdős problem 505

Erdős Problem 505 (disproved). Borsuk's conjecture is false for sufficiently large nn: there exists a dimension nn and a bounded set S⊆RnS \subseteq \mathbb{R}^n with positive diameter such that SS cannot be covered by n+1n + 1 subsets each of diameter strictly less than diam⁡(S)\operatorname{diam}(S).

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/505.lean

Formal Conjectures

FormalConjectures/ErdosProblems/505.leanErdos505.erdos_5054 linesExact file
∃ n S,  Bornology.IsBounded S ∧    0 < Metric.diam S ∧      ∀ (F : Fin (n + 1) → Set (EuclideanSpace ℝ (Fin n))), S ⊆ ⋃ i, F i → ∃ i, Metric.diam S ≤ Metric.diam (F i)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:505
  • PLBY Lean proofsErdosProblems.Erdos505

Reported activity

Reported by these sources. Not reviewed here.

Continue