[FOM] formal proofs
Freek Wiedijk
freek at cs.ru.nl
Thu Oct 23 06:11:48 EDT 2014
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
More information about the FOM
mailing list