[FOM] Formally verifying "checkers is a draw"

[Timothy Y. Chow]

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