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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/705.lean

Formal Conjectures

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

Reported activity

Reported by these sources. Not reviewed here.

Subtle errors
GPT-Erdős
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry