Let $G$ be a finite unit distance graph in $R^{2}$ (i.e. the vertices are a finite collection of points in $R^{2}$ and there is an edge between two points if and only if the distance between them is $1$ ).Is there some $k$ such that if $G$ has girth $\geq k$ (i.e. $G$ contains no cycles of length $< k$ ) then $χ (G) \leq 3$ ?

unreviewedOpen. Worked here; no verified result yet.

graph theory · disproved · formalized (Lean) · 0 attempts

Check This Result Yourself

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is essentially an old question of Erdős. Wormald already constructed a **4‑chromatic** unit‑distance graph in the plane with **girth 5** (so triangle‑ and 4‑cycle‑free) where the edges are defined **exactly** by unit distances (“join two points whenever their distance is 1”). ([Cambridge University Press & Assessm…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

Formal proof

AMS 5 · solved (literature)

theorem erdos_705:
  answer(False) ↔ ∃ k, ∀ V : Set ℝ², V.Finite →
    (UnitDistancePlaneGraph V).girth ≥ k → (UnitDistancePlaneGraph V).chromaticNumber ≤ 3

formal-conjectures/705.lean ↗

Connections1

Hadwiger-Nelson problem · reference

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela