[FOM] Formally verifying "checkers is a draw"

[Timothy Y. Chow]

On Tue, 12 Aug 2014, Josef Urban wrote:
> I think as long as (some form of) the Moore's law holds, this might not 
> be a serious issue. Compared to ten years ago, working with the largest 
> formal math libraries has become very easy - practically all of it fits 
> today in a notebook's RAM. Re-checking Flyspeck ten years from now will 
> probably cost very little.

I do expect that Flyspeck will cost very little ten years from now. 
However, I don't think that that's the right way to think about the 
question.  If your vision (and Dana's vision?) of computer-assisted math 
is realized, then I expect that computers will start automatically 
generating proofs of results whose verification effort will dwarf that of 
Flyspeck or even "checkers is a draw."  No matter how powerful our 
computers get, we'll probably push them to the limits of our own patience.

Bas Spitters remarked, "It is not clear to me that there are many 
naturally occurring co-NP-hard results."  I think that there are a lot of 
them lying around but we just haven't drawn attention to them.  It is 
common, for example, to see an assertion along the following lines in a 
mathematical paper: "We conjecture that P(n) is true for all n.  We have 
verified that P(n) is true for n <= 26."  If P(n) is co-NP-hard then this 
throwaway comment in the paper may represent large amount of computation. 
Many combinatorial non-existence results have a co-NP-hard flavor even if 
they are not officially co-NP-hard.

Now, you might respond that these sorts of finite computations merely 
provide supporting evidence for interesting conjectures and are not 
themselves interesting enough to embed into some standard library of known 
math.  After all, we don't do more than include a throwaway comment today, 
so why would that practice change?

Many finite computations might be uninteresting, but it is not hard to 
imagine that there might be many interesting theorems whose proofs reduce 
to a finite computation.  A full proof of the interesting theorem might 
need to include the full verification of P(n) for all n <= 26.  Indeed, 
the Kepler conjecture is basically an example of this phenomenon.  A very 
high-level summary of the proof is that Fejes Toth reduced the conjecture 
to a large finite computation, which was then carried out.  My expectation 
is that this sort of thing is only going to increase in the future.  It 
won't be just one high-profile project that takes months of computation; 
everybody will be generating theorems whose proofs take days (or more) to 
verify with whatever machines are available.  And naturally, we will be 
more interested in using our CPU-days finding new theorems rather than 
re-verifying last week's theorems.

Tim