[FOM] Talk on Formal Verification

[Timothy Y. Chow]

Ben Sherman wrote:

> I doubt that the verification of any "good" proof of a "major theorem" 
> should require excessive computation (not including dependencies).

Isn't Flyspeck an obvious example?

The q-TSPP theorem is another one.  It just won the AMS Robbins Prize so 
there is no doubt that it's a major theorem.  The amount of computation is 
not all that large but the certificates occupy about a gigabyte of disk 
space, and currently you need Mathematica to perform the verification.

Again, I agree that currently such proofs are not the norm.  But that's 
because we human beings are still novices at using computers to do math. 
I think it won't be long before the theorems that currently make people go 
"gee whiz that was a big computation---better add it to the Wikipedia 
list" will be so commonplace that we will smile at people who are 
surprised by them.

Tim