Vela

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?

Worked, still open.

geometry · open · formalized (Lean) · 0 attempts

use this record

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

AMS 52 · open (literature)

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

status

open

notary

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

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.