[FOM] Formal verification

[Arnold Neumaier]

On 10/21/2014 09:14 PM, Freek Wiedijk wrote:
> Dear Arnold,
>
>> Whereas making a mathematically fully acceptable proof written in
>> Latex formally rigorous (i.e., acceptable to a proof assistent) has
>> an overhead factor of roughly 40, and currently returns nothing but
>> an increases assurance of correctness.
>
> I always claim that properly formalizing a textbook page
> is about one week of work without doing much else.  So you
> claim you could write and polish a latex page in a single
> workhour then?  Well, maybe.

No. I claimed that 1 page of math takes roughly 1/2 h to write in 
handwriting, roughly 1 hour to nicely format in latex (according to 
current standatrds in math), but roughly 40 hours to encode in a proof 
assistant.


> 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.  I think that was Lamport's point
> in his How to Write a Proof.

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


Arnold Neumaier