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
The answer is yes, proved by Juhász [Ju79], who proved more generally that the complement of must contain a congruent copy of any set of four points.
Erdos214.HasRedCopies 4SolvedStatement only, no proof