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

[Tjark Weber]

On Fri, 2014-10-24 at 00:33 +0000, Rempe-Gillen, Lasse wrote:
> > 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.

Certainly. However, this feature has existed for many years, and yet we
don't see widespread formalization of results by mathematicians who are
working relative to [insert your favorite conjecture here]. There are
clearly other obstacles as well.

> 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.

Surely. If we didn't think that statements of theorems are (usually)
easier to digest than their proofs, the very concept of machine-checked
proofs would be of questionable value.

Best,
Tjark