Article published last week in Quanta Magazine on the famous Four Color Problem of Graph Theory.
“It requires four colors to color West Virginia, Pennsylvania, Ohio, Kentucky, Virginia and Maryland — three for West Virginia’s neighbors and a fourth for West Virginia itself.”
The short answer is no. Notation varies from field to field and while there are broadly-agreed standards there are minor variations everywhere. Most people I know who do research mathematics do not believe that more rigorous formalization of notation would help them. Human brains are fuzzy and benefit from loose syntax in certain ways. We are a long, long way from using a language sufficiently well-specified and precise for automated checking to be possible on a large scale. Arxiv.org has a huge corpus for anyone interested in figuring out the scale of this problem.
> Michigan, with its separate upper peninsula, doesn’t actually prevent the U.S. map from being four-colorable, but it could, mathematically.
Couldn't you always "connect" the upper and lower parts of Michigan, four color the map that way, and then erase the line you drew? I'm having trouble seeing why Michigan (or Michigan-like states) could ever pose a problem as it seems to be solvable easily.
Does the hole caused by Lake Michigan pose a problem? I see the number of colors grows if you have a torus, but Lake Michigan (or its equivalent) is a 2D hole not a 3D one.
If you consider water to be included in the four colors, then connecting the upper and lower peninsulas through the water does nothing but move the problem between the Michigan segments to be a problem between the water segments.
If you connect Michigan between the water and the land, then you'll have to account for the fact that the water on one side and land on the other can be colored the same during the connection but _can't_ after the connection is erased.
Surprised that the article didn't mention that the four-color theorem has been fully formalized in Coq[0], which also helped uncover bugs in the original program used to check the configurations. The formal proof remains maintained to this day with CI continuously checking its validity. It's also been packaged into Nixpkgs.[1] So for those who want to follow along at home and rebuild it:
There is a difference between emergence of knowledge in oneself and emergence of knowledge in others. Sure, a computer program checks; however, what we are after is human understanding.
11 comments
[ 3.5 ms ] story [ 38.3 ms ] thread“It requires four colors to color West Virginia, Pennsylvania, Ohio, Kentucky, Virginia and Maryland — three for West Virginia’s neighbors and a fourth for West Virginia itself.”
For example, Sigma (summation) is essentially a for loop.
Couldn't you always "connect" the upper and lower parts of Michigan, four color the map that way, and then erase the line you drew? I'm having trouble seeing why Michigan (or Michigan-like states) could ever pose a problem as it seems to be solvable easily.
Does the hole caused by Lake Michigan pose a problem? I see the number of colors grows if you have a torus, but Lake Michigan (or its equivalent) is a 2D hole not a 3D one.
If you connect Michigan between the water and the land, then you'll have to account for the fact that the water on one side and land on the other can be colored the same during the connection but _can't_ after the connection is erased.
[0] https://github.com/coq-community/fourcolor
[1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...