Coloración del plano: el problema de Hadwiger-Nelson

Abstract

[en] How many colors are needed in order to color the Euclidean plane in a way such that no two points at unit distance have the same color? This problem was first posed by Edward Nelson in 1950, and shortly after the first bounds were found: a lower bound of 4 and an upper bound of 7. These bounds were the best known for almost 70 years, until in April 2018 the biomedical gerontologist Aubrey de Grey shared a graph with 1585 vertices and 7909 edges of length 1, that could not be colored with 4 colors, thus improving the lower bound to 5. Besides looking for graphs with edges of length 1 that can’t be colored with 5 colors (which would further improve the lower bound to 6), one of the current goals is finding a smaller graph that can’t be 4-colored. To that end, two propositional logic tools have proven useful: SAT solvers and DRAT checkers. Currently, the smallest 5-chromatic graph found is due to Marijn Heule, with only 553 vertices. An improvement in both the number of vertices of the smallest 5-chromatic graph and the upper or lower bounds is still being actively pursued.