[FOM] Talk on Formal Verification

[Josef Urban]

On Sat, Jan 30, 2016 at 3:19 AM, Colin McLarty <colin.mclarty at case.edu> wrote:
>
>
> 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.

Right, the last verification we did on a single server (nothing too
fancy) and it took a couple of days in real time.

>
> 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?

The Flyspeck numbers might look impressive for formal math, but they
are tiny e.g. with the CPU/GPU numbers that today routinely come up
when training deep neural nets for large-scale recognition tasks. 5k
CPU hours is nothing today. Multiples of that already are and will be
used for training mathematical AI in various ways - just see the
numbers used for training the AlphaGo deep neural nets for comparison
( https://storage.googleapis.com/deepmind-data/assets/papers/deepmind-mastering-go.pdf
). Verification is cheap, intelligence is expensive :-).

Josef

>
> Colin
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>