[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: computer proofs*From*: Stephen Cook <sacook@cs.toronto.edu>*Date*: Wed, 2 Dec 1998 10:17:38 -0500*Cc*: sacook@cs.toronto.edu*Sender*: owner-fom@math.psu.edu

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

**Follow-Ups**:**Randy Pollack**- Re: FOM: computer proofs**Vladimir Sazonov**- Re: FOM: computer proofs

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]