From: Nathan Zook <nzook@bga.com>
Date: Sun, 6 Aug 95 22:50:13 PDT
To: Ray Cromwell <rjc@clark.net>
Subject: Re: RSA has been proved correct
In-Reply-To: <199508070329.XAA11774@clark.net>
Message-ID: <Pine.3.89.9508062316.U15677-0100000@maria.bga.com>
MIME-Version: 1.0
Content-Type: text/plain




On Sun, 6 Aug 1995, Ray Cromwell wrote:

>    All you need to do is verify yourself (i.e. formally prove the
> correctness of the theorem prover) to rely on the results of the
> theorem prover. 

Oh, is THAT all?  (more on this later)


> denying the Peano postulates)
(Perish the thought!)

>The theorem prover works like this:

<elided brute-force prover>

Do you advise using the unabridged Archimedian Sieve to determine if a 
number is prime?

> a false theorem, although it will fail to prove some theorems. 

Just feed it ~X as well.

> And it is
> news to me that "the general mathematical community is still suspicious of
> the four color theorem." Not only are they not suspicous of the theorem,
> they aren't suspicious of the proof. It's been verified and reproduced
> over and over again, and it has also been shortened down from the
> original (I believe 2000+ special graph cases) to just over 400.

Now we hit an impasse.  I thought the 4-color theorem was considered done 
as well, until a professor of mine contradicted me on this point.  It 
sounds like you might have more current info.  (Mine is 2-3 years old.)


> [note above: the theorem prover fails if the production rules allow
> theorem shortening. The system must be primitive recusive, but there
> are many restricted domains of theorem proving which are.]

Very restricted, I would think.  Most cases of universalizing would, I'ld 
guess.

>   The classification of the simple groups was a 1000+ page written
> proof. Which one is would you trust to have a mistake somewhere? The
> computer checked one, or the human checked one?

That depends on my trust of the human and of the checker.  Frankly, I'ld 
be leary of either.  (And I was told in Algebra that it was 10k+, but the 
point is basically the same.)

>   This general line of discussion is getting out of hand. You can't
> *prove* anything for sure. Even if it seems logical to you, how do you
> know your own mind isn't buggy? 

This is one of the points that I have pushed on this issue.  Our intution 
on many of these matters is _way_ off until you train it.  And still, 
there are famous cases of failure by trained people.

>   Ultimately, you can't even trust yourself. 

That's why we go to school.


Okay, on the subject of verifying theorem checkers:

First, you mention some distance into your post, that the theorems being 
checked must be "primitively recursive".  That rather limits you away 
from interesting theorems, wouldn't you say?  In particular, you couldn't 
dream of touching those earlier mentioned biggies.  But that's not all.  
Try the Galois theorems.  Fermat's little theorem?   Barre' catagory 
theorem?  Chinese Remainder Theorem?  Fundamental Theorem of Algebra?  
(In topology, in complex anal, in algebra...)

So I assume that the theorem checkers being deployed aren't limited to 
handling primitively recursive systems.  You now are dealing with a 
rather extensive program.  And proving that a general theorem prover 
works is _not_ something to just sit & do.

.......

Nathan