[FOM] Formal verification

[Freek Wiedijk]

Dear Arnold,

>>And formalization is not just about correctness, it's
>>also about _explicitness._  With a formal version of math,
>>there is no space for unclarity what the definitions and
>>steps in the proofs are.
>
>This is one of the main reasons why most mathematicians will not use
>the present generation of proof assistants. For the mathematical
>language is designed (and even highly optimized) in a way that one
>can leave most things unsaid and still convey a (usually) correct
>proof correctly to the reader (who may have to do a little
>interpretation work, a skill learnt during the standard university
>math education).

So with this the computer helps.  When formalizing you
_don't_ have to give all the details _yourself_ (the
automation of the system helps a lot with that, and if the
AI guys like Josef are right, it might even get much better
in the near future.)  But all those details still _are_
there, inside the computer memory.

Freek