[FOM] formal proofs

[Timothy Y. Chow]

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?

Tim