FOM: computer proofs

[Stephen Cook]

Here is an excerpt from Vladimir Sazonov's Nov 24 message which I think
nicely compares published proofs making use of computers with those
which do not:


==================================================
....  Both a mathematician (which 
himself also works here as a kind of computer) and electronic 
computer are not very reliable (may be by different reasons:  
some illness or crash, etc.).  The main point, as I understand 
it, is that only *formal* proof may be a genuine mathematical 
proof. Of course, what is "formal" was understood in mathematics 
somewhat differently (but quite coherently!) in different 
historical periods and even by different peoples in the same 
period.

However, being human beings, we do not like to write absolutely 
formal proofs and prefer to give only some convincing evidence 
that such a proof may be written (of course, together with some 
intuitive backgrounds behind this proof). We usually (and quite 
reasonably) evaluate this informal evidence much higher than the 
formal proof itself (as written symbol-by-symbol). Using such an 
informal evidence is the main difference between the ordinary 
"human-mathematical proof" vs. "computer proof".  But, 
nevertheless, this evidence concerns exactly to *existence of a 
formal proof*.  ....
=============================================================

The above excerpt seems to me to state the situation well.  
Sazonov's next paragraph is a little less clear, but still interesting:

===============================================
Another (actually self evident but often ignored) point which is 
worth and necessary to note and which I consider philosophically 
important consists in the "requirement" that any formal mathematical 
proof should have intuitively feasible length (i.e. the number of 
symbols). Say, (even feasible) rigorous proof in PA *of existence 
of a proof* of some theorem A is strictly speaking not a feasible 
proof of that theorem (however, it usually can be converted 
into a proper feasible proof of A).  On the other hand, by the 
evident vagueness of the intuitive notion of feasibility, we 
could consider more restrictively as *proper* only those proofs 
which have been checked by *human* beings ("human feasibility" 
vs.  "physical" or "computer feasibility").  Then 4CT may be 
considered as still unproved.  Moreover, it is possible in 
principle that its negation is formally consistent (in this more 
restricted sense of feasibility of proofs). 
===============================

This brings up an interesting question:   Is there a formal version of
Wiles' proof in ZFC which has feasible length?  More problematical
is the same question for PA.

Steve Cook