NetNews Usenet Archive 1992 #18/NN_1992_18.iso/spool/comp/arch/8854

Internet Message Format | 1992-08-12 | 4.2 KB

Xref: sparky comp.arch:8854 alt.folklore.computers:12446 comp.benchmarks:1290
Newsgroups: comp.arch,alt.folklore.computers,comp.benchmarks
Path: sparky!uunet!haven.umd.edu!darwin.sura.net!zaphod.mps.ohio-state.edu!uwm.edu!zazen!schaefer.math.wisc.edu!wilson
From: [e-mail] (Bob Wilson)
Subject: Re: dinosaur horsepower
Message-ID: <[e-mail]>
Reply-To: [e-mail] (Bob Wilson)
Organization: Univ. of Wisconsin Dept. of Mathematics
References: <[e-mail]> <[e-mail]> <[e-mail]> <[e-mail]>
Date: Wed, 12 Aug 92 15:03:56 GMT
Lines: 63

In article <[e-mail]> [e-mail] (Ellyn Sandor) writes:
>[e-mail] (J. D. McDonald) writes:
>>In article <[e-mail]> [e-mail] (Robert Bernecky) writes:
>>>I'm just finishing a course in Philosophy of Math. One topic we covered
>>>was computer proofs, with the 4-colo(u)r theorem as the prime example.
>>>The prof (Jim Brown -- a superb lecturer, and excellent teacher, for
>>>those of you interested in the topic!) noted that the proof took
>>>months on a "supercomputer".
>>Subjectively the same problems I did then run faster now on a high end
>>PC .... which also draws little balls showing the atom positions
>>on the screen, doing ball color fills in software, in real time.
>
>    I'm not mathematician, but I remember reading and dimly understanding
>parts of the proof in question.  I seem to remember that the parts of the proof
>are organized in "rings" and the software exhaustively proved all sub-proofs
>up to a given ring.  Each ring was exponentially much bigger than the other,
>with rings 1-3 provable by hand (with 3 being a pain in the butt), ring 4
>requiring a computer, and ring 5 being (at the time) unprovable without a way
>bigger computer. (or one of those thingies where people say "even with a
>computer the size of the universe, it can't be solved in less time than it
>takes to count all the quarks in the universe, unless you buy the hackers
>more Jolt and Thai food than has existed in all of history")
>    On the other hand, the importance of each higher ring was appropriately
>diminished: i.e. proving ring 1 meant about a 50% chance of the proof being
>true, proving ring 2 meant 75% chance, ring 3 90%+, and ring 4 99.9%+.
>    OK, this is probably full of holes, but anyway:
>    1) How close is this is to the (very general) idea?
>    2) How long does it take to rerun the proof on a modern hot machine
>    3) Can we do ring 5 now?
>
>        Showing my ignorance
>                Stephan
>--
>--
>Stephan Meyers | [e-mail]
>(Art)^n Laboratories, inventors of the Stealth Negative PHSCologram
>[phone]
This is not my particular area of math but I am pretty sure the proof
dosn't run quite that way. Here is a paraphrase as I recall it:
(1) Traditional, human mathematical techniques are used to show that if
there is any map which is not four-colorable then one of a finite
collection of classes must containt a map which is not four-colorable:
There might be other non-four-colorable maps not in these classes,
but if there are any at all there will be at least one in the collection.
(2) Human techniques produce a set of construction techniques which if
carried out exhaustively would create examples from all the classes
described in the collection in (1).
(3) Human techniques create tests which can tell if a given map is
four-colorable, not necessarily by actually exhibiting a coloring.
(4) The computer power is used to carry out the constructions in (2)
and show using the techniques of (3) that each class is
four-colorable. Since each turns out to be so there can be no maps
(meeting the hypotheses of the theorem, of course) which are not
four-colorable, by (1).

What the proof is really belongs in some other group, but since it
is popular to talk these days about proofs which are only
probabalistically "true" it seemed appropriate to show why this
is not one of them. This is possibly relevant to this group since
many of the places such proofs ARE being used is in connection with
properties of computing systems.
Bob Wilson
[e-mail]