[FOM] formal proofs

[Timothy Y. Chow]

Dominic Mulligan wrote:

> Hmm.  Paraphrased, isn't "Roberts' Gauntlet" asking a group of people 
> with no interest of particular expertise in the subject of homotopy 
> theory (Mizar users, who as Roberts points out, in 40 years of 
> continuous development of the tool have not once aimed to formalise 
> homotopy theory --- giving as good an indication as any to where their 
> interests and knowledge lie) to compete in a timed race against experts 
> in the field in formalising a major result?  This is being interpreted 
> as a serious challenge and something we can draw conclusions from ... 
> why exactly?

I was the one who introduced the word "gauntlet", so perhaps I can 
comment.

Recall that Urs Schreiber originally stated, "I'd think that with 
traditional foundations even stating this theorem [Blakers-Massey] 
formally is impossible for all practical purposes, let alone formally 
checking its proof."  David Roberts afterwards strengthened the challenge 
from "impossible for all practical purposes" to "impossible in two years," 
and I agree that raising the bar that high makes the challenge less 
interesting.  Let me stick to Schreiber's form of the challenge.

What I thought made the challenge interesting was the implicit suggestion 
that HoTT (or NCT, as Jay Sulzberger humorously suggested) was such a 
gigantic leap forwards in foundational thinking that "old-style" 
foundations could not possibly begin to compete with it.  To me, this was 
a really striking claim, especially when a concrete example was provided, 
that superficially did not look very different from any other piece of 
advanced mathematics.  I thought that something could be learned about the 
relationship between the "old" and "new" foundations by examining this 
example critically---the alleged Great Leap Forward would either be shown 
to be exaggerated rhetoric, or the rhetoric would be proved to be correct 
in a very concrete fashion.

As it turns out, it seems that examining this example has been rather
instructive (at least to me), even without rolling up one's sleeves to 
start trying to formalize Blakers-Massey in earnest.  I found Paul Levy's 
comments particularly clarifying.  It seems to me to come down to the old 
question that one can ask of any theorem, namely, what is its *real 
content*?

For an ancient example, let's consider the Pythagorean theorem.  What is 
this theorem *really* about?  Is it a statement about the physical world? 
Is it a theorem in Euclid's system?  Or is it a theorem about the real 
numbers, in all their complete-ordered-field, continuum-hypothesis-laden 
glory?  Or is it just a *definition*?

The pragmatist might find this debate pointless, because there are 
standard ways of moving between the different interpretations, so there is 
no need in practice to ask for the true Pythagorean theorem to please 
stand up.  This sort of phenomenon is commonplace in modern mathematics, 
where one author might take X to be a definition and derive Y as a theorem 
and another author might take Y to be the definition and derive X as a 
theorem.  Both are possible, but in practice, picking the right starting 
point can make a big difference.  If you pick definitions that come close 
to capturing the heart of the phenomenon of interest, then your arguments 
will be shorter, cleaner, and clearer.  A different starting point could 
work, but it would cost more.

Without actually knowing anything about the actual content of the 
Blakers-Massey theorem, I think that something similar is going on here. 
Someone might ask, is the theorem, deep down, really a theorem about sets? 
The experts are telling us, no, the actual content of the theorem is best 
expressed purely in the language of HoTT.  If you insist on making it a 
theorem about sets, you can do so, but at a significant cost.  I suspect 
that Schreiber is exaggerating the cost, but it is obvious that there is 
some cost.

This much should be relatively uncontroversial, but I think it gets more 
controversial when some proponents of HoTT suggest, or seem to suggest, 
that it is a superior foundation not just for Blakers-Massey and the like, 
but for all of mathematics.  Joe Shipman made this point.  I, like 
Shipman, am unclear whether HoTT is supposed to be a candidate for this 
role.  Would, for example, the Flyspeck project have been completed with a 
fraction of the effort if HoTT had been used?  Do HoTT proponents envision 
the next generation of undergraduate mathematics textbooks on analysis and 
algebra having their brief summaries of set theory replaced by summaries 
of HoTT?  Will future generations of mathematicians no longer think of a 
finite group as a finite set equipped with a binary operation, or of the 
reals as a set of numbers?  This, to me, is the main question that I 
haven't seen answered by HoTT proponents.

Tim