[FOM] Formal verification

Freek Wiedijk freek at cs.ru.nl
Thu Oct 23 05:41:58 EDT 2014

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.


More information about the FOM mailing list