Erdős problem 214

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

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

214.lean

Retained formal statement4 of 6

Erdős, Graham, Montgomery, Rothschild, Spencer, and Straus [EGMRSS75] had earlier showed that $3\leq k\leq 10^{12}$ .

FormalConjectures/ErdosProblems/214.leanErdos214.erdos_214.variants.egmrss1 lineExact file

13 ≤ Erdos214.k ∧ Erdos214.k ≤ 10 ^ 12

SolvedStatement only, no proof