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.
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.
From Scott Aaronson today:
And de Grey commented: