# Has there been a computer search for a 5-chromatic unit distance graph?

The existence of a 4-chromatic unit distance graph (e.g., the Moser spindle) establishes a lower bound of 4 for the chromatic number of the plane (see the Nelson-Hadwiger problem).

Obviously, it would be nice to have an example of a 5-chromatic unit distance graph. To the best of my knowledge, the existence of such a graph is open. Has there been any (documented) attempt to find such a graph through a computer search? For instance, has every $n$-vertex possibility been checked up to some $n$?

• An interesting variation, which seems more amenable to computer search, is to look for non-4-colorable almost-unit distance graph. You can indeed ask for the chromatic number $\chi_\epsilon$ of the graph whose vertices are the points of the plane, and an edge joins two vertices if their distance is between $1$ and $1+\varepsilon$. Obviously $\chi_\varepsilon$ decreases when $\varepsilon\to 0$, but the limit is not known. It is not known if the limit is the chromatic number of the plane either. – Benoît Kloeckner Apr 22 '16 at 20:07
• @Benoit Do you have some references for almost-unit distance graphs? – domotorp Oct 12 '17 at 8:26
• @domotorp: no, I don't think it has been actually looked at (I have some lose ideas myself, but nothing written). – Benoît Kloeckner Oct 12 '17 at 14:30
• @Benoit I've just realized that $\chi_\varepsilon\ge 6$, as shown by the following simple argument. Divide the plane into a grid of length $\varepsilon$ and color each small square to the color of its center. If the original coloring avoided distances $1\pm \varepsilon$, then this new coloring will still avoid unit distances. Since each region is nice, at least 6 colors are needed because of this result: sciencedirect.com/science/article/pii/0097316573900204 – domotorp Aug 3 '18 at 7:57

As of this morning there is a paper on the ArXiv claiming to show that there exists a 5-chromatic unit distance graph with $1567$ vertices. The paper is written by non-mathematician Aubrey De Grey (of anti-aging fame), but it appears to be a serious paper. Time will tell if it holds up to scrutiny.

EDIT: in fact, it must be the one with 1585 vertices, according to checkers, see https://dustingmixon.wordpress.com/2018/04/10/the-chromatic-number-of-the-plane-is-at-least-5/

• You have to be kidding me! – Nik Weaver Apr 9 '18 at 18:48
• It is computer checkable if the graph (including vertex locations) is available. I don't think it should be dismissed out of hand, even though the result is quite surprising. – Brendan McKay Apr 10 '18 at 0:19
• The graph is now available in multiple formats (including DIMACS) here: dustingmixon.wordpress.com/2018/04/10/… – Dustin G. Mixon Apr 10 '18 at 14:39
• This is an amazing result! @Juho: It wouldn't hurt to run a different SAT solving program on it, as an independent check. – Timothy Chow Apr 10 '18 at 15:18
• @TimothyChow treengeling finished with UNSAT result as well, as expected (or hoped). I can upload the files later on too if anyone is interested. – Juho Apr 11 '18 at 10:40

It depends how serious you require the search to be. ☺

When writing this note, I made a few attempts at experimenting in this direction, but I quickly came to the conclusion that either I didn't know how to approach the experimental problem, or that it was just too large to be feasible, or both.

I tried to concentrate on a particular set of graphs, namely the minimal $5$-chromatic subgraphs of $(\mathbb{F}_p)^2$ (with an edge between $(x,y)$ and $(x',y')$ iff $(x-x')^2+(y-y')^2=1$) for small $p$, because some of the remarks in the aforementioned note (esp. around prop. 5.3) suggest that this might be a good place to look. But even there, I obviously got nowhere (although I can't say that I tried extremely hard).

It is at least known that there is no 5-chromatic unit distance graph on at most 12 vertices [1, Theorem 4]. I don't know if something similar is known for larger values of $n$.