As a follow-up to my previous post, I wanted to discuss an overview of de Grey’s proof that the chromatic number of the plane is at least 5, as well as some recent progress that has been made on the polymath proposal page and elsewhere.
The core idea of de Grey’s proof is to select a finite point set H in the plane and a coloring property P, and then demonstrate two incongruous statements:
(a) For every proper k-coloring of the plane, there exists a copy of H whose inherited coloring satisfies P.
(b) For every proper k-coloring of the plane, every copy of H inherits a coloring that doesn’t satisfy P.
Indeed, if both statements hold, then there is no proper k-coloring of the plane. To prove (a) and (b), we pass to finite unit-distance graphs in the plane. Explicitly, to prove (a), one finds a finite point set L such that for every proper k-coloring of L, there exists a copy of H in L whose inherited coloring satisfies P. Similarly, to prove (b), one finds a finite superset M of H such that every proper k-coloring of M forces the inherited coloring of H to not satisfy P.
For example, for k=3, we may take H to be two points of distance , and let P be the property that the vertices receive different colors. Then letting L be the vertices of a – – triangle, we see that for every proper 3-coloring of L, the two vertices of unit distance must receive different colors, and so one of these must have a different color from the third vertex that’s away. This copy of H necessarily satisfies P. Next, let M be the diamond graph of four vertices forming two equilateral triangles of unit side length. Here, the end points have distance , forming H, and any 3-coloring of M will force the points in H to have the same color, i.e., H’s inherited coloring fails to satisfy P.
Given L and M, one may produce a finite unit-distance graph that is not k-colorable. Indeed, extend each copy of H in L to a copy of M. Performing this operation to the L and M described above produces the Moser spindle.
To tackle k=4, de Grey takes H to be the 7 points in the hexagonal lattice of norm at most 1. Observe that the 6 points of norm 1 can be decomposed as the vertices of two triangles of side length . He takes P to be the property that one of these triples receives the same color. To prove (a), he constructs L by overlaying portions of 4 copies of the hexagonal lattice, resulting in a graph of 121 vertices. With this choice of L, the proof of (a) does not require computer assistance, though a computer makes the proof less mundane. To prove (b), he constructs M by aligning several copies of the Moser spindle, resulting in 1345-vertices. For this choice of M, the proof of (b) requires computer assistance.
As in the 3-colorable case, one may combine these graphs to produce a finite unit-distance graph that is not 4-colorable. In de Grey’s paper, the resulting graph N has 20425 vertices (presumably, there are many duplicated vertices here, considering L contains 52 copies of H, each of which are extended to a copy of M, i.e., 121+52*1345 = 70061 vertices with double-counting). de Grey then proceeds to “shrink” N by removing unnecessary vertices, or replacing point subsets with smaller ones that still preclude 4-colorability. These moves are necessarily computer assisted. The result is a 1581-vertex graph that can be independently verified as not 4-colorable with the help of a SAT solver (in fact, this point set is a superset of the 1577 points identified in the second update here).
Given this breakthrough, it is natural to wonder whether the techniques can be extended to prove that the plane is not 5-colorable. Considering the Moser spindle was a fundamental gadget in de Grey’s proof, it seems like an appropriate first step to hunt for the smallest 5-chromatic unit-distance graph (or even a 5-chromatic unit-distance graph whose lack of 4-colorability is more easily verified). de Grey has proposed a polymath project to this effect.
The last few days have seen a bit of activity in various directions along these lines, which I’ll summarize below:
- We found a modification to L that has 97 vertices and 40 copies of H. (The proof of (a) with this new L still doesn’t require a computer.) Aubrey de Grey has observed additional symmetries in this modification, suggesting that further reductions might be made.
- Tamás Hubai identified various simplifications that can be made to M. He also pointed out that we could let H be the vertices of an equilateral triangle of side length (which looks like a natural generalization of the k=3 proof above), though it would require more copies of M in the pre-shrunk graph N.
- Marijn Heule recast whether M forces H to not satisfy P as a SAT problem, and can apply DRAT-trim to produce a proof of unsatisfiability. The vertices that are inconsequential to this proof are removable. Randomly permuting clauses produces a different proof, suggesting a randomized approach to iteratively remove vertices. Apparently, this shrinks M considerably, but the final result is yet to come
On the side, I have been discussing with collaborators about other methods of simplification, which I summarize below:
- It would be nice if one could prove that a given graph is not 4-colorable by producing a Lovasz certificate, that is, a weighting of the vertices and a weighting of the edges such that the resulting weighted adjacency matrix with vertex weights on the diagonal is positive semidefinite with unit trace. If the sum of these matrix entries is larger than 4, then this would certify that the graph is not 4-colorable. Soledad Villar coded up a projected gradient descent solver to hunt for such a certificate (exploiting the sparsity of the weighted adjacency matrix), and so far, she reports the sum of the entries as 3.9. Time will tell if this approach brings fruit, but Fernando de Oliveira Filho points out that this will do no better than the Lovasz number of the entire plane’s unit-distance graph. Does this produce a new lower bound on the Lovasz number and fractional chromatic number of the plane?
- At the moment, it seems that the fundamental barrier to simplifying N is the construction of M that proves (b). It seems that de Grey’s approach in his paper was to start with H, then L, then M. As an alternative, one might consider searching through candidates for M to identify how subsets of points are forced to be colored, and then use that information to inform the choice of H and L. Boris Alexeev has indicated to me that this approach should be amenable to computer search.