FOM: More on conclusiveness of proofs

[Randy Pollack]

F. Xavier Noria commented:

> Is there anyone so that never have done a proof, which he was
> convinced that it was right, but it wasn't?

This is a good the point.  What does it mean to say "I'm really
certain that Euclid's proof of the infinity of primes is a valid
proof".  An error may still be found tomorrow.  We do mathematics as
best we can, checking a proof ourselves several times, discussing it
with colleagues, sending it to independent referees, etc.  By this
means we gain high confidence that we understand what we're talking
about, but nothing is lost by admitting that we are carrying out a
human activity.  There is nothing absolute about mathematics.

However I disagree with Shipman's comments that randomized proofs
should be as convincing as conventional proofs.  The reason is that a
conventional proof itself is the evidence for our belief.  I can
discuss a particular proof with colleagues and independent referees.
There is no "proof" that can be discussed when we use Rabin's
algorithm.  The trace of a probabilistic proof is not convincing, as
it is the "randomness" of the choices that is important; I must watch
you flip the coins.  Once you write down the choices, they could just
as easily have been carefully selected to give the desired outcome.

Similarly, I'm not convinced by the Appel-Haken proof of the 4-color
theorem, because there is no proof; and even if the checking program
wrote out some kind of trace (of thousands of cases) we humans would
gain no confidence from examining the trace.  We'd do better to
examine the checking program, which is much shorter than such a trace.

If a program checking the 4-color theorem could write out a proof in
some reasonable formal system, we humans probably wouldn't gain
confidence from examining the proof directly, but we could write a
program to check the proof.  If the formal system has few enough
rules, and its side conditions are simple enough to have confidence in
programs that test them, we could gain confidence from this
independent checking.  Further, colleagues, independent referees,
etc., could also write checkers.  This is not quite like just writing
several programs to test the 4-color theorem; as checking a given
formal system should be very simple, while testing the cases of the
4-color theorem involves all kinds of technicalities.

This idea is expanded in my recent paper "How to believe a
machine-checked proof", available on the web
<http://www.brics.dk/~pollack/export/believing.ps.gz>.  The notion of
"proof as evidence" is not completely clear, as there is some size of
proof beyond which we gain no confidence by examining such a proof;
e.g. the 4-color theorem.  My suggestion changes the limits a bit by
admitting indirect evidence: we believe a checker by examnining it
directly (several hundred lines of program) and then believe what it
says about a proof that is too big to examine directly.

-- 
Randy Pollack                            <http://www.brics.dk/~pollack/>
BRICS, Dept. of Computer Science                      <pollack at brics.dk>
University of Aarhus, Ny Munkegade, bldg. 540         Tel: +45 8942 3377 
DK-8000 Aarhus C, DENMARK                             Fax: +45 8942 3255