[FOM] Formally verifying "checkers is a draw"
Timothy Y. Chow
tchow at alum.mit.edu
Fri Aug 1 22:12:33 EDT 2014
This is a topic that I have briefly touched on before on FOM, but I want
to pose some more targeted questions, directed at FOM readers who are
knowledgeable about formal verification.
Some years ago, Schaeffer et al. announced that checkers (a.k.a. draughts)
on an 8x8 board is a draw.
http://webdocs.cs.ualberta.ca/~chinook/publications/solving_checkers.html
Their proof was a combination of a giant endgame database and a very long
run of a sophisticated search algorithm. The question I am interested in
is what issues would arise in trying to formalize the proof of "checkers
is a draw" using one of the well-known proof assistants.
I think that many people regard proof assistants as providing additional
certainty about the correctness of an alleged proof. There seems to be a
tacit assumption that a proof may be difficult to find, and perhaps
somewhat tedious to encode using a proof assistant, but once these two
steps are complete, we will have a short certificate in hand that can be
quickly verified with a short computation using a small, carefully
verified piece of code.
What I suspect, however, is that in the case of theorems like "checkers
is a draw," which have a PSPACE (or worse) flavor to them, the tacit
assumption that "proofs are short" will necessarily be violated. The fact
that Schaeffer et al. combined a long computation with a large database
suggests to me that it may be practically infeasible to "write down" the
proof, even if "writing" isn't restricted to paper but includes writing to
disk. So my questions are:
1. Are current proof assistants designed so that the proof must, for the
most part, be "written down"? Or is there a lot of flexibility in trading
off certificate size and verification time, so that a formal proof of
"checkers is a draw" could be stored and verified with roughly the same
time and space requirements as Schaeffer et al.'s original proof?
2. Is there anything to my intuition that the PSPACE nature of strategy
games makes "checkers is a draw" particularly thorny for proof assistants,
or do essentially the same issues arise for any large combinatorial
calculation such as computing combinatorial designs with specific
parameters (Ramsey number calculations, nonexistence of projective planes,
etc.)?
Tim
More information about the FOM
mailing list