In my previous post I explained how we know that the chromatic number of the plane is at least 4. If we can construct a unit distance graph (a graph whose edges all have length ) which needs at least colors, than we know the plane also needs at least colors. We were able to construct a unit distance graph that needs at least 4 colors (the Moser spindle), and hence the chromatic number of the plane is at least 4.
It turns out that de Grey’s new proof follows exactly this same pattern: he constructs a unit distance graph which needs at least 5 colors. So why hasn’t anyone else done this before now? The Moser spindle (a unit distance graph with chromatic number 4) has been around since 1961; why did it take almost 60 years for someone to come up with a unit distance graph with chromatic number 5?
The reason is that the graph is very big! de Grey’s graph has 1581 vertices. Although it is itself constructed out of copies of smaller pieces, which are themselves constructed out of pieces, etc.—so it’s not quite as hard to analyze as any random 1581-vertex graph—proving that it requires 5 colors still required a computer. Even the process of finding the graph in the first place required a computer search. So that’s why no one had done it in the last 60 years.
A lot of people have been working on improving and extending this result. The current record-holder for smallest unit-distance graph with chromatic number 5 has 610 vertices, and was found by Marijn Heule using a computer search. Here’s a picture of it, provided by Marijn:
It’s unknown whether we will be able to find a proof that can be constructed and understood by humans without the help of a computer. It’s also unknown whether these techniques and the associated technology will be able to extend far enough to find a unit distance graph with chromatic number 6 (if such a thing exists—though it seems many mathematicians believe it should).