[FOM] Talk on Formal Verification

[Josef Urban]

On Jan 31, 2016 2:33 AM, "Mario Carneiro" <di.gama at gmail.com> wrote:
>
>
>
> On Sat, Jan 30, 2016 at 2:05 PM, Ben Sherman <sherman at csail.mit.edu>
wrote:
>>
>> I think it's important to distinguish between computation required for
proof search and computation required for proof checking. While I can
imagine using lots of computation for proof search, I doubt that the
verification of any "good" proof of a "major theorem" should require
excessive computation (not including dependencies).
>
>
> To me this is a major flaw in Flyspeck (which I might have the
opportunity to rectify in my lifetime) - it takes too long to run. My
personal views are probably nonstandard in this regard, but I would spend
100 times the computation to cut down the size of a formal proof by half
(since the one-time cost will eventually pay dividends in later
re-verifications).

I think Flyspeck will indeed serve for many experiments of this kind. The
part which now takes long (and was parallelized) is however not the
standard "proof search". Most time is taken by "doing verified arithmetics"
- i.e., a large number computations done in such a way that all the
operations go through the HOL Light kernel.

There might be various ways how to further speed it up, but quite some work
has already been done on that - see e.g. Alexey Solovyev's PhD thesis.

Josef
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160131/4d4014d0/attachment.html>