created, $=dv.current().file.ctime & modified, =this.modified
tags:mathcs
rel: Comedy of Colors
NOTE
I remember encountering this in college, but in reading more about it I learned more.
In mathematics, the four color theorem, or the four color map theorem, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color.
It was the first major theorem to be proved using a computer. Initially, this proof was not accepted by all mathematicians because the computer-assisted proof was infeasible for a human to check by hand.
Thought
This boundary of where we have to be supported by computers in our calculations and proofs
Heinrich Heesch developed a computer program for the proof. Unfortunately, at this critical juncture, he was unable to procure the necessary supercomputer time to continue his work.
On Heesch
In Göttingen, he worked on Group theory. In 1933, Heesch witnessed the National Socialist purges of university staff. Not willing to become a member of the National Socialist organization of university teachers as required, he resigned from his university position in 1935 and worked privately at his parents’ home in Kiel until 1948.
Using mathematical rules and procedures based on properties of reducible configurations, Appel and Haken found an unavoidable set of reducible configurations, thus proving that a minimal counterexample to the four-color conjecture could not exist. Their proof reduced the infinitude of possible maps to 1,834 reducible configurations (later reduced to 1,482) which had to be checked one by one by computer and took over a thousand hours. This reducibility part of the work was independently double checked with different programs and computers. However, the unavoidability part of the proof was verified in over 400 pages of microfiche, which had to be checked by hand with the assistance of Haken’s daughter Dorothea Blostein.
In 2005, Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq proof assistant. This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel.
The four color theorem applies not only to finite planar graphs, but also to infinite graphs that can be drawn without crossings in the plane, and even more generally to infinite graphs (possibly with an uncountable number of vertices) for which every finite subgraph is planar.