This is the fifth “research” thread of the Polymath16 project to make progress on the Hadwiger–Nelson problem, continuing this post. This project is a follow-up to Aubrey de Grey’s breakthrough result that the chromatic number of the plane is at least 5. Discussion of the project of a non-research nature should continue in the Polymath proposal page. We will summarize progress on the Polymath wiki page.
What follows is a brief summary of the progress made in the previous thread:
– We now have a 5-chromatic unit-distance graph with 633 vertices and 3166 edges. This is the current record holder.
– We now have a human-verifiable proof that there exists a finite unit-distance graph with a vertex such that there is no 5-coloring of in which is bichromatic (see this and that). This result is “in between” and , since the latter implies the result, which in turn implies the former. Domotor suggests that this might be used to prove .
– We’ve collected several probabilistic inequalities, but we’re still hunting for a human-verifiable contradiction. We have a short computer proof of , and we suspect there’s a human-verifiable proof within reach. Presumably, the proof will involve new ideas that can be leveraged for additional inequalities.
– Tamás Hubai identified all 4-colorings of with the help of a computer. These (finitely many!) colorings are invariant under translation by 8 and rotation by . Presumably, this will help us identify useful claims about the colorings of that are provable by hand.