erdős #508 · Hadwiger-Nelson problem

← #507 · #509 (packet.json; erdosproblems.com)

What is the chromatic number of the plane? That is, what is the smallest number of colours required to colour such that no two points of the same colour are distance apart?

claimed — no verifier run, no signed judgmentunreviewedOpen. Worked here; no verified result yet.

geometry · open · formalized (Lean) · 0 attempts

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

The exact value is **not known**. This is the **Hadwiger–Nelson problem**: determine the chromatic number of the unit-distance graph on (\mathbb{R}^2).

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

Formal proof

AMS 52 · open (literature)

theorem HadwigerNelsonProblem :
    χ(ℝ²) = answer(sorry)
formal-conjectures/508.lean ↗

Check it yourself

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

vela reproduce examples/erdos-problems

Verify this yourself

Run this command — the output must match these fingerprints.

vela reproduce examples/erdos-problems
  • packet.json · sha256 7b1a960d462f7f2df52808b5f23ef7d7d6e21213e406180c205782e95c2cc589

Search Vela

Search problems, results, contributors, and pages — or jump straight to an id.