# FOM: computer proofs

Stephen Cook sacook at cs.toronto.edu
Wed Dec 2 10:17:38 EST 1998

```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

```