[FOM] New umbrella?

[Timothy Y. Chow]

Jay Sulzberger wrote:
> On Tue, 28 Oct 2014, Joseph Shipman <JoeShipman at aol.com> wrote:
>> This is exactly the kind of metatheorem I talked about in my
>> previous post. All that remains to be debated, then, is the
>> empirical question of how much mathematics would be better
>> formalized in HoTT "from the ground up" rather than in ZFC. I
>> suspect the answer would be "a small fraction", as judged by
>> number of published refereed papers, but I am very interested
>> in any disagreement on this point, because without disagreement
>> on this point there is really nothing left to argue about.
>
> No.  There remains all the new mathematics of HoTT.  And all the
> mathematics which people who learn HoTT will discover.

I'm puzzled by why there seems to be such a language barrier.

Shipman has explicitly listed some classical theorems in previous posts:

1. Prime number theorem.
2. Geometrization for 3-manifolds.
3. Graph minor theorem.
4. Fundamental theorem of calculus.

It's clear that this is supposed to be a sampling of well-known classical 
theorems; one could easily multiply examples.  Fermat's Last Theorem. 
Classification of finite simple groups.  Independence of the continuum 
hypothesis.  And so on.

The question is whether HoTT offers advantages in the formalization of 
these theorems.  Maybe Shipman erred by using the term "a small fraction," 
which is vague and debatable.  Perhaps referring to HoTT itself as a 
"small fraction" of mathematics is perceived as belittling.  Let's not get 
sidetracked.  There have already been a lot of people getting offended 
(needlessly, in my opinion) in this thread.  The question being posed 
isn't whether HoTT might lead to a wealth of interesting new mathematics 
in its own right.  Doubtless it will.  The question is whether its 
advantages extend to formalizing areas of mathematics for which it has not 
been specifically designed.

Well, does it?  For example, if HoTT had been around 15 years ago, would 
Hales have been much better off using HoTT for Flyspeck?

Tim