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 SRnS \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 SMetric.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

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page