This is a linkpost for https://arxiv.org/pdf/1804.02385.pdf
Well. That's really, really, really crazy.
Also, from Noam Elkies on Math Overflow:
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.
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.
I hope Aubrey de Grey negotiated the moral trade with the mathematicians successfully, and now that he solved one of their most beloved problems, they will start working on solving aging.
Haha, this would be wonderful. Let's get Terence Tao on the aging problem!
This is a long standing open problem in math. Many people learn about it as early as high school as an example of an open problem, because it is so easy to state:
How many colors does it take to color every point in the plane so that ever pair of points of distance exactly 1 from each other have different colors?
There are simple proofs that anyone here can understand that this number is between 4 and 7, and those were the only bounds we knew for a long time.
The lower bound was improved to 5 recently by Aubrey de Grey! The same Aubrey de Grey that you probably think of as the face of solving aging! He points at a concrete subset of 1567 points in the plane that cannot be colored with four colors.
This is super exciting. I think this is basically the main example of a simple open problem in math that we (used to) have no progress on.
I hope Aubrey de Grey negotiated the moral trade with the mathematicians successfully, and now that he solved one of their most beloved problems, they will start working on solving aging.