The Hadwiger-Nelson problem asks for the chromatic number of the plane, i.e., the minimum number of colors needed to color the plane if no two points at unit distance one from one another are given the same color. The problem was first discussed (though not published) by Nelson in 1950 (Soifer 2008, de Grey 2018). Since that time, the exact answer was known to be 4, 5, 6, or 7, with the lower bound provided by unit-distance graphs such as the Moser spindle and Golomb graph (both of which...