[FOM] Devlin on incorrect proofs

[Jasper Stein]

> We might be able to raise our confidence level in a checked proof if it
> were written in a precise enough symbolism to be checked by a computer
> program. But then wouldn't some small margin of potential error still
> remain in the supposed correctness of the program itself?---either in the
> specification of the algorithm, or in its implementation, or in the
> physical functioning of the computer? I would like to know from members of
> this list who are in a position to know, whether there are any theoretical
> results about confidence-levels in automated proof-checking that cannot be
> exceeded (perhaps as a function of the length of input, i.e. length of
> proof to be checked for correctness).

There is a whole branch of science / math / informatics devoted to 
automated proof checking and automated reasoning.

Usually these proof checkers utilize the Curry-Howard correspondence to 
convert mathematics into type theory. That is to say, every mathematical 
statement is turned into a type, and a formal proof is then a term of 
that statement's corresponding type.

The idea is that type checking is easy, that is to say, can be performed 
by a very small independent program: so small that it, in turn, can be 
verified 'by hand'. This is called the "de Bruijn-principle". Since we 
are now confident about the validity of the type checking program, we 
can in turn utilize it to infer the truth of mathematical statements: we 
feed the type checker (a) with the formalised version of the statement, 
that is to say, a type; and (b) the formalised proof of the statement, 
that is, a term of the type theory. Then we say "go check that term (b) 
has type (a)". If the term type-checks, the theorem is proved.

Obviously, a 100% security level can never be achieved, for the reasons 
you mention. There is a 'tower' of things to trust: we need to trust the 
Curry-Howard isomorphism to be adequate, then we need to trust our 
capability of carrying out the formalisation without flaws, then we need 
to trust the type checking program, then we need to trust the computer's 
faultless functioning, and therefore we need to trust the compiler, the 
computer's chips, etc. etc. until, at last, we need to trust that our 
understanding of the physical laws is correct, by which we have molded 
the physical materials into a computer.

After some experience with formalised mathematics, I personally feel 
that the biggest issue is the adequacy of the Curry-Howard isomophism, 
that is, the question whether we can faithfully enough represent 
mathematics inside type theory - although there may be ways which I have 
not considered yet, and which would solve the (rather freakish) problems 
I've run into.


Jasper
-- 
Het verschil tussen theorie en praktijk is dat in theorie
er geen verschil is tussen theorie en praktijk.