[FOM] Talk on Formal Verification

[Colin McLarty]

On Fri, Jan 29, 2016 at 4:22 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:


> A typical semiformal proof of a major theorem should, nowadays, be thought
> of as including a few hundred CPU hours of computation with commercial
> software on a machine with a few terabytes of space.


Are there some kind of data to support this?  I certainly have no data, but
I admit to doubting this is typical.

This computation time is in the ballpark for the recent proof of the
largest yet known Mersenne prime. The Mersenne project at
http://www.mersenne.org/primes/?press=M74207281 reports that took 31 days
of non-stop computing on a PC with an Intel I7-4790 CPU (it has since been
checked in much less time on much larger machines).

And checking Mersenne primes is not typical, it is generally taken as an
extreme example of computation-consuming math.

The Flyspeck Project reported taking about 5000 processor-hours (on larger
machines, I believe) but they note that almost all verifications were made
in parallel with 32 cores.  So any one of the cores did the verification in
just over 150 hours -- so this might well be more than hundreds of CPU
hours on a PC.

But, again, Flyspeck is a widely cited extreme use of computation.

What kind of measures are known for the use of computation in research math?

Colin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160129/5af02386/attachment-0001.html>