Erdős Problem 705

Reference: erdosproblems.com/705

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

Let G be a finite unit distance graph in R². Is there some k such that if G has girth ≥ k, then χ(G) ≤ 3?