[FOM] response to Lasse Rempe-Gillen (Re: Formal verification)

[Rempe-Gillen, Lasse]

> There is plenty support for conditional verification in today's 
> interactive theorem provers. For instance, you can easily defer the 
> proof of a lemma.

This is very useful. I appreciate the dangers of working with unproved theorems, and Andrei's comments about these dangers being magnified when working with automation are particularly illuminating.

Nonetheless, it would seem to me that - if the goal is to move towards more mathematics being formalized - this still seems like a useful approach, as long as one is aware of the pitfalls. Surely it will take less effort to e.g. obtain a 99.99% safe (i.e. checked and agreed by mathematicians) formalization of the statement of FLT, than to formalize the proof of FLT. 

Inevitably there will be some cases where inaccurate statements are found in subsequent formalizations of the auxiliary results. On the other hand, what is potentially more work (e.g. for a potential referee) - check that the statements assumed conform to the accepted statements of standard theorems, or to check the proofs in a normally written article to the same degree of certainty?

Best wishes,
Lasse