A colorful problem that has long frustrated mathematicians | Hacker News Reader

A colorful problem that has long frustrated mathematicians

quantamagazine.org

53 pointspyman_in11 comments

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:

  $ nix build --rebuild nixpkgs#coqPackages.fourcolor

Takes 4m 19s on my M1 Pro.

[0] https://github.com/coq-community/fourcolor

[1] https://github.com/NixOS/nixpkgs/blob/master/pkgs/developmen...

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.”

> 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.

Okay I see what you're saying. I was considering water as a hole in the map not a color, but that does make sense.

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.

Does modern math have a universal convention for pseudo code, to directly translate a computer proof idea into code?

For example, Sigma (summation) is essentially a for loop.

Russel and Whitehead attempted to formulate such a convention. Much of our computer science derives from this very idea.

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.

That’s a really nice write up.

Quanta is quality

Reply on news.ycombinator.com