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).

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

505.lean

Retained formal statement1 of 3

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).

Erdős [Er44] suspected this. Disproved by Kahn–Kalai [KK93] for n≥2015n \geq 2015. Currently known to be false for n≥64n \geq 64. A formal proof was formalised by Boris Alexeev using Aristotle.

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.