[FOM] Formally verifying "checkers is a draw"

[Bas Spitters]

Dear Tim,

Flyspeck just finished, taking 5000h of computation time.
https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion
http://afp.sourceforge.net/devel-entries/Flyspeck-Tame.shtml

Tom Hales has been advertising this page:
https://en.wikipedia.org/wiki/List_of_long_proofs
It seems that checkers could be added there.

It is not clear to me that there are many naturally occurring
co-NP-hard results.
I don't recall anyone mentioning this before, so, if correct, it could
be a new insight.
Just add these co-NP-hard proofs to the above mentioned wikipedia page.

Best,

Bas

On Mon, Aug 4, 2014 at 3:54 AM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> Thanks to all who responded.  I learned several interesting things from this
> discussion.
>
> 1. By email, someone told me that Flyspeck is in the home stretch and is
> estimated to take about 10,000 CPU hours.
>
>
> https://www.youtube.com/watch?v=DJx8bFQbHsA&index=3&list=PL9kd4mpdvWcCUOrG5S7KrvOFDhyqnXoUj
> (at approx 33 min).
>
> Someone else emailed me with a pointer to another highly computational
> proof, related to the Erdos discrepancy problem.
>
> http://arxiv.org/pdf/1402.2184v1.pdf
>
> Near the end of the paper, the authors suggest that the proof "is probably
> one of the longest proofs of a non-trivial mathematical result ever
> produced."  A quick glance suggests that it is somewhat smaller than
> "checkers is a draw," but perhaps the authors would not consider the latter
> a "non-trivial mathematical result."
>
> 2. The fact that checkers has a PSPACE flavor is probably not directly
> relevant, but it *does* seem to be relevant that there are interesting
> mathematical theorems whose proofs do not seem to fall into the "NP
> paradigm."  By the "NP paradigm," I mean the idea that the proof of an
> interesting mathematical theorem might take a lot of effort to discover, but
> the verification of the proof (once discovered) should take exponentially
> less effort.  Something like "checkers is a draw" or "such-and-such a
> combinatorial structure does *not* exist" seem to have the property that the
> effort involved in verifying a proof is comparable to the effort required to
> discover it.  The effort may be reduced somewhat by storing a (partial or
> full) certificate, but it will still be laborious because there may not
> exist an exponentially succinct certificate.
>
> What this fact suggests to me is this.  We can expect the database of
> formally verified mathematics to keep growing in the near future.  If
> "co-NP-hard" results proliferate, then there will be strong pressure to
> structure the database in such a way that the results will *not* be
> re-verified every time the database is loaded up, because that will just be
> too computationally expensive.  No matter how this is done, it seems to me
> that the door is opened to new errors creeping in.  For example, a theorem
> might be marked as proved, and then later accidentally altered. If it is not
> re-checked, the error could sit around for a long time undetected.  Even if
> the core of the proof assistant is perfectly correct, and executes perfectly
> every time it is run, the database could still accumulate errors in this
> manner.
>
> Perhaps all this is obvious to the experts, but as an interested bystander,
> I have gotten the impression that formally verified mathematics is sometimes
> touted as satisfactorily solving the problem of accumulated errors in the
> corpus of known mathematics.  There is no doubt that the project of formally
> verifying mathematics, if successfully carried out, will dramatically reduce
> the occurrence of erroneous proofs.  However, if my observations above are
> correct, and co-NP-hard results proliferate, then the problem of errors
> creeping in undetected because nobody wants to expend the effort to check
> them again will not entirely go away.
>
>
> Tim
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom