[FOM] Formally verifying "checkers is a draw"
Timothy Y. Chow
tchow at alum.mit.edu
Tue Aug 12 19:48:22 EDT 2014
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
More information about the FOM
mailing list