Hadwiger–Nelson Problem
Colour every point of the plane so no two points exactly one inch apart match. How many colours do you need?
In plain terms
Imagine painting every single point of an infinite sheet of paper. The only rule: any two points exactly one inch apart must be different colours. How few colours can you get away with?
Seven is enough — tile the plane with hexagons slightly under an inch across and repeat seven colours in a pattern. Four is not enough, which you can see from a small arrangement of seven points called the Moser spindle. So the answer is 4, 5, 6 or 7, and for sixty-eight years nobody could narrow it.
Then in 2018 an amateur — Aubrey de Grey, better known for research on ageing — found an arrangement of 1581 points that cannot be coloured with four. The answer is now known to be 5, 6 or 7. Which one is still anybody's guess.
What is known
The problem is secretly finite. A compactness theorem says the whole infinite plane needs k colours exactly when some finite set of points does. So progress comes from building finite point sets — "unit-distance graphs" — that resist colouring, and every one of them is an object you can hand to a computer and check.
That is what happened after 2018. Polymath16, an open online collaboration, spent three years shrinking de Grey's 1581-point graph. The record is now 509 points, found by Jaan Parts. Every step was a concrete object anyone could verify independently.
Nobody has found a point set that forces six colours, and nobody has found a colouring of the plane using fewer than seven.
Why it is hard
The two ends of the problem resist for opposite reasons. Pushing the lower bound to 6 means finding a finite graph that is 6-chromatic — but the search space is the set of all finite point configurations in the plane, which is not something you can enumerate. Pushing the upper bound below 7 means inventing a genuinely new colouring of the whole plane, and the hexagonal one has stood since the 1950s.
There is also a subtlety that makes the problem stranger than it looks: for some ways of asking the question, the answer depends on which axioms of set theory you adopt. Restricting to "reasonable" colourings — ones whose colour classes are measurable — provably needs more colours than the general case might.
What a breakthrough would mean
This is the most visual problem in this library, and the one where an amateur most recently moved a famous constant — which is itself the interesting part. De Grey's graph was found by computer search guided by human insight about which structures to spindle together, and then verified by SAT solvers. The whole episode is a case study in what computer-assisted mathematics currently looks like: a human picks the shape of the search, a machine settles it, and independent machines re-check the answer.
Settling χ = 5 versus 6 versus 7 would not obviously cascade into other fields the way a proof about primes might. Its value is different: it is one of the cleanest test cases for whether machine search can push a genuinely open geometric question, which is exactly the question this lab exists to gather evidence about.
What this lab tried
Standing: Refuted One blind attempt, which closed its own route by proving it. The ring generated by the triangular lattice and the spindle rotation, Z[zeta][rho], is exactly 4-chromatic via an explicit colouring, so no construction inside it -- more copies, more centres, deeper ladder levels, bigger Cayley balls -- can reach five colours. Do not re-attempt anything inside that ring. The open arena the attempt identifies is the mixed groups containing rho_4; read attempt 001's obstruction section and Lead 1 before proposing any rotation-based construction.
Every approach below is recorded in full, including the ones that failed and why. Attempt titles link to the complete record.
Attempt 001blindVerified
Proved that the entire ring generated by the triangular lattice and the Moser spindle rotation is exactly 4-chromatic, by an explicit colouring, so no construction inside it can ever witness five colours -- which retro-explains a census, four kinds of search and Cayley balls to 10315 vertices that all returned 4.
- Range checked
- The colouring rule is proved for the whole ring and checked at ladder levels 0-8 (all 24k+18 unit vectors per level) and on real balls up to 10315 vertices and 77016 edges with zero monochromatic edges. Census: all 30 Eisenstein norms n <= 79 at patch norm 79. Interface bound cross-checked on 112 (n, patch) pairs. Capping sweep: 39 rotation groups. Largest certified graph in the earlier phase 751 vertices and 3796 edges. Nothing bears on chi(R^2) beyond the classical 4; the ring is one countable point set, not the plane.
- Open gaps
- The mixed groups containing rho_4, above all E + rho_3 E + rho_4 E, admit no mod-2 capping functional and were not settled: neither a capping quotient nor a non-4-colourable ball was found. That is the one arena this attempt leaves open.
- The census rule 'chi = 4 iff 3 | n' is a correlation over 30 values of n plus an algebraic characterisation of the split, with no proof connecting them.
- The capping sweep covers one- and two-rotation groups with n <= 21 only, and the conjecture that failures are exactly the groups containing a rotation of even denominator is untested beyond that.
- The constructible closure under circle intersections is strictly larger than the ring -- halving is exactly what the mod-2 colouring cannot survive -- and was not computed, for want of a square-root routine in multiquadratic fields.
- Methodological lesson
- Eight of nine push rounds were searches; every one returned '4-colourable' without saying why, and the ninth was a five-line algebraic check that settled all of them at once and would have done so before any search was run. When a search family keeps returning the same answer, look for the invariant that forces it rather than for a bigger instance. Separately, the two-implementation rule caught two silent errors that produced entirely plausible numbers: a wrong common denominator in field addition, and an inclusion-exclusion identity mislabelled as a colouring count.
- Design note
- harness/hadwiger-nelson holds only what PROBLEM.md asks of it -- exact field arithmetic, the two-sided certifier, and the colouring checkers, now including a scaling solver -- while the lattice, ring and rotation constructors sit in explore/, because they encode this route and would steer a blind agent.
Go deeper
Problem statement and published background · Full prior-art notes · Machine-readable index
Found something, or think we got it wrong?
Both are welcome, and the second especially. Nothing here has been peer-reviewed by a human mathematician, so errors are expected rather than embarrassing — one record in this library was already corrected by a later review.
Challenge something on this page · Report an attempt you ran · Browse open issues
scripts/blind.sh hadwiger-nelson ../workMore on blind and informed mode.