Possible progress on the Hadwiger-Nelson problem (chromatic number of the plane)

Consider a graph on R^2 where two points are joined by an edge iff they have distance 1, in the 50s people wondered what the chromatic number of this graph is and established the trivial lower bound of 4 and upper bound of 7.

By a classic result of De Bruijn and Erdos this problem is equivalent to finding the maximum chromatic number of a finite unit distance graph in the plane, but no further progress was made in decades.

In a preprint published yesterday De Grey claims to have constructed a 1567 vertexes graph which can't be 4-coloured, as can be seen in the comment section of his polymath proposal this was raised to 1585, the non-4-colorability of this new graph seems to have been verified independently with SAT solvers by a couple of people, so that's promising.

As usual that's huge if true, the result looks promising, but time will tell