Erdős problem 214 · problems.science

Let $S\subset \mathbb{R}^2$ be such that no two points in $S$ are distance $1$ apart. Must the complement of $S$ contain four points which form a unit square?

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

214.lean

Retained formal statement1 of 6

Let $S\subset \mathbb{R}^2$ be such that no two points in $S$ are distance $1$ apart. Must the complement of $S$ contain four points which form a unit square?

The answer is yes, proved by Juhász [Ju79], who proved more generally that the complement of $S$ must contain a congruent copy of any set of four points.

FormalConjectures/ErdosProblems/214.leanErdos214.erdos_2143 linesExact file

1True ↔2  ∀ (S : Set (EuclideanSpace ℝ (Fin 2))),3    Erdos214.UnitDistanceAvoiding S → ∃ p, (∀ (i : Fin 4), p i ∈ Sᶜ) ∧ Congruent p Erdos214.unitSquare

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.

Sources

Search problems.science