[FOM] Talk on Formal Verification

[Timothy Y. Chow]

On Fri, 29 Jan 2016, Colin McLarty 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.

My statement wasn't intended to be an empirical claim about the current 
mathematical literature.  Rather, I was exhorting readers to "get with the 
times" and realize that thinking of "semiformal proofs" as being a few 
hundred pages of handwritten text is 19th-century thinking.  I agree that 
we haven't yet reached the stage where proofs of the type that I described 
outnumber 19th-century-type proofs, but IMO it's only a matter of time 
before we start really coming to grips with what computers can do for us. 
When that happens, 19th-century mathematics may look as quaint to us as 
Roman numerals, and Flyspeck will be a mere flyspeck in a grand tapestry 
of mathematics that has been built by a community of reasoners for which 
100 CPU-hours of logical inferences are almost like a single step of 
reasoning is today.

Even if you don't think this will happen, the point is that this sort of 
thing could happen, and we are already witnessing baby examples of it like 
the proof that checkers is a draw.  If we are envisaging (say) a 
22nd-century future in which all of mathematics is formalized, it should 
be all of 22nd-century mathematics that is formalized and not just all of 
19th-century mathematics.  What reason do we have to believe that in the 
22nd century, semiformal proofs will involve only negligible amounts of 
semiformal computation?  Current trends sure don't seem to suggest that.

Tim