Xref: utzoo comp.theory:853 sci.logic:886 sci.math:11708
Path: utzoo!utgpu!watserv1!watmath!att!rutgers!cs.utexas.edu!uunet!sco!jeffr
From: jeffr@sco.COM (Jeff Radick)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re: Re^4: Question About the Four Color Proof
Summary: What is a proof, anyway?
Keywords: computer proof
Message-ID: <7135@scolex.sco.COM>
Date: 13 Jul 90 23:20:51 GMT
References: <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <9649@hubcap.clemson.edu> <4997@milton.u.washington.edu>
Sender: news@sco.COM
Reply-To: jeffr@sco.COM (Jeff Radick)
Organization: The Santa Cruz Operation, Inc.
Lines: 69

In article <4997@milton.u.washington.edu> aesop@milton.u.washington.edu (Jeff Boscole) writes:
> ...
>Forgive me for being dense....  I've attempted to understand these issues
>thru Philosophy of Science classes and so forth....  Precisely -where- is
>the beef with a "proof by an (unverified.by.hand.calculation) computer
>program?"
> ...

It seems to me that a Philosophy of Science class should address
this issue, but ... well, here's my opinion:

Presumably a "proof" of an assertion, in the general sense of the word,
is a test of its truth.  As used by mathematicians, philosophers,
and logicians, a "proof" is an argument which convinces a person
knowledgeable in the subject matter of the assertion in question
that the assertion follows from some set of hypotheses by a series
of steps of reasoning which are generally accepted as valid.  This
is normally done by stating some series of steps in the chain of reasoning
and either directly or indirectly alluding to some rule by which
that steph should be considered to be valid; usually many steps or rules
are omitted as being "obvious" but which in principle can be provided
by those reasonably knowledgeable in the field in question.  For
example, few proofs will cite "modus ponens" every time it is used
(in fact few will cite it at all) but a mathematical proof might
well cite the Baire category theorem or Poincare's lemma or Gauss'
Theorema Egregium.

The point of this is that a "proof" is in principle something to
be understood by human beings.  If noone understands the chain
of reasoning sufficiently well to be convinced that all steps
are correct, then in a certain very real sense it is not really a
proof.

The question for a proof in which the output of a computer program
is used as one or more critical steps in the reasoning, is whether
or not the output of the program is correct.  If the correctness
of the program is not "proven", then at least in principle the
correctness of the proof citing its output is in doubt.  If the
output of the program is itself intended to be a "proof", then
in principle it can be checked by humans but if it is preposterously
long -- say thousands of pages -- then it is unclear that anyone
will ever really understand it all, so it is unclear that any
human being can really be satisfied that all steps in the proof
are "correct", hence it is not certain that the proof can be
really accepted as "correct".

Thus a practial approach to the problem might be to put the onus
of proof back on the program itself.  If the program is small
enough to be amenable to an acceptably short proof (i.e., short
enough to be understood by a human being) then perhaps its output
and its proof could be accepted as a valid part of the larger proof.

Now it might be that what is actually proven is not the program
itself but rather the algorithm used.  Then the question is
whether the program actually used is a valid implementation
of the algorithm.  This can be addressed in an experimental
sort of way by having different researchers independently
implement the algorithm, then compare results.  However,
the results may still be in doubt since conceivably the
independent researchers may still have a common error.

Whether these issues have been adequately addressed in a way
acceptable to the mathematical community in the case of the
Four-Color problem is beyond my realm of expertise; however
I believe this to be a valid statement of the issues involved.

Jeff Radick
software engineer and math student
jeffr@sco.com or uunet!sco!jeffr or radick@ucscb.ucsc.edu