Xref: utzoo comp.theory:842 sci.logic:879 sci.math:11669
Path: utzoo!attcan!uunet!aplcen!uakari.primate.wisc.edu!zaphod.mps.ohio-state.edu!swrinde!ucsd!ucbvax!bloom-beacon!eru!luth!sunic!nuug!sigyn.idt.unit.no!sigyn.idt.unit.no!stig
From: stig@idt.unit.no (Stig Hemmer)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re: Re^4: Question About the Four Color Proof
Message-ID: <1990Jul12.172556.5790@idt.unit.no>
Date: 12 Jul 90 17:25:56 GMT
References: <786@qusunu.queensu.CA> <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <9649@hubcap.clemson.edu>
Sender: news@idt.unit.no (Usenet news admin)
Reply-To: stig@idt.unit.no (Stig Hemmer)
Organization: Div. of CS & T, Norwegian Institute of Technology
Lines: 13

The story I have heard is that the output from the program is possible to 
check by hand, and that is was done.

The proof consists of finding a unavoidable set of subgraphs, and then 
showing that each and every one can be reduced.

Both parts were done with computer asistance, but both can be done by hand.
As far as I remember there were ~1000 subgraphs, so it is quite a big task,
but I think they did it.

My source is 'Mathematics: The New Golden Age' by Keith Devlin.

Stig 'Tortoise' Hemmer   aka   stig@idt.unit.no   aka   hemmer@norunit.bitnet