[FOM] formal proofs

[Steve Awodey]

> On Oct 22, 2014, at 1:36 PM, David Posner <dposner at sbcglobal.net> wrote:
> 
> Professor Schreiber
> Surely, if HoTT mathematics cannot be formalized in set theory then …

The Blakers-Massey theorem is not some exotic "HoTT mathematics”, but standard algebraic topology. 
Moreover, the question was not whether it could in principle be formalized in set theory, but rather whether it can actually be done
in a formal verification system like Mizar.

> On Oct 22, 2014, at 6:32 PM, Joseph Shipman <JoeShipman at aol.com> wrote:
> 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?


Actual examples of the use of Coq to do standard, “non-homotopical” mathematics are not hard to find: 
Gonthier’s team’s recent formalization of the Feit-Thompson theorem comes to mind.
HoTT is an extenson of the basic system of Coq, i.e. intensional Martin-Löf type theory.

Steve