[FOM] Formal Proofs

[Harvey Friedman]

Concerning my statement about Freek's "ugly piece of garbage" (smile).
Here is my entire message:

"This is, of course, a totally unacceptable ugly piece of disgusting
garbage (smile), according to any current standards of mathematical
practice. But I remember reading that there has been some reasonably
successful work on producing nice output. (I was involved in some
early stage in that). Perhaps FOM readers need to be reminded of some
references for creating nice output?

Incidentally, this is a kind of beautiful example, I think just meaty
enough to be interesting.

CHALLENGE: Use this example to create a new field of *micro proof
theory*, whereby new kinds of subtle quantitative and possibly
qualitative features of actual mathematical proofs are investigated,
those which correspond to important features of actual mathematical
proofs that are immediately recognized as interesting and significant
by those reflecting on actual mathematical practice."

Notice the second paragraph above. Also notice that I mentioned the
serious work on making output look like normal math.

Consider the following. There are about 65 faculty in mathematics at
Ohio State. I believe that every single one of these people, when
shown Freek's output, would privately agree that is of "a totally
unacceptable ugly piece of disgusting garbage as mathematical prose".
Furthermore, no standard math journal would ever accept a proof
written that way.

But this is a problem actually being SOLVED - just to what extent, I
don't know, and I thought Freek would know this literature.

I would also have thought that the proof theorists on this thread, or
following this thread, would be rather interested in that Challenge
above. This may be the future of proof theory - or at least of a major
chunk of proof theory. I know that the proof assistant people are
almost entirely focused on implementing more features and having the
stuff under the hood be more powerful - which is of course admirable.

In fact, the Challenge is the best answer that I know to the following
serious criticisms. I.e., that the formal proof movement is at least
obviously good for the development of a deeper understanding of
fundamental features of mathematical proofs. The usual serious
criticisms are in fact rather serious, even if they can be defended
against. So the development of a deeper theory of proofs as a
motivator is actually quite important.

CRITICISMS:

1. The ratio of effort to reward in formal verification of pure
mathematics is ridiculously bad. The defense is that the ratio is
being reduced.
2. When formal verification is particularly important, or a case is
made for that, then special ad hoc tools are used and are needed to be
developed, largely from scratch. A defense might be that one can reuse
at least some of these ad hoc developments.
3. The output is so disgusting that serious pure mathematicians won't
play. The defense is that there is progress on better output.
4. Formal proofs don't raise the certainty level as advertised. The
defense is that maybe it does with self verifying systems. But I think
things get very murky here, and I continue to outline a plan for
making this much much more transparent. Evidence is perhaps coming in
to me that people don't have a good idea as to what my plan is for
this.
5. For some mathematical theorems, there is the unaddressed issue of
whether one has even formalized the theorem perfectly. The defense is
that very often this is not a problem, like FLT as an extreme example.

POSITIVES: (for me, there are enough spinoffs of the formal proof
movement to pique my interest).

1. CHALLENGE above. Micro proof theory - study of new deeper
fundamental features of actual mathematical proofs. Actually, this may
not even have been properly initiated at all.
2. Motivation for the development of and implementation of a truly
massive and massively interesting set of decision procedures. AND,
even when one encounters algorithmic undecidability, there are ALWAYS
associated decision procedures when one goes to large (or even not so
large) input spaces. Easily enough for 10^6 Ph.D. theses and careers.
3. Historically, there has been the informal and wrong idea that
formalization is utterly impossible for state of the art theorems, as
"mathematical proving is not subject to complete logical analysis".
Well, maybe that is the case at the creative conceptual level -
particularly finding proofs and formulating theormes - but we are
talking here at the level of finished polished rigor. Is it possible
to actually have files residing on computers that constitute finished
polished completely rigorous proofs of deep state of the art? The
answer is yes, but only through the formal proof revolution are we
able to have this. I regard this as a principal foundational issue
that has been nearly put to rest. This is a real victory for f.o.m.

BUT now I hear rumblings that 3 has not been put to rest from these
higher homotopy types people. So we come to what I call the UMBRELLA
issue.

The normal course of events is simply to adhere to the time tested
Standard Umbrella of ZFC. Put category theory, usual type theories,
etc., under this Umbrella. After ZFC, immediately create special
infrastructure, which look like simply careful definitions and basic
theorems.

But, just as some category theorists in the good (bad) old days,
pushed for overthrowing the Standard Umbrella, basically replacing it
by a new Umbrella, or overthrowing the whole idea of an Umbrella, we
have some people pushing for something like this again.

What happened with the old movement to overthrow the Standard
Umbrella, is that enough f.o.m. people, philosophers, mathematicians,
and others, considered the overthrowing of the Standard Umbrella, and
generally didn't like the idea of No Umbrella much, and started to dig
in to what it would really entail, foundationally and philosophically,
to replace the Standard Umbrella. They found that the same issues
arise with the New Umbrella, only these issues had already been
properly addressed in the Standard Umbrella, and any way of handling
them in the New Umbrella either caused new problems, or were imitative
of the Standard Umbrella. So the movement to replace the Standard
Umbrella pretty much died (not completely of course). Even MacClane
starts off his book Categories for the Working Mathematician with "a
category is a set of objects, together with a set of arrows,
etcetera". And if you try the category of all categories, etc., you
wind up with difficulties more or less like trying the set of all
sets, etc.

Now with the radical wing of the higher homotopy type people (by the
way, I do know some part timers who are NOT radicals), there is the
idea that we need to overthrow the Standard Umbrella and replace it
with either No Umbrella, or a New Umbrella. The claim seems to be that
there are better reasons for overthrowing the Standard Umbrella than
there were before, with the radical category theorists.

Well, just as in the case of the radical category theorists, these new
radicals are going to have to carefully, and painstakingly, make their
case for the overthrow of the Standard Umbrella to a wide range of
foundationalists, philosophers, mathematicians, even computer
scientists. They are going to have to do two things:

A. Give a completely transparent account of a generally understandable
situation where the Standard Umbrella allegedly really breaks down. It
is easy to point to some math that few people have studied and simply
say "the Standard Umbrella is inadequate" and just leave it at that.
That is completely unconvincing. See the recent FOM postings of Freek
and Levy on this point. Radicals - please comment on Freek and Levy on
this point.I

I think that the radicals want to make a claim that "something really
radical in connection with equality must be done which simply cannot
be handled under the Standard Umbrella". But there are many convenient
ways of handling situations like this. It's called extra information.
A toy example is f:A into B. Well, the usual way of treating functions
is that f:A into B is equaled to f:A into C if the range is contained
in B and in C. HOWEVER, as you know, you can talk of functions as
pairs (graph(f),B), where you pack the codomain into the function. So
you can introduce special variables for "packed functions" F, and use
the notation dom(F) and codom(F). Everything remains beautifully
simple, and this is all within the Standard Umbrella, admittedly based
on ZFC WITH SUGAR. Now this is a trivial example of what is second
nature to any good f.o.m. person. Before overthrowing the Standard
Umbrella, we are going to have to know that highly skilled f.o.m.
people have digested the challenge, presented in generally
understandable terms, and become convinced that such devices -
particularly information packaging with accompanying sugar - don't
work perfectly fine. Radicals who are not steeped in f.o.m. simply
cannot be prima facie trusted.

Here I am acknowledging claims that "yes, it can be done under the
Standard Umbrella, but it is completely impractical". However, it is
fully practical in any situation foundationalists, philosophers,
almost all mathematicians, are familiar with at this point.

B. After A - which of course may (will) never happen - the radicals
have to construct a New Umbrella. Here philosophical coherence,
simplicity, general usability, and general transparency are absolute
requirements. The Standard Umbrella spectacularly meets these
requirements. Some even slightly opaque kind of intensional equality
is not going to work for this. Well, if that becomes the essential
point, then there are serious variants of the Standard Umbrella where
extensionality is dropped. However, my instinct is that I don't like
it, and information packing is highly preferable, with accompanied
sugar.

Harvey Friedman