[FOM] Mathematical Certainty?

[Dan Goodman]

As I'm new to this list and not a specialist, I apologise if the ideas below
are completely familiar to everyone and have already been discussed at great
length.

"What is the nature of mathematical certainty in theory and in practice?"

I'm also interested in exactly this question. On the latter part of the
question, I found "New Directions in the Philosophy of Mathematics", edited
by Thomas Tymoczko, very interesting. Many of the ideas mentioned in Harvey
Friedman's post are discussed in that book including the probabilistic
approach to certainty in mathematical proof.

One essay discusses proof checking programs, and argues that we can't rely
on them because as well as the unreliability of the software and hardware
involved, the translation process from mathematics as usually written to a
form the computer can understand is itself highly susceptible to error. The
author (or possibly authors) give the example of the translation of the
usual statement of Fourier's theorem into the language of the proof checking
program - it is almost completely indigestible. This doesn't seem like a
difficulty in principle though, more a comment on the current state of the
art.

Following on from this, another essay in the same book proposes that we look
at the process of mathematical proof as being like engineering. We cannot be
assured that the proof is correct because there are so many ways, known and
unknown, to make a mistake. However, we can guard against the known ways in
which proofs can fail. Methods include: finding an alternative proof or two,
checking proofs by computer using two or more different proof checking
programs, getting more than one person to check the numerical calculations
(if there are any) using different methods, and so forth. In particular, if
a different approach yields the same result, that tells us more than, say,
running the same proof checking program through different compilers or on
different computers.

It seems to me that just as the axiomatic study of arithmetic tells us a
great deal about arithmetic as it is actually practiced without being the
same as it, the study of foundations tells us about mathematical practice
without being the same as it. Just as computer programmers have to worry
about things like overflow errors when writing algorithms which are
mathematically proven to work, practicing mathematicians need to worry about
the stability of their proofs despite believing that the foundations are
secure.

Ideally we want to make our proofs such that isolated small mistakes don't
ruin the entire proof. What's interesting is that informal proofs are often
more stable than purely formal proofs because they are driven by ideas
rather than purely symbolic calculations, and if the ideas are right then a
mistake in the formalism should be easily corrected. The slightly
counterintuitive consequence of this is that maybe we should actually prefer
a slightly informal proof driven by strong ideas to a formal proof checked
by a computer.

Dan Goodman