Computers, mathematical proof, and a priori knowledge

The computer played an essential role in the proof given by Kenneth Appel and Kenneth Henken of the Four-Color Theorem (4CT).1 First proposed in 1852 by Francis Guthrie, the four color problem is to determine whether four colors are sufficient to color any map on a plane so that no adjacent regions have the same color. Appel and Heken’s proof involves a lemma that a certain ‘avoidable’ set U of configurations is reducible. The proof of this critical lemma requires certain combinatorial checks which are too long to do by hand. The job was done by an IBM 370/168, using over 1200 hours of computer time. In 1977, Appel and Heken, assisted by John Koch, published the proof, and the 4CT has since been considered an established result. No one has seen the entire proof of the reducibility lemma. It was too long to print out; even if it had been, no one would be able to run through it step by step.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
Download options
PhilPapers Archive

Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 24,411
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

121 ( #36,792 of 1,924,718 )

Recent downloads (6 months)

5 ( #187,017 of 1,924,718 )

How can I increase my downloads?

My notes
Sign in to use this feature

Start a new thread
There  are no threads in this forum
Nothing in this forum yet.