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

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/

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$.

---

[1] Pritikin, Dan. "All unit-distance graphs of order 6197 are 6-colorable." Journal of Combinatorial Theory, Series B 73.2 (1998): 159-163.