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 best known bounds currently are
4 ≤ Erdos214.k ∧ Erdos214.k ≤ 7SolvedStatement only, no proof