[FOM] Mathematical Certainty?

[David Corfield]

Dan Goodman wrote:

> 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. 

Which is part of the reason why, when asked what provides 
the main evidence for the Riemann Hypothesis, mathematicians
point to a not-quite-worked out analogy to another field
rather than to the 1.5 billion verifications. Even a gappy network
of ideas can be quite convincing.

>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.

An excellent way of putting it. 

Taking things a stage further, one could take proofs in a field to be 
checks that we've got the strong ideas right and linked properly.

Just one further step and:

"The quest for ultimate triviality is characteristic of 
the mathematical enterprise." (Rota, Indiscrete Thoughts, 93)

David Corfield
Faculty of Philosophy
10 Merton St.
Oxford OX1 4JJ
http://users.ox.ac.uk/~sfop0076