[FOM] Formally verifying "checkers is a draw"

[Josef Urban]

On Mon, Aug 4, 2014 at 3:54 AM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:

>
>
> 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.

I do not think anybody argues that computer verification gives a 100%
certainty. See for example Section 3 ("Issues of Trust") of Hales's
"Mathematics in the Age of the Turing Machine"
(http://arxiv.org/abs/1302.2898). Real computers are physical devices
- in the quantum world anything can happen with a sufficiently low
probability and avoiding/correcting hardware errors during long
computations is probably an interesting science.

It feels good that the debate is no longer just "is computer-verified
math possible/useful/practical at all?", but also "how safe it really
can be?". It seems likely that "safety analysis" of various
verification approaches and systems will get more and more attention
(perhaps this is already happening). My feeling is that the chances of
a fake proof being wrongly certified by HOL Light due to a random
physical error (say alpha-particle bombardment) are very low already
today, and they get astronomically low when the verification is
repeated.

It is useful to have mechanisms that do not re-verify every proof in a
large theorem database before allowing one to work with it. But at
least the current large (open-source) projects draw enough attention
to be re-verified from scratch quite often. It may be as easy as
downloading an installation package and running "make" - compare this
to re-checking long informal proofs. And re-checking is not the only
motivation for complete re-running: having the whole network of proofs
fully computer-understandable allows interesting applications like
automated proof analysis, proof mining, proof/theory refactoring, etc.

Josef




>
>
> Tim
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom