1977: The first mathematical theorem to be proven by a computer: No more than four colors are required to color the regions of any given regional map so that no two adjacent regions have the same color.
2005: Following disputes among mathematicians about the validity of computerized proofs, development of Coq – an interactive theorem prover.
To the MNS presentation* Theorem: There is a finite number of “basic” maps which comprise any given map
* Theorem: Five colors suffice to color the regions of any given regional map so that no two adjacent regions have the same color
* Theorem: Two colors suffice to color a chess-like map
* Theorem: Not all maps can be colored with 3 colors (Determining 3-colorability is NP-complete problem)
* Some proofs might not be verifiable by human beings
To the MNS presentationGraph Theory (MSC2010#97K30)
* Map Coloring
* Graphs
Logic (MSC200#97E30)
* Validity of proof
* Proof by computer
To the MNS presentation
To start the presentation click anywhere in the 1st slide.
To move to the next slide use the keyboard arrows
