The chromatic number of the plane (Hadwiger-Nelson problem) is a maths problem dating back to the 1945.
How many colors are needed to color the plane so that no two points at unit distance are the same color?
Aubrey de Grey’s breakthrough result in early 2018 proved for the first time that at least 5 colours are required. Since then mathematicians from around the world have been continuing to work on the problem through Polymath16.
This is a library/ collection of code designed to give someone looking to dig into this fascinating problem a good starting point. It’s designed to be used in jupyter notebooks. Pull requests and ideas are welcome.
CNP>=5 is a library that replicates De Grey’s result in python, along with several ‘optimizations’ invented by others. The code includes functions to generate, among plenty of others, De Grey’s original N graph, and prove there is no way to colour it with 4 colours using the fantastic PySAT.
#TODO: Include image of N
It also includes a starting point for finding minimal graphs (one of the goals of the Polymath project). There are several functions included for finding smaller graphs from Unsat-Cores, generated by the solver. It can also generate minimal graphs - graphs where removal of any node will lead to a colour-able graph, from a Minimal Unsat Core (MUS). This is a technique used in generating the current records for the smallest graphs (given enough computing power).
#TODO: Show image of minimal proofs for smaller c Starting graph, and resulting minimal proofs for CNP > 1, 2, 3
Also, I include a collection of code for creating and manipulating graphs in intuitive ways. Rotating, shifting, and merging. Since math is done exactly in Sympy, the resulting graph can later be confirmed to be exactly unit length without worrying about floating point precision.
Use requirements.txt to grab the nessasary packages.
pip install -r requirements.txt
And check out Example.ipynb for some examples!