The Chromatic Number of the Plane is at Least 5 - Aubrey de Grey

From Scott Aaronson today:

De Grey constructs an explicit graph with unit distances—originally with 1567 vertices, now with 1585 vertices after after a bug was fixed—and then verifies by computer search (which takes a few hours) that 5 colors are needed for it.  So, can we be confident that the proof will stand—i.e., that there are no further bugs?  See the comments of Gil Kalai’s post for discussion.  Briefly, though, it looks like it’s now been independently verified, using different SAT-solvers, that the chromatic number of de Grey’s corrected graph is indeed 5, including by my good friend Marijn Heule at UT Austin.
If and when it’s also mechanically checked that the graph is unit distance (i.e., that it can be embedded in the plane with distances of 1), I think it will be time to declare this result correct.  Update: De Grey emailed to tell me that this part has now been independently verified as well.  I’ll link to details as soon as I have them.

And de Grey commented:

Yesterday I fixed the bug that led me to believe I had a 1567-vertex solution and reran my deleteability-seeking code overnight ; the result is that I now have a 1581-vertex graph (i.e., four vertices can be removed from the graph that various people verified yesterday) and I have stuck a revised manuscript on the arxiv which should go live later today.