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


> there is a 125-page attempt at the Poincare' conjecture.  Try it.  If 
> these "provers" find heretofore unobserved flaws, THEN I'll concede that 
> they would be useful tools in mathematics--in uncovering flaws.  But they 
> _still_ don't "prove" that these theorems are correct.  They only 
> convince themselves.  But convincing me that I should believe them 
> involves convincing me that there has been no failure in the program--at 
> any of the levels I've previously discussed.  And, by the way, this is why 
> the general mathematical community is still suspicious of the 4-color 
> theorem.  In fact, the orginal "proof" contained a number of flaws.  
> All discovered were all easily patched, but the fact that they existed in 
> the first place means that we have no reason to believe that something 
> subtle is yet to be discovered.


   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. It's the web of trust model. And before you jump up and 
say "but how can you prove the theorem prover, maybe Godel...", there is a 
very simple theorem prover that is provable via mathematical induction. If 
you don't trust induction, then I don't know what to tell you. (it's like 
denying the Peano postulates) The theorem prover works like this:

Start off with your axiom set and your rules of production. (for instance,
a context free grammar, that might say "if x+y=z is a theorem, then
x+(y+1)=z+1 is a theorem") And enumerate all possible theorems on
the parse tree. If you reach theorems of length N that exceed the
theorem you're trying to prove than either it is a nontheorem or
undecidable. This procedure will never produce a "yes" answer for
a false theorem, although it will fail to prove some theorems. 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.
Physicists aren't suspicuous of relativity either.
[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.]


  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?

  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? How do you know you're not hallucinating?
Even something as simple as Euclids proof of the infinitude of primes.
You think it's been proved? ha! You are merely delusional. The rest of
us sane people saw the disproof years ago, but every time you start
to read the disproof, your mind goes into its own little universe
and starts substituting in screen memories making you *think* 
you just read a proof, not a disproof.
 
  Ultimately, you can't even trust yourself. The world is a risky
place, and sometimes you just have to live with the fact that one
day, something you chose to place faith in and rely on is going to be
pulled from underneath you.

-Ray