Erdős Problem 705

References:

• erdosproblems.com/705
• [OD99] P. O'Donnell, High girth unit-distance graphs. PhD Dissertation, Rutgers University (1999).

theorem Erdos705.erdos_705 : False ↔ ∃ (k : ℕ), ∀ (V : Set (EuclideanSpace ℝ (Fin 2))), V.Finite → (SimpleGraph.UnitDistancePlaneGraph V).girth ≥ k → (SimpleGraph.UnitDistancePlaneGraph V).chromaticNumber ≤ 3

Let $G$ be a finite unit distance graph in $\mamthbb{R}^2$. Is there some $k$ such that if $G$ has girth $≥ k$, then $\chi(G) ≤ 3$?

The general case was solved by O'Donnell [OD99], who constructed finite unit distance graphs with chromatic number $4$ and arbitrarily large girth.