[FOM] formal proofs
Timothy Y. Chow
tchow at alum.mit.edu
Sun Oct 26 20:56:52 EDT 2014
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
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
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
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.
More information about the FOM