[FOM] Proof Engineering Implications 1

[Harvey Friedman]

I'd like to discuss some issues and topics related to the Proof Engineering
developments.

Proof Engineering is at least tangentially very interesting for foundations
of mathematics.

The main thrust of Proof Engineering, which is to verify as much of deep or
deep/important mathematics as efficiently as possible, is not per se
relevant for f.o.m.

But in the course of its present development, it has already provided
evidence - if not proof - of some basic claims in f.o.m.

Specifically, there was a time when many mathematicians and also a certain
number of logicians - I heard this more from model theorists than other
kinds of math logicians - who were skeptical that one could actually obtain
proofs of deep state of the art mathematical theorems. Obtain in the sense
of it residing on your hard drive. There was the feeling that formalization
is so far removed from mathematical thought that it would forever remain
totally impractical - in two senses. First, the strong sense that any
formal proof of really big deep theorems is going to be exponentially
large. That the formalization process essentially blows up. That somehow
mathematics is inherently informal, and that once you pin everything down
somewhere in a big proof, multiple things arise, each of which has to be
handled, and then multiple things for each of these arise, and so forth,
and things rapidly get totally out of control.

Well, I never believed this story, but I always felt it needed to be
refuted by actual formalization of some big deep theorems.

The second sense where people were skeptical was that, well maybe it
wouldn't exponentiate, but the effort to create formal proofs would be
humanly impossible. The effort involved would be just too great - again
with the idea that mathematical thought is so informal and inherently
different than any formalisms.

Formalization, although still very time consuming generally, is progressing
very well, and many big deep theorems are now formally verified.

HOWEVER, I have the feeling that there are still some kinds of big deep
theorems that one still can be skeptical about being capable of being
formalized and have the proof reside on your hard drive, with a human
amount of effort. Here are some possibilities that may prove thorny. I
don't keep up with anything like all that is going on in Proof Engineering,
and rather than be overly careful, I would like to hear from the experts
some of whom are on the FOM about this.

1. There are some very nasty things going on formally in big deep proofs in
math logic. E.g., the proof in EFA (exponential function arithmetic) that
if ZF is consistent then so are ZFC + GCH and ZFC + not CH and ZF + "the
reals are the countable union of countable sets". and ZFC + "all sets are
Baire measurable".

2. The proof in EFA that the Graph Minor Theorem is not provable in
Pi-1-1-CA_0. There is also the Graph MInor Theorem itself as a piece of
combinatorics.

3. FLT and Poincare Conjecture.

4. Perhaps the BIGGEST of all - when this gets into a "ready to run" state.
This is the confirmation of the consistency of mathematics
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#83. Why the BIGGEST? Because of Goedel's second incompleteness theorem,
there is always a need to constantly run the algorithms sketched in #83.
This amounts to computer verification of instances of a  general fact -
that all of the relevant search spaces have elements. This fact has "proof"
in quotes, because the proof is not in ZFC. The algorithm can be run with
ever larger parameters for ever stronger (or weaker) theories, not just
ZFC. In that way, it never gets old. There is ABSOLUTELY NO NATURAL
STOPPING POINT in this computer investigation.

5. One of the special difficulties with the big deep proofs in math logic -
see 1,2 -  is that the mere statements are nasty, and one must first of all
make sure that there are no bugs in the statement! How do you verify that
there are no bugs in the statement of a theorem, and just what does that
mean?

In another direction for Proof Engineering to take,

6. Prove that the engineering designs for the Supercollider are correct.

But that is starting to take us to the cousin field of software
verification. There is of course the idea that this work on Proof
Engineering we are talking about can be used for software verification.
This is of course obviously true to some extent, but I am curious to what
extent? Almost all of the math in almost all computer programs is
relatively trivial. The issues therefore seems to be somewhat or even quite
different.

As a foundationalist, I am interested in the nature and structure of actual
mathematical proofs. The Proof Engineering community is not too concerned
with my foundational interests.

I am not sure that there is yet a clear systematic communication to the
rest of us of striking logical features of actual mathematical proofs by
the Proof Engineers. When it does become clear enough just what features we
should be looking for, and when these features cannot be just discovered
theoretically and by hand, Proof Engineering probably can easily be adapted
to reveal remarkable things.

I am beginning to have some definite things in mind for a theory of actual
mathematical proofs. However, at this early stage, I can handle it with
theory and by hand, so I don't yet need Proof Engineering.

But what if I ask "what interesting things do we know about actual
mathematical proofs"? What answer do I get?

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140812/0cdab846/attachment-0001.html>