The Hadwiger-Nelson Problem #
The Hadwiger-Nelson problem asks for the minimum number of colors required to color the plane such that no two points at unit distance from each other have the same color.
Reference: Wikipedia
This file points to the canonical formalization in FormalConjectures.ErdosProblems.«508».