It seems that the current status is that the 1567-point graph is 4-colorable (and there was a bug in de Grey’s code), but it was obtained by removing a few too many vertices from a 1585-point graph that’s not 4-colorable (and this has now been [independently] checked by a SAT solver). So we still have a new lower bound of 5 on the chromatic number of the plane; but I need to edit my post because the target is no longer 1567.
If the 1567 figure is wrong, Aubrey de Grey needs to amend that arXiV paper… Also I wouldn’t put too much trust in a result that was reached “by a SAT solver” either, unless either the SAT results came with a proof certificate that can be fed to a formally correct checker, or (in the UNSAT case) the solver itself was formally verified to provide correct and complete results.
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.
Well. That’s really, really, really crazy.
Also, from Noam Elkies on Math Overflow:
If the 1567 figure is wrong, Aubrey de Grey needs to amend that arXiV paper… Also I wouldn’t put too much trust in a result that was reached “by a SAT solver” either, unless either the SAT results came with a proof certificate that can be fed to a formally correct checker, or (in the UNSAT case) the solver itself was formally verified to provide correct and complete results.
From Scott Aaronson today:
And de Grey commented: