[FOM] formal proofs

[Joseph Shipman]

What I am confused about is whether Homotopy Type Theory is supposed to be a foundation for the type of mathematics you give examples of, or whether it is supposed to be a foundation for all of mathematics.

For example, would there be any point in trying to formalize a proof of the Prime Number Theorem, or of Perelman's proof of the Geometrization conjecture for 3-manifolds, or of the Robertson-Seymour Graph Minor Theorem, in HoTT? Does HoTT have any advantages over ZFC for proving those three theorems?

If not, then I would like an estimate of what fraction of contemporary professional mathematics (as measured by published proofs) is the type of mathematics for which HoTT is better suited than ZFC to completely formalize it.

-- JS

Sent from my iPhone

> On Oct 21, 2014, at 11:34 PM, Urs Schreiber <urs.schreiber at googlemail.com> wrote:
> 
>> On 10/21/14, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
>> Urs Schreiber wrote:
>> 
>>> A good example of this is the formal proof, in HoTT, of the
>>> Blakers-Massy theorem
>>> (http://ncatlab.org/nlab/show/Blakers-Massey+theorem) by Lumsdaine,
>>> Finster and Licata. The full formalization is here:
>>> 
>>> https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda
>>> 
>>> I'd think that with traditional foundations even stating this theorem
>>> formally is impossible for all practical purposes, let alone formally
>>> checking its proof.
>> 
>> This is a nice gauntlet!  Before a traditionalist embarks on a project to
>> refute this claim, let me clarify what is at stake.
>> 
>> Question for Urs: Suppose a traditionalist were to thoroughly refute your
>> claim above.  Would that "score any points" for the traditional side in
>> this debate?  Or is this just a casual remark on your part, which if
>> refuted would not cause you to change your mind on any substantive issue?
> 
> 
> This was not a casual remark, this was a reply to the question that
> has been repeatedly asked here, as to what the point of homotopy type
> theory is.
> 
> It had been mentioned here before that homotopy type theory [1] offers
> some advantages for formal set-based mathematics, such as providing
> quotient types and isomorphism invariance. What seems not to have been
> mentioned much before here is that the key point of homotopy type
> theory however is that it goes way beyond this in that it provides a
> native (i.e. direct, synthetic, see below) formalization not just of
> constructive set theory, but of homotopy theory [2] (aka algebraic
> topology). And the neat thing is: of homotopy theory in its modern and
> most powerful incarnation in the guise of infinity-toposes [3].
> 
> Just like plain dependent type theory is the internal language of
> locally cartesian closed categories, so homotopy type theory is the
> internal language of locally cartesian closed infinity-categories, and
> homotopy type theory with univalent type universes is the internal
> language of infinity-toposes [4, 14]. This means that homotopy type
> theory provides a "structural" foundation of the kind that William
> Lawvere had found in topos theory [5], but refined to homotopy theory
> in the refined guise of infinity-topos theory.
> 
> My statement that the mathematics of homotopy theory and algebraic
> topology is beyond the scope of what may practicably be implemented in
> tradtional set-based foundations was not meant to be provocative.
> Looking at the mathematics that has been implemented in set-based
> foundations over the years [6] and extrapolating this progress into
> the future, it seems uncontroversial to me that the formalization of
> just the basics of simplicial homotopy theory [7] and higher topos
> theory [8] in traditional set-based mathematics is prohibitively
> tedious, and that using traditional set-based mathematics to engage in
> the formalization of proof of theorems of practical interest in these
> fields is out of the question, not in principle of course, but for all
> practical purposes.
> 
> And yet, homotopy type theory natively knows about all this.
> 
> For instance the formal proof [9] of the Blakers-Massey theorem [10]
> does not need to begin by first formalizing what a simplicial set is,
> what a Kan fibrancy condition is, what the infinite tower of homotopy
> groups is, what weak homotopy equivalences are, what homotopy pushouts
> are, how they reflect in long exact sequences of homotopy groups;
> because all this is native to homotopy type theory. Accordingly, the
> proof [9], on top of being a formal proof, is elegantly transparent
> and of actual practical interest. Moreover, since the formal HoTT
> proof [9] generalizes the traditional statement to more general
> infinity-toposes, it is actually a genuine new mathetical result of
> genuine interest in modern homotopy theory, to practicing
> mathematicians not concerned about foundations. This seems to be a
> kind of achievement unheard of [6] within the traditional
> formalization of set-based mathematics.
> 
> The reason why this may happen with homotopy type theory, the reason
> why homotopy type theory provides not just any but provides a
> practical foundation for mathematics including modern homotopy
> theory/algebraic topology, is that it provides a "synthetic" language
> for these topics, which allows to formally speak about the basic
> concepts natively without the need to first formalize several
> textbooks worth of material starting from bare set theory to even get
> started.
> 
> To my mind these are statements of the obvious to anyone who looked
> into the matter. The fact that they are not more widely appreciated is
> not due to this being possibly controversial, I believe, but because
> the intersection of the sets of researchers who genuinely appreciate
> modern homotopy theory in the guise of higher topos theory and those
> who appreciate formal logic, type theory and what it means to have an
> internal language of a higher topos is very small.
> 
> Indeed, also various of practitioners homotopy type theory care only
> about the truncation of the theory down to set theory, to "hsets"
> [11]. The crucial relation of homotopy type theory to higher topos
> theory was Steve Awodey's vision [12]. It has been realized notably by
> Mike Shulman [13,14], Peter Lumsdaine [15] and others and deserves to
> be more widely known.
> 
> Mike Shulman's 2012 course notes [16] are possibly still the best
> introduction on this matter. Anyone trying to get an idea of what the
> point of homotopy type theory is as a new practical foundation for
> modern high-level mathematic rooted in homotopy theory and higher
> topos theory could do worse than starting with these notes.
> 
> 
> [1] http://ncatlab.org/nlab/show/homotopy+type+theory
> [2] http://ncatlab.org/nlab/show/homotopy+theory
> [3] http://ncatlab.org/nlab/show/(infinity,1)-topos
> [4] http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory
> [5] http://ncatlab.org/nlab/show/ETCS
> [6] https://plus.google.com/+UrsSchreiber/posts/YS6asZLgbbj
> [7] http://ncatlab.org/nlab/show/Simplicial+homotopy+theory
> [8] http://ncatlab.org/nlab/show/Higher+Topos+Theory
> [9] https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda
> [10] http://ncatlab.org/nlab/show/Blakers-Massey+theorem
> [11] http://ncatlab.org/nlab/show/set+theory#ReferencesInHomotopyTypeTheory
> [12] http://ncatlab.org/nlab/show/homotopy+type+theory#Awodey
> [13] http://ncatlab.org/nlab/show/homotopy+type+theory#Shulman12
> [14] http://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos
> [15] http://ncatlab.org/nlab/show/higher+inductive+type#ShulmanLumsdaine12
> [16] http://ncatlab.org/nlab/show/homotopy+type+theory#ShulmanCourse
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom