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
Juhász [Ju79] also improved the upper bound to .
¬Erdos214.HasRedCopies 12SolvedStatement only, no proof