[FOM] formal proofs

[Freek Wiedijk]

Dear Urs,

>The full formalization is here:
>https://github.com/dlicata335/hott-agda/blob/master/homotopy/BlakersMassey.agda

How many lines of Agda is this including all the Agda files
it imports (and including all non-Blakers Massey related
Agda it needs from HoTT libraries)?  I really would like
to know this.

>I'd think that with traditional foundations even stating this theorem
>formally is impossible for all practical purposes, let alone formally
>checking its proof.

That sounds like nonsense.  I just downloaded a textbook
about homotopy theory (which I don't know anything about),
<http://www.maths.ed.ac.uk/~aar/papers/diecktop.pdf>
and this theorem is proved on page 150.  It all looks very
much like run-of-the-mill mathematics to me.  So if I use my
heuristic of one week to formalize a textbook page, why would
formalizing this proof be more than a single PhD project?

Now maybe you were able to use a lot less than that effort
than that, because you hardwired a lot of homotopy goodies
in your foundations.  But how many man-year has been invested
in the whole HoTT project already?

Freek