Let me mention (again) my paper that touches on many of these points:
@InProceedings{Pollack:belief,
author = {Robert Pollack},
title = {How to Believe a Machine-Checked Proof},
booktitle = {Twenty Five Years of Constructive Type Theory},
editor = {Giovanni Sambin and Jan Smith},
year = 1998,
publisher = {Oxford University Press}
}
Also available from <http://www.brics.dk/~pollack/export/believing.ps.gz>.
There is a distinction between 2 kinds of computer proofs that has not
been clear in the recent FOM discussion. In one kind of computer
proof, we use a computer to syntactically check a (more or less
explicit) derivation in a given formal system. Usually, a user gives
some commands that a system like Mizar "compiles" into atomic steps of
a formal system. (Of course, allowing reference to already proved
statements.) Mizar claims to check a particular formal system, but
doesn't actually construct a representation of the formal proofs it
checks. Some proof systems such as Mike Gordon's HOL do, implicitly,
construct such a proof. Taking it even further, my own proof checker,
LEGO <http://www.dcs.ed.ac.uk/home/lego/> constructs explicit
representations of proofs in the Extended Calculus of Constructions
(ECC), which can be independently checked without knowing anything
about the internal structure of LEGO. As long as you know the
inference rules for ECC, you can check a proof yourself, or write your
own computer program to check such proofs. Such an independent
checking program only needs to syntactically check a particular formal
system, i.e. a few axioms and rules. No matter how long the _proof_
to be checked, the proof checker is a simple program, much simpler
than many informal mathematical proofs in textbooks. I am not
claiming "absolute certainty" here, I'm comparing complexities.
The implementation of such a proof checker may use machine arithmetic
to implement the syntactic check of the given formal system, but if
the proof being checked involves arithmetic, it will be the formal
arithmetic defined in the formal system, and will not call machine
arithmetic to execute the steps directly.
The second kind of computer proof is like the 4CT proofs discussed on
this list. Some informal algorithms are programmed and executed on a
computer. These may be long, complicated and subtle algorithms (if
the necessary computation is very long, there will be much
optimization of the program), which makes it hard to believe.
Also we are expecting that the semantics of the computer to
match some informal mathematical foundation. For example, the
[Robertson, Sanders, Seymour] quote posted by Steve Cook says
> ... our programs use only integer arithmetic, and so we need not be
> concerned with round-off errors and similar dangers of floating
> point arithmetic.
But it still depends on correct integer arithmetic, perhaps arbitrary
precision, etc., as implemented in hardware.
Finally I agree entirely with Sazonov's point "that any formal
mathematical proof should have intuitively feasible length". In fact
proof checkers of the first kind, that actually construct a
representation of a proof, seem to enforce this requirement. So much
so that the business of completely formal mathematics (or "explicit
mathematics") is largely finding formal systems that we believe and
that support proofs of feasible length.
--
Randy Pollack <http://www.dcs.gla.ac.uk/~pollack/>
Computing Science Dept. <pollack at dcs.gla.ac.uk>
University of Glasgow, G12 8QQ, SCOTLAND Tel: +44 141 330-6055