The chromatic number of the plane is at least 5

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.