Xref: utzoo comp.theory:854 sci.logic:887 sci.math:11709
Path: utzoo!utgpu!news-server.csri.toronto.edu!torsqnt!hybrid!scifi!bywater!uunet!mstan!amull
From: amull@Morgan.COM (Andrew P. Mullhaupt)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re: Re^4: Question About the Four Color Proof
Summary: Oh No! Loop invariants again.
Message-ID: <1233@s8.Morgan.COM>
Date: 13 Jul 90 16:23:10 GMT
References: <786@qusunu.queensu.CA> <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <9649@hubcap.clemson.edu>
Organization: Morgan Stanley & Co. NY, NY
Lines: 74

In article <9649@hubcap.clemson.edu>, steve@hubcap.clemson.edu ("Steve" Stevenson) writes:
> amull@Morgan.COM (Andrew P. Mullhaupt) writes:
> 
> >... includes comments by Graph Theory experts ...
> >suspect a hole in the arguments which reduce the problem.... This kind of
> >thing goes on all the time in math, and doesn't differentiate the
> >FCT from most other spectacular conjecture resolutions.
> 
> 
> True enough, however my interest is in the fact that a computer program is
> involved. In the philosophical sense, has FCT been `proven' if it has an
> `unproven' computer program in the middle?

I am not aware of any reason that the computer part of the FCT proof
should not be proven; what I mean here is that the source for the
program can (and should) be equipped with a proof of partial correctness.
(Since we know it halts, partial correctness implies total correctness.)
Now the only hole in such an approach is faulty execution of the
program by the system which processes it. (Likely a compiler or
interpreter, an O/S and some hardware.) Now correctness of compilers
and operating systems should be a given, but it's not. At present,
the communities which produce compilers and operating systems are not
sufficiently convinced of the merit and feasability of correct compilers
and operating systems to produce them. So we can consider the whole of
the proof from the compiler/interpreter, through the operating system
and hardware as a single processor and assess the risk of error.

The first point is the nature of errors. There are no floating point
computations (as far as I know) so that a Lanford style proof by
estimates is not necessary. The answer is either that you can successfully
dispense with each of the finitely many critical cases or no you can't.
Now the likelihood of an error in the hardware over the run in question
is (on today's machines) a fixed small number, likewise the operating
system and compiler. You can satisfy practical doubts you may have
regarding the computation by repeating it more than once with different
hardware, compilers and operating systems. (It might be easier to use
different flavors or versions of the same operating system so long as
they arent the same code.) It now becomes a problem in statistics to
compute confidence bands for the hypothesis that the set of computations
you have performed has been without error. You can quite reasonably
expect to obtain results which are as good as you could obtain for
passing manuscripts through referees, etc. So as a practical matter
there is not much reason to treat computations as different from
proofs.

The other issue is that the computer proof of the FCT is not even in
principle checkable by humans in reasonable time; whereas other, 
equally stultifying proofs (e.g. Carleson's pointwise convergence of
L2 Fourier series theorem) _can_ be checked by _some_ (very determined)
humans, even though most of us mortals take the experts' word on it.
Well ok. There it is. You pays your nickel and you takes your choice.
Who are you going to believe? 

This is not an idle issue; the recent proof of the Wagner conjecture
(yet another jihad most of us will not experience in our lifetimes)
results in a way to show that lots and lots of interesting kinds of
graphs have only finitely many minimal cases under minors. I.e. this
is a machine for resolving lots of questions in graph theory in the
same way as the FCT. Before he got g_19 by hand, Deshouillers was 
aware that the result could have been had by exhaustion to the then
best estimates by the use of a massively parallel computer. We almost
went ahead and did it, too. A lot of mathematics is coming in range
of cheaper and faster computers as time goes by, and we're going to
see more and more cases where results hang by hybrid proofs. 

My response is twofold. We have to make mathematicians aware of the
fact that programming can be done as theorem-proving. We have to
institute a standard for quality control in computation. The right
people to do it are the mathematicians, because they have the greatest
need to understand the reliability of computations, and because they
are the best equipped to face the problems involved.

Later,
Andrew Mullhaupt