[FOM] formal proofs (was: Hersh on Flyspeck

[Harvey Friedman]

On Sat, Oct 11, 2014 at 10:34 PM, Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> When a proof of a major theorem has been completely formalized and
> mechanically checked there is a tendency to think, "So what?  It was a
> lot of work, but we already knew the theorem was true."
>
> Perhaps machine proof-checking will finally come of age when an attempt
> to check an important proof reveals that the informal version of
> the proof is critically flawed in a way that isn't a mere lack of
> formality, and places the truth of the theorem in doubt.
>
> -- hendrik

But I think that the proof checking enterprises have served and
continue to serve an important foundational purpose. Namely, to
establish that absolute rigor does exist in the most concrete sense.
It could have been that absolute rigor was only a formal construct.
E.g., it certainly can be justifiably claimed - and justifiably denied
also - that infinite sets or real numbers to infinite precision are
"merely" formal constructs, and have no "real" existence. We now have
a growing number of examples that the usual foundational schemes for
mathematics do support absolute rigor in an undeniably concrete sense.

Most mathematicians used to believe that big theorems like FLT cannot
be proved with absolute rigor - that there are too many details to
allow concrete existence of an absolutely rigorous proof. Now I am not
sure that they believe this now, as the developments in the
construction of absolutely rigorous proofs penetrate their
consciousness.

The thinking used to be, I think, that rigorous mathematics is an open
ended creative process, and that you cannot create deep mathematical
proofs constrained by any coherent fixed set of axioms and rules. The
refutation of this point of view can be construed as a major victory
for the usual foundations of mathematics.

If you put aside this fundamental foundational viewpoint, then your
issue does arise in a serious way.

Of course, there is another aspect that has tremendous importance, or
at least potential importance at the practical level. That is, the
matter of specifying and verifying the absolute correctness of
computer programs. Of course, this normally involves only relatively
trivial mathematics. Nevertheless, very interesting and important
issues arise as we try to make this more and more powerful and useful.

Harvey Friedman