FOM: Conclusiveness of Proofs II (a reconstruction)

[JSHIPMAN@bloomberg.net]

Apparently my original post "II" fell into the bit bucket; trying again now:
In my first post I avoided the issue of whether a proof could be made "maximally
convincing" by being completely formalized.  Although there is some hope that
"ordinary" proofs may eventually be done in such a way as to be machine-
checkable (e.g. by the mathematician interacting with a "mathematician's
assistant" software program which produces a 100% formalized proof; I do not
expect to see this for another quarter- to half-century), this does NOT exhaust
the possibilities for "completely convincing argument". Cryptographers routinely
generate 500-digit "primes", relying on the existence of a feasibly computable
predicate P(w,n) which is always "true" for w<n, n prime but false for at least
3/4 of w<n when n is composite.  After 1000 or so random choices of w all give
"true" we are "morally certain" n is prime.  Pratt showed {Primes} in NP so
there is a short "classical proof" in this case but we can't always find it,
and Shamir showed that any set in PSPACE has an "interactive proof system"
whereby we can theoretically attain "moral certainty" re membership.-Joe Shipman