Erdős problem 508 — wave 9o report

Date of live-page check and computation: 2026-07-28 UTC.

Outcome

The classical problem is not solved here: the verified range remains \(5\leq\chi(\mathbb R^2)\leq 7\). The concrete progress is:

1. (d) Computational-only, exact finite case. For the graph

\[ H_{11}=\bigl(\mathbb F_{11}^2, \{uv:(u_1-v_1)^2+(u_2-v_2)^2=1\}\bigr) \] I verified \[ \boxed{\chi(H_{11})=5}. \] The graph has 121 vertices, 726 edges, and degree 12. A displayed 5-colouring is checked edge by edge. A dependency-free exhaustive DSATUR search proves non-4-colourability in 2,565 search nodes.

1. (b) Rigorous modulo Hensel's lemma and the checked DRAT certificate.

Extending Madore's reduction gives \[ \boxed{\chi\!\left(\mathbb Q(\sqrt3,\sqrt5,\sqrt{11})^2\right)=5}. \] In particular, no 6-chromatic unit-distance graph can have an embedding whose coordinates all lie in \(K=\mathbb Q(\sqrt3,\sqrt5,\sqrt{11})\). This is a precise obstruction to extending the de Grey/Heule coordinate-field machinery to a lower bound of 6 without first leaving \(K\).

1. (d) Computational certificate audit. The CNP-SAT repository's

529-vertex data were independently checked in exact multiquadratic arithmetic: the 529 points are distinct and their complete unit-distance graph has exactly 2,670 edges. Its CNF is exactly the expected 4-colouring encoding. The repository contains proof/529-4-sbp.drat but no corresponding 529-4-sbp.cnf; the proof does not verify against the only supplied 529 CNF. It does verify after inserting the three symmetry-breaking unit clauses \(1,6,23\). These clauses fix three colours on vertices \(1,2,6\), which form a triangle, so they are without loss of generality.

The finite-field fact in item 1 was already asserted without proof in a footnote of Madore's 2015 preprint. The contributions here are a small standalone exact verification, its extension to the actual multiquadratic field used by the 529-vertex certificate, and identification/checking of the missing symmetry-breaking input needed to reproduce that certificate.

Step 0: authoritative live page and skip gate

I fetched both the rendered page and its LaTeX-source view through the Bright Data browser, and separately opened the linked discussion thread. Direct HTTP was not used as a substitute.

The exact current statement is:

What is the chromatic number of the plane? That is, what is the smallest number of colours required to colour \(\mathbb{R}^2\) such that no two points of the same colour are distance \(1\) apart?

Live metadata relevant to the mandatory gate:

• status: OPEN;
• claimed proofs: 0;
• “Currently working on this problem”: None;
• “Interested in collaborating”: None;
• last page edit: 22 January 2026;
• one comment.

Thus the task was not skipped. The sole comment, by BorisAlexeev on 27 October 2025, points out that Erdős wrote \(F(2)\leq6\) in [Er75f, p.107], suggests this was almost certainly a typo for \(\leq7\), and asks what follows if it was not a typo. It contains no claimed proof and no current-worker marker.

The page's listed mathematical results are:

• an equilateral triangle gives \(\chi\geq3\);
• the Moser spindle and Golomb graph give \(\chi\geq4\);
• the current classical bounds are \(5\leq\chi\leq7\);
• de Grey gives the lower bound, and a suitably scaled hexagonal tiling gives

the upper bound;

• the page says the fractional chromatic number is at least 4 and at most

\(4.359\ldots\), citing Croft for the latter;

• it cross-references problems 704, 705, 706, and 1070.

Authoritative URLs:

• problem: <https://www.erdosproblems.com/508>
• LaTeX source: <https://www.erdosproblems.com/latex/508>
• sole discussion: <https://www.erdosproblems.com/forum/discuss/508>

Primary-source literature check

I verified that the following papers/preprints exist and say the claims used here.

• Aubrey de Grey, The chromatic number of the plane is at least 5,

arXiv:1804.02385. It constructs a finite unit-distance graph that is not 4-colourable; the smallest graph in that paper has 1,581 vertices.

• David Madore, The Hadwiger-Nelson problem over certain fields,

arXiv:1509.07023. Proposition 4.6 proves \(4\leq\chi(\mathbb Q(\sqrt3,\sqrt{11})^2)\leq5\) by reduction to \(\mathbb F_{11}^2\). Lemma 4.5 displays a 5-colouring of that finite graph; its footnote states, without using or proving it, that the finite chromatic number is exactly 5.

• Marijn Heule, Trimming Graphs Using Clausal Proof Optimization,

arXiv:1907.00929. It reports the 529-vertex, 2,670-edge 5-chromatic graph and points to the CNP-SAT data repository. The paper reports roughly 100,000 CPU-hours for the graph-reduction experiments.

• Jaan Parts, *Graph minimization, focusing on the example of 5-chromatic

unit-distance graphs in the plane*, arXiv:2010.12665. It reports a 509-vertex, 2,442-edge 5-chromatic unit-distance graph. I did not need that larger certificate audit for the field obstruction and did not independently certify its data here.

• Konrad Mundinger, Sebastian Pokutta, Christoph Spiegel, and Max Zimmer,

Extending the Continuum of Six-Colorings, arXiv:2404.05509. Its six-colourings are off-diagonal: five colours avoid unit distance and the sixth avoids another distance \(d\). They are not 6-colourings solving the classical problem.

• Ákos Dúcz and Dániel Varga, *A unit-distance graph in the plane with

independence ratio below \(1/4\)*, arXiv:2606.28157, dated June 2026. This postdates the page's last edit and claims the sharper fractional result \(\chi_f(\mathbb R^2)>4\). It recovers the integer lower bound 5 but does not improve it.

• Georgy Sokolov and Vsevolod Voronov,

On the chromatic number of the plane for map-type colorings, arXiv:2502.01958, proves results under extra regularity/map hypotheses. Those do not determine the unrestricted chromatic number in problem 508.

The searches found no primary source improving the unrestricted integer range \(5\leq\chi(\mathbb R^2)\leq7\). This is an honest search result, not a theorem that no such source exists.

Exact small case: \(\chi(H_{11})=5\)

Index vertices as \((x,y)\), with \(x,y\in\{0,\ldots,10\}\). Two vertices are adjacent precisely when

Direct enumeration gives 121 vertices and 726 edges; every vertex has degree 12.

Here is the verified 5-colouring. Row \(x\), column \(y\), contains the colour of \((x,y)\):

01024323041
13212130214
04321043421
41410324130
24143241043
31034310434
43242103241
30321030314
04210242101
21432301030
12103212102

Its colour-class sizes are \(23,28,23,24,23\). The checker reconstructs all 726 edges and tests every one. The SHA-256 of the table with newline after each row is 42b2c542b71915e1da70bcd342d5997d3312ad1a8356a164d7ed6ed1266df263.

For the lower bound, the vertices

form a triangle: the three squared differences are respectively \(1,45,34\), all congruent to \(1\bmod11\). In any 4-colouring their colours are distinct, so a global permutation lets the search fix them to colours 0, 1, 2.

The recursive checker then:

1. selects an uncoloured vertex of maximum saturation (DSATUR);
2. tries every colour absent from its coloured neighbours;
3. updates neighbour-colour counts exactly;
4. prunes only when an uncoloured vertex has no available colour;
5. returns SAT only after all 121 vertices are coloured.

The ordering heuristics change only branch order. Every legal branch is still visited. The search exhausts 2,565 recursive nodes and returns UNSAT, so \(H_{11}\) is not 4-colourable. Together with the table this proves the finite result. In the requested taxonomy this is (d) computational-only, even though the enumeration is exhaustive and reproducible.

The multiquadratic-field obstruction

Let

Upper bound \(\chi(K^2)\leq5\)

This is Madore's valuation reduction, with the additional generator \(\sqrt5\).

1. Modulo 11,

\[ 5^2=3,\qquad4^2=5. \] The derivatives of \(T^2-3\) at 5 and \(T^2-5\) at 4 are nonzero modulo

1. Hensel's lemma therefore puts compatible square roots of 3 and 5 in

\(\mathbb Q_{11}\), reducing to 5 and 4 respectively.

1. Adjoining \(\sqrt{11}\) gives the totally ramified quadratic extension

\(L=\mathbb Q_{11}(\sqrt{11})\), whose residue field is still \(\mathbb F_{11}\). Hence \(K\) has an 11-adic place with \[ \sqrt3\mapsto5,\qquad \sqrt5\mapsto4,\qquad \sqrt{11}\mapsto0. \] Let \(A\) be its valuation ring in \(K\).

1. Integrality lemma. If \(a^2+b^2=1\) in \(K\), then \(a,b\in A\).

Otherwise let \(m=\min(v(a),v(b))<0\) and divide by a coordinate of valuation \(m\). Reduction gives either \(1=0\), when the other coordinate has larger valuation, or a solution of \(1+z^2=0\) in \(\mathbb F_{11}\), when the valuations tie. Both are impossible: \(-1=10\) is not a square modulo 11.

1. Therefore every unit edge in \(K^2\) stays inside one additive coset of

\(A^2\). Translate each coset to \(A^2\), reduce its two coordinates modulo the maximal ideal, and apply the displayed 5-colouring of \(H_{11}\). Unit edges reduce to edges of \(H_{11}\), so this is a proper 5-colouring. Since \(K\) is countable, representatives can be selected from a fixed enumeration; no unmentioned geometric regularity is being assumed.

Thus \(\chi(K^2)\leq5\). This part is (b) rigorous modulo the named Hensel lemma; the rest of the reduction is elementary.

Matching lower bound from the 529-vertex graph

At CNP-SAT commit bb414955a6ef5f49f7df2b245b1e778aa67c068a, the verifier checks:

• all 529 coordinate expressions exactly in the eight-element basis

\[ 1,\sqrt3,\sqrt5,\sqrt{15},\sqrt{11},\sqrt{33},\sqrt{55},\sqrt{165} \] over \(\mathbb Q\);

• all \(\binom{529}{2}\) pairs in exact rational multiquadratic arithmetic;
• precisely the repository's 2,670 pairs have squared distance 1;
• the points are all distinct;
• the 11,209-clause CNF is exactly: one “at least one of four colours”

clause per vertex and four conflict clauses per edge.

The CNF omits “at most one colour” clauses, but this is equisatisfiable with ordinary colouring: from any satisfying multi-colour assignment choose one true colour at each vertex; edge clauses ensure adjacent choices differ.

The supplied proof has “sbp” in its filename, but the repository has only cnf/529-4.cnf. Hash-pinned drat-trim reports that pairing as not verified. Add

1 0
6 0
23 0

and change the header from 11,209 to 11,212 clauses. Literals 1, 6, and 23 mean vertex 1 has colour 1, vertex 2 has colour 2, and vertex 6 has colour

1. The edge data contain all three edges among vertices 1, 2, and 6, so any

proper 4-colouring can be relabelled to satisfy these units. With these clauses, drat-trim verifies the proof in about 4 seconds and reports that the core uses 0 RAT lemmas.

Finally, reducing all 529 exact coordinates by \(\sqrt3\mapsto5,\sqrt5\mapsto4,\sqrt{11}\mapsto0\) and applying the finite table gives an explicit proper 5-colouring, with class sizes \(108,123,94,97,107\). Hence the checked graph has chromatic number exactly 5 and lies in \(K^2\). This supplies \(\chi(K^2)\geq5\).

Combining both directions gives

The lower direction is (d) computational-only at the raw certificate level and (b) rigorous modulo the hash-pinned DRAT checker when regarded as a machine-checked proof.

Notice that this does not settle Madore's smaller-field interval for \(\mathbb Q(\sqrt3,\sqrt{11})\): the checked 5-chromatic coordinates really contain \(\sqrt5\). The conclusion proved here is for the three-radical field \(K\).

What this isolates, and the remaining wall

By the de Bruijn–Erdős compactness theorem, a proof of \(\chi(\mathbb R^2)\geq6\) can be given by a finite unit-distance graph that is not 5-colourable. The field result isolates a necessary condition:

A 6-chromatic unit-distance graph admits no unit-distance embedding entirely in \(\mathbb Q(\sqrt3,\sqrt5,\sqrt{11})^2\).

Thus adding more vertices, rotations, or SAT minimisation while keeping all coordinates in this field cannot improve the classical lower bound. A lower-bound attack must leave this field (or use a construction not representable inside it) and then prove non-5-colourability. An upper-bound attack must instead construct a genuine 6-colouring of all of \(\mathbb R^2\); the verified off-diagonal six-colourings do not supply that. These are the two exact missing objects.

The computational scale is not a reason to claim impossibility, but it is a real wall. Heule reports roughly 100,000 CPU-hours for the 529-vertex minimisation experiments. At a representative commodity/spot rate of \$0.04–\$0.10 per core-hour, merely reproducing that historical search budget is roughly \$4,000–\$10,000. This is a benchmark, not a credible estimate for finding a 6-chromatic graph; there is no defensible finite cost estimate without a candidate family. I did not run such a search on this machine.

Reproduction

Standalone verifier:

runs/erdos508_wave9o_verify.py

Its dependency-free small-case mode is:

python3 runs/erdos508_wave9o_verify.py --small-only

The full audit downloads four CNP-SAT files and drat-trim.c from commits and SHA-256 digests pinned inside the script, compiles the checker with gcc, performs all exact geometry/CNF checks, audits the failing original pairing, and verifies the corrected certificate:

python3 runs/erdos508_wave9o_verify.py

For an offline checkout and prebuilt checker:

python3 runs/erdos508_wave9o_verify.py \
  --asset-dir /path/to/CNP-SAT \
  --drat-trim /path/to/drat-trim

The final full local run completed in 19.004 seconds, used at most about 67 MB, and printed:

F11 graph: 121 vertices, 726 edges, regular degree 12
F11 5-colouring: valid; class sizes [23, 28, 23, 24, 23]
F11 5-colouring SHA256: 42b2c542b71915e1da70bcd342d5997d3312ad1a8356a164d7ed6ed1266df263
F11 exhaustive 4-colour search: UNSAT; nodes 2565
Residue checks: sqrt(3)=5, sqrt(5)=4, and -1 is nonsquare mod 11
G529 exact geometry: 529 distinct points and exactly 2670 unit pairs
G529 coordinates: in K=Q(sqrt(3),sqrt(5),sqrt(11)); sqrt(5) occurs
G529 CNF: exact 4-colouring encoding, 2116 variables, 11209 clauses
G529 explicit mod-11 5-colouring: valid; class sizes [108, 123, 94, 97, 107]
G529 repository CNF + sbp proof: NOT VERIFIED (expected packaging gap)
G529 CNF + WLOG units 1,6,23 + sbp proof: VERIFIED
ALL REQUESTED CHECKS PASSED in 19.004s

The verifier itself has 615 lines and SHA-256 345b3923b654bc27ce283e3ea7616a1b7c4c604a07903e8ec8c4f72f14972610.

PARTIAL: Verified \(\chi(\mathbb F_{11}^2)=5\) and, modulo Hensel/DRAT checking, \(\chi(\mathbb Q(\sqrt3,\sqrt5,\sqrt{11})^2)=5\); hence no 6-chromatic unit-distance witness can lie in that field, while \(5\leq\chi(\mathbb R^2)\leq7\) remains open.