FOM: computer proofs

[Don Fallis]

Hi,

The "ideal" procedure for mathematical justification is something like this:

The mathematician writes down a sequence of statements.  She then checks
the statements one at a time to make sure that each statement is an axiom
or follows from previous statements in the sequence.  At the end of this
procedure, the mathematician is justified in believing that the theorem is
true (and that there is a proof of the theorem) because she knows the
justification for each step of that proof.

Of course, as D. Hume pointed out about 250 years ago, this is not a
perfectly reliable source of justification.  Mathematicians sometimes make
mistakes.  As a result, the mere fact that computers (and computer
programmers) sometimes make mistakes does not identify an epistemic
distinction between using computer proofs and using the "ideal" procedure.

Even so, there is clearly an epistemic distinction between using computer
proofs and using the "ideal" procedure.  With a computer proof, a
mathematician may be justified in believing that a theorem is true (and
that there is a proof of the theorem), but not because she knows the
justification for each step of her proof.  (This is so regardless of
whether or not the mathematician has proved the correctness of the program
or even the correctness of the compiler.)

Of course, as M. Detlefsen pointed out in the Journal of Philosophy about
20 years ago, the use of computer proofs is not the only way in which
actual mathematical practice has diverged from the "ideal" procedure.  For
one thing, mathematicians sometimes do not know the justification for each
step of their proofs because they sometimes rely on the expert testimony of
other mathematicians.  I imagine that many of the mathematicians who go on
to derive consequences of FLT will be in just this epistemic position.

Now, the formal study of proof (and the study of the foundations of
mathematics in general) has given us a pretty comprehensive understanding
of the epistemology of the "ideal" procedure.  However, since
mathematicians do not always follow the "ideal" procedure, I would submit
that we do not have anywhere near a comprehensive understanding of how
mathematicians are justified in believing the theorems that they have proved.

Mathematical justification is a very mixed bag.  A comprehensive
epistemological account would have to include accounts of how people are
justified in believing scientific facts about the physical world (e.g.,
facts about how computers work) and of how people are justified in
believing testimony (which, by the way, is not a completely worked out
issue among epistemologists) as well as a lot of other stuff.

By the way, given this situation, I think that it is difficult to say with
conviction that probabilistic proofs (which, like computer proofs, can
provide mathematicians with indirect evidence of the existence of a formal
proof) are epistemically inferior to the other stuff in this mixed bag.

take care,
don

Don Fallis
School of Information Resources & Library Science
University of Arizona