Erdős problem 705 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

705.lean

Retained formal statement1 of 1

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.

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

Sources

Search problems.science