One of the coolest open problems in math is the chromatic number of the plane (CNP), that is, the Hadwiger–Nelson problem. Considering it has a unit-distance embedding in the plane, the Moser spindle ensures that CNP is at least 4. Furthermore, one may tile the plane with hexagons of the appropriate size and then color those tiles with 7 colors to prove that CNP is at most 7. Yesterday, Aubrey de Grey posted a paper on the arXiv that proves that CNP is at least 5 (see also announcements from Gil Kalai, Jordan Ellenberg and Terry Tao). As one might expect, the graphs in his proof feature an amalgam of spindle-type structures. de Grey describes a unit distance graph of 20,425 vertices that is not 4-colorable, and then he describes how to find smaller graphs with this property. He concludes with a description of a graph with 1567 vertices. He has since proposed a polymath project to decrease this number even further.

Last night, I worked with Boris Alexeev to get a handle on de Grey’s final graph construction. He describes two collections of vertices and . Here, is a subset of , but for simplicity, we will take to be all of , which we will denote . This set is described as the orbit of 39 points under the action of the group generated by rotation by 60 degrees and reflection about the -axis (warning: the 5th point in de Grey’s writeup has a parenthesis mismatch). The resulting set has size 397 (there are duplicates to remove). Now we take two copies of (one is actually and the other is ), except we rotate the second copy by . This will produce an edge between and its rotated version (it will also produce 5 additional edges due to the rotational symmetry of ). The resulting set of points has size 793 (only the origin was double-counted). Now we shift all of these points to the right by to produce a set we’ll call . Take a second copy of and rotate by . This introduces an edge between and its rotated version (this corresponds to the edge between B and C in Figure 5 of de Grey’s paper). The resulting set of points has size 1585 (again, only the origin was double-counted). Note that this is 18 vertices more than reported by de Grey because our two copies of each have 9 additional vertices for simplicity.

For the sake of reproducibility, the following files might be useful:

- The 1585-vertex graph described above in DIMACS format
- A naive translation of 4-colorability of this graph into a SAT problem in DIMACS format
- The vertices of this graph in explicit Sage notation

Boris started running the above SAT instance last night using a few of popular SAT solvers, and the first to return UNSATISFIABLE was Glucose 4.0 (which is based on MiniSat), after 5.5 total hours on 16 cores (i.e., an m4.4xlarge instance on Amazon EC2), amounting to 20 minutes of clock time. It also takes less than a second to 5-color this graph.

I would be interested to find alternative certificates of this theorem. The Lovász number of a graph’s complement is famously sandwiched between the clique number and the chromatic number of the original graph. A short MATLAB script (running CVX) demonstrates that the Lovász number of the Moser spindle‘s complement is , forcing the chromatic number (integer) to be at least 4. (**EDIT:** My original MATLAB script neglected to take the graph complement.) In general, semidefinite programs are slow for large problem instances, but Lovász might be faster than SAT solvers in this setting. Furthermore, to certify that the 1585-vertex graph above is not 4-colorable, it suffices to find a dual-feasible point with value strictly larger than 4. Perhaps finding such a point is a reasonable pursuit. (This is not unlike the pursuit of fast certificates here and here.)

**UPDATE:** Aubrey suggested that we consider what happens when we remove the remaining 18 vertices. This amounts to removing 9 vertices from two of the copies of in the above construction. Instead, we performed a more conservative test by only removing 9 vertices from one of the copies of . However, we found that doing so resulted in a graph that is 4-colorable (and in fact, the coloring is identified in just a few seconds). Just to be sure, we also tried removing rotated versions of these 9 vertices in case our interpretation of was different from Aubrey’s intended construction, but every choice we made produced a graph that is (quickly) 4-colorable. As such, we cannot verify the 1567-vertex construction (or even a 1576-vertex construction). Regardless, Aubrey’s main result is apparently valid with the 1585-vertex construction described above.

**UPDATE:** After the previous update, we wondered which vertices could be removed from the 1585-vertex graph without the graph becoming 4-colorable. After an exhaustive search, we found that exactly 8 vertices are individually removable, namely, the vertices indexed by 3, 4, 23, 24, 948, 949, 952, and 953 in our files. Furthermore, we found that removing all 8 of these vertices produces a 1577-vertex graph that is also not 4-colorable. As such, this graph appears to be the unique minimal 5-chromatic induced subgraph of the 1585-vertex graph above. Therefore, for the proposed polymath project, the pursuit of a smaller unit-distance graph with chromatic number at least 5 will necessarily require a different approach than hunting for subgraphs of this graph.

**UPDATE:** To avoid any possibility of confusion, I wanted to point out that of the files I linked to above, our methodology first generated the file that contains exact coordinates of the vertices. (We derived this from an interpretation of Aubrey’s construction, extrapolating from the explicit coordinates that he lists at the end of his paper.) Next, we identified likely edges by numerical approximation. Finally, we used exact arithmetic to check that each of these likely edges honestly corresponds to unit distance. This last step took about an hour of running Sage on a standard laptop.

Thanks Dustin and Boris! I have just received a report that the 1567-vertex graph is 4-colorable; could you please check it?

Update: the smallest case may need to be revised up to 1585 vertices. Many thanks to Brendan McKay and Gordon Royle for letting me know overnight that they had successfully 4-coloured my 1567er; as a result I found a bug in the part of my code that implements the relaxation described in section 5.4 and now it agrees. Mercifully this only means, in the worst case, that fewer than nine vertices can be removed from S to make Sa; the worst case is that we could remove none, which leaves the full graph with 1585 vertices that Dustin Mixon and Boris Alexeev have confirmed the non-4-colorability of (as they report above).

It will probably take me the rest of the day to determine how many vertices I can in fact remove from S to make Sa; I will post here when I have an answer.

Update: after fixing my bug and re-running the code that seeks deletions from Sa, I now find that just two vertices can be deleted wtthout introducing a problematic (as defined in section 5.4) 4-coloring. This therefore leads to a size of 1581 for the full 5-chromatic graph (which contains two copies of Sa). I have just uploaded to the arxiv a revision of my paper (I gather it will go live within a few hours), incorporating this correction as well as making the construction clearer in section 6 (and adding a number of particularly apposite acknowledgements!). Whew! I will now post this update to the slew of other blogs I know of where the topic is being discussed, and I’ll also fix Wikipedia’s page on the H-N problem (I didn’t make the initial edit that reported 1567, but I think speed is of the essence for that).

I also see that Geoffrey Exoo has now verified my graph M:

https://gilkalai.wordpress.com/2018/04/10/aubrey-de-grey-the-chromatic-number-of-the-plane-is-at-least-5/#comment-40108

and there is another confirmation of the 1585er noted here:

https://mathoverflow.net/questions/236392/has-there-been-a-computer-search-for-a-5-chromatic-unit-distance-graph#297407

Hi guys! Thank you for making the graph easily available!

I was curious about the independence ratio (= independence number / no. of vertices) of this graph, as it would provide an upper bound for the density of a set of points avoiding distance 1. As it turns out, the independence ratio is >= 0.3 (bound found by Gurobi in a few minutes), which is quite bad compared to the Moser spindle.

One nice project would be to find graphs with small independence ratio, instead of graphs with large chromatic number.

BTW, it would also be interesting to know the fractional chromatic number of this graph.

> it would also be interesting to know the fractional chromatic number of this graph

I totally agree. In particular, I would love it if the fractional chromatic number were larger than 4, and easily certified as such. Along these lines, I’m working with Soledad Villar to estimate the Lovász number of the graph complement.

I think the theta number of the complement won’t be so interesting… It cannot beat the theta number of the whole unit-distance graph (see 4.6f in my thesis http://dutiosb.twi.tudelft.nl/~fmario/thesis.pdf), which for R^2 is quite weak. The fractional chromatic number is another thing entirely.

@Fernando: Do you have an estimate of the theta number for the whole unit-distance graph?

@Dustin: The theta number of the complement of the unit-distance graph should be 3.482872798… (the inverse of 0.2871193; check out table 4.2, p. 74 in my thesis). I think Evan de Corte had an approach using branch-and-bound and the theta number to compute better bounds for the fractional chromatic number of some graphs (I think this is not written down).

Hi Dustin,

Speaking of the fractional number of the plane, as far as I know the current record is 383/102= 3.7549…

It is achieved by a unit-distance graph of order 73. See the reference below.

Exoo, Geoffrey; Ismailescu, Dan A unit distance graph in the plane with fractional chromatic number 383/102. Geombinatorics 26 (2017), no. 3, 122–127.

Hi Fernando and Dustin,

The point with approx objective value 3.9 that I found may not be exactly feasible (smallest eigenvalue -1e-6). I am working on estimating the Lovasz number for this specific graphs more precisely.

I agree about the fractional CN. One of the people who verified my construction was Landon Rabern, who I believe holds (with his coauthor Dan Cranston) the current record for the lower bound on the fractional CN of the plane, namely 76/21≈3.6190 :

https://arxiv.org/abs/1501.01647

I encourage anyone interested in this to visit the page where we are discussing a Polymath project to simplify my construction as a way of (among other things) gaining insights into related questions, of which this is certainly an important one. It’s here:

https://wordpress.com/read/blogs/8741421/posts/1139

The discharging method in that paper actually allows us to get 105/29 = 3.6207 which we mention at the end, the details for the slightly worse bound were significantly simpler, so we went with that for readability. The value 105/29 hits a natural barrier to the method, so some new idea is needed for improvement. I’ve been able to get a small improvement using a variant of your construction, but it is way too complicated to even bother writing down. It is plausible that there is a simpler way, there are tons of variations to try. It would be great to push the lower bound over 4.

Oliveira Filho (who just commented above) and Vallentin proved that if we look at the measurable fractional chromatic number of the plane, so fractional colorings where only Lebesgue measurable sets get non-zero weight, the lower bound can be improved to 3.725. If we don’t accept the axiom of choice, there are extensions of ZF (e. g Solovay’s model) where everything is Lebesgue measurable. There is an interesting metaquestion: Do the fractional chromatic number of the plane and the measurable fractional chromatic number of the plane differ assuming ZFC?

Many thanks Landon (and apologies for overlooking 105/29). The ZFC issue is also being discussed at Scott Aaronson’s blog:

https://www.scottaaronson.com/blog/?p=3697

I also used SAT solvers to verify graphs from Aubrey’s paper. The property of graph M is verified by glucose in less than 0.5 sec on my notebook. I didn’t hope that SAT solvers will be able to handle the large graph with 20425 vertices, but glucose solved it in ~200sec on my notebook.

Smaller problem is not necessarily a simpler problem. It happens with SAT…

The files can be found here:

https://drive.google.com/open?id=1bWXkqQJyLyxF4Q4eO7YB9aBMN-4pN43S

Would you be able to give us a format importable by Mathematica, like g6, or maybe just the entire adjacency list and vertex coordinates in textfiles?