[FOM] Formal verification
Arnold Neumaier
Arnold.Neumaier at univie.ac.at
Wed Oct 22 03:36:19 EDT 2014
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
More information about the FOM
mailing list