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

totallybogus 11 Apr 2018 22:44 UTC
3 points
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.
- Rob Bensinger 11 Apr 2018 23:14 UTC
  10 points
  Parent
  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.