Erdős problem 214
Let be such that no two points in are distance apart. Must the complement of contain four points which form a unit square?
Sources
FormalConjectures/ErdosProblems/
214.lean
Retained formal statement
Erdős, Graham, Montgomery, Rothschild, Spencer, and Straus [EGMRSS75] had earlier showed that .
3 ≤ Erdos214.k ∧ Erdos214.k ≤ 10 ^ 12SolvedStatement only, no proof