[HN Gopher] A colorful problem that has long frustrated mathemat...
___________________________________________________________________
A colorful problem that has long frustrated mathematicians
Author : pyman_in
Score : 48 points
Date : 2023-04-06 12:17 UTC (1 days ago)
(HTM) web link (www.quantamagazine.org)
(TXT) w3m dump (www.quantamagazine.org)
| siraben wrote:
| 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...
| pyman_in wrote:
| 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."
| nobodyandproud wrote:
| 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.
| leroy-is-here wrote:
| Russel and Whitehead attempted to formulate such a convention.
| Much of our computer science derives from this very idea.
| curiousgibbon wrote:
| 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.
| raincom wrote:
| 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.
| martinjacobd wrote:
| > 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.
| well1912 wrote:
| 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.
| martinjacobd wrote:
| 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.
| jjtheblunt wrote:
| That's a really nice write up.
| intalentive wrote:
| Quanta is quality
___________________________________________________________________
(page generated 2023-04-07 23:02 UTC)