That is: any coloring of the plane with four colors has two points at distance 1 from each other. So says a paper just posted by Aubrey de Grey.
The idea: given a set S of points in the plane, its unit distance graph G_S is the graph whose vertices are S and where two points are adjacent if they’re at distance 1 in the plane. If you can find S such that G_S has chromatic number k, then the chromatic number of the plane is at least k. And de Grey finds a set of 1,567 points whose unit distance graph can’t be 4-colored.
It’s known that the chromatic number of the plane is at most 7. Idle question: is there any chance of a “polynomial method”-style proof that there is no subset S of the plane whose unit distance graph has chromatic number 7? Such a graph would have a lot of unit distances, and ruling out lots of repetitions of the same distance is something the polynomial method can in principle do.
Though be warned: as far as I know the polynomial method has generated no improvement so far on older bounds on the unit distance problem (“how many unit distances can there be among pairs drawn from S?”) while it has essentially solved the distinct distance problem (“how few distinct distances can there be among pairs drawn from S?”)
Quomodocumque 
[…] 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 […]
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, and I’m pleased to say that Dustin Mixon and Boris Alexeev have confirmed the non-4-colorability of that graph using a completely different algorithm than mine (a SAT solver):
https://dustingmixon.wordpress.com/2018/04/10/the-chromatic-number-of-the-plane-is-at-least-5/#comment-3748
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.
Here are some off the cuff speculations about the polynomial method. My first thought was to see if I could show that the average degree of a unit distance graph had to be less than 6, since that would easily force 6-colorability. (Inductively, color the graph gotten by fixing the lowest degree vertex, then there is a color left for the last one.)
Unfortunately, there are unit distance graphs of degree N for any N. Namely, take N unit vectors v_1, v_2, …, v_N, and let the vertices of the graph be the sums of the 2^N subsets of {v_1, …, v_N}. More generally, if G and H are unit distance graphs, so is
. (The vertices of 
are ordered pairs (u,v) with u in G and v in H, and the edges are ((u,v), (u,v’)) and ((u,v), (u’,v)) where (u,u’) or (v,v’) are required to be edges of G and H respectively.
However, the chromatic number of
is bounded by the maximum of those for G and H. (View the colors as elements of 
, and add the colorings of G and H to produce a coloring of 
.) So this isn’t useful in building counterexamples.
So I wonder whether the polynomial method could show something like “a unit graph with high average degree is approximately the product of unit graphs of average degree less than 6”. This reminds me of a beautiful paper of Green and Tao https://arxiv.org/abs/1208.4714 which shows that if N points determine O(N) distinct lines, then almost all the points lie on a cubic curve.
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
But wouldn’t that give a pretty strong bound on the number of edges in a unit graph with N vertices? At present I don’t think we know better than N^{4/3} and I’m sure people have tried to swing the polynomial hammer at this. N^{1+eps} is conjectured and maybe people conjecture something even more refined, along the lines of what you say here? https://arxiv.org/abs/1709.08048
Yes, I am imagining something which might aim for a bound like
, so if people can’t get beyond 
then I’d say we’re dead in the water. Oh well, that’s why its off the cuff.
@JSE: I believe there is only one known UD graph, mentioned (discovered?) by Ed Pegg, that has e > v^(4/3);it has 16 vertices and 41 edges, and interestingly it is s subgraph of the graphs I explored (though I didn’t come across Ed’s mention of it until after I’d found my solution). See https://math.stackexchange.com/questions/2575268/maximally-dense-unit-distance-graphs for Ed’s post. Perhaps interestingly, in my explorations I got the impression that e > v^(5/4) does not get any harder to achieve as v grows.
It would be extremely interesting if one could get infinitely many examples with e > v^a for any a > 1!
If we think of the plane as C, can we assume all points are algebraic? My guess is yes. If so, in addition to the smallest counter-example by # of vertices, I wonder what is the smallest degree number field containing a counter-example.
@Kevin Your guess is right. The field of real algebraics is real closed, so any collection of polynomials which has roots in the reals also has roots in the real algebraics. (And, of course, a complex number is algebraic if and only if its real an imaginary parts are.) See https://en.wikipedia.org/wiki/Real_closed_field#Model_theory:_decidability_and_quantifier_elimination .
This line of thinking tells you almost nothing about the degree, though.