[FOM] formal proofs

[Urs Schreiber]

On 10/22/14, David Posner <dposner at sbcglobal.net> wrote:

> So the statement that there are mathematical theorems for which set
> theoretic formalizations cannot or even might not exist would imply that


No, I am talking  -- rather explicitly so, I'd think, please see my
message -- about practicable formalization, not in-principle
formalization.

I have been recalling what would seem to be a commonplace: that
formalization in traditional foundtions of results that are of actual
interest in contemporary mathematical research practice tend to very
quickly become extremely tedious, to the extent that it is hardly ever
done at all and quickly becomes impossible for all practical purposes
(while of course in principle, one imagines, it should always be
possible).

While this is commonplace (or so I would have thought), the
interesting new fact which deserves to be highlighted more is that in
the foundations of homotopy type theory, some high-level statements of
actual interest in contemporary fields such as modern algebraic
topology may have formalization not only in principle, but
practically, it may even happen (unheard of in traditional
foundations) that a formal proof is given of an result of interest for
research mathematicians for which no informal proof had been known
earlier (such as the proof of the Blakers-Massey theorem for general
infinity-toposes).

David Roberts offered a more pronounced version of this issue of
practicality in his message
http://www.cs.nyu.edu/pipermail/fom/2014-October/018249.html

This is much in the spirit of Paul Taylor's "Practical foundations of
mathematics"

 http://ncatlab.org/nlab/show/Practical+Foundations+of+Mathematics

only that it is yet a bit better even. Where Paul Taylor argued that
type theory and its categorical semantics offers a practical advantage
over traditional foundations, homotopy type theory carries this
further and observes that taking the constructive aspect fully
seriously in taking intensional identity types fully seriously makes
type theoretic foundations actually be a practically useful formal
language for homotopy theory and topics that are considered in
contemporary research algebraic topology.