[lnkForumImage]
TotalShareware - Download Free Software
Confronta i prezzi di migliaia di prodotti.
Asp Forum
 Home | Login | Register | Search 


 

Forums >

comp.lang.lisp

4 color map theorem

Pascal J. Bourguignon

9/30/2015 1:48:00 PM


Wouah! It's already been 39 years since we have this software generated
proof:


https://en.wikipedia.org/wiki/Four_col...

During the 1960s and 1970s German mathematician Heinrich Heesch
developed methods of using computers to search for a proof. Notably he
was the first to use discharging for proving the theorem, which turned
out to be important in the unavoidability portion of the subsequent
Appel-Haken proof. He also expanded on the concept of reducibility and,
along with Ken Durre, developed a computer test for it. Unfortunately,
at this critical juncture, he was unable to procure the necessary
supercomputer time to continue his work (Wilson 2014).

Others took up his methods and his computer-assisted approach. While
other teams of mathematicians were racing to complete proofs, Kenneth
Appel and Wolfgang Haken at the University of Illinois announced, on
June 21, 1976,[9] that they had proven the theorem. They were assisted
in some algorithmic work by John A. Koch (Wilson 2014).

â?¦

â?¦ the unavoidability part of the proof was verified in over 400 pages of
microfiche, which had to be checked by hand (Appel & Haken 1989).


--
__Pascal Bourguignon__ http://www.informat...
â??The factory of the future will have only two employees, a man and a
dog. The man will be there to feed the dog. The dog will be there to
keep the man from touching the equipment.� -- Carl Bass CEO Autodesk