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$?

Erdős problem 705

Start work

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

705.lean

Retained formal statement1 of 1

Let $G$ be a finite unit distance graph in Unparsed notation: \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.

FormalConjectures/ErdosProblems/705.leanErdos705.erdos_7055 linesExact file

1False ↔2  ∃ k,3    ∀ (V : Set (EuclideanSpace ℝ (Fin 2))),4      V.Finite →5        (SimpleGraph.UnitDistancePlaneGraph V).girth ≥ k → (SimpleGraph.UnitDistancePlaneGraph V).chromaticNumber ≤ 3

SolvedStatement only, no proof