[FOM] Talk on Formal Verification

[Timothy Y. Chow]

Mario Carneiro wrote:

> The problem here is that "reasonable time" is defined on a human scale, 
> so probably in the order of seconds to minutes, but this applies 
> separately to each proof program that is written, so a large composite 
> proof like Flyspeck, involving tens of thousands of these "reasonable 
> times" adds up to something quite unreasonable. If a little extra in the 
> way of search hints was stored, this could doubtless be cut down 
> considerably. There is a tradeoff between storage space and verification 
> time here, but I think it is clear which resource is in shorter supply 
> right now.

This is a great point.  To me it indicates that the old-fashioned mindset 
that "verification is trivial" is already biting us, and that we need to 
rethink it.

One other comment I have, which I mentioned when I brought up checkers 
before on FOM, is that proofs that involve analyzing games tend to be much 
less amenable to the kind of time-space tradeoff that Mario mentions.  We 
can think of this as the difference between the classes NP and PSPACE. 
Now, the theorem that checkers is a draw is not very interesting from the 
point of view of mainstream mathematics, but I can easily imagine someone 
one day coming up with a proof that requires the detailed analysis of a 
large game (an Ehrenfeucht-Fraisse game perhaps?) and that there's just no 
way to cut down the exponential exploration of the game tree to a 
polynomial computation.

Tim