[FOM] Checkers is a draw

[Timothy Y. Chow]

On Sun, 22 Jul 2007, joeshipman at aol.com wrote:
> How large is the database storing this proof?

I don't know, but it shouldn't be too hard to do a back-of-the-envelope 
estimate.  Or you could email Schaeffer directly if you really care.

> This is a good example of a kind of interactive proof not typically 
> treated formally -- although the database itself can be converted to a 
> real formal proof whose size is probably measured in hundreds of 
> terabytes, and so is not "humanly feasible" to check, the applet which 
> allows you to play against the database is a sort of interactive proof 
> that would convince a world-class grandmaster in a humanly feasible 
> amount of time, but would not convince an ordinary checker player.

It would convince a world-class grandmaster that Chinook is an extremely 
strong player, but it would not necessarily convince said grandmaster that 
Chinook is a *perfect* player.

For that, the proof would have to be encoded as a special error-correcting 
code, so that any error in the proof would be "amplified," allowing its 
detection (with high probability) with a feasible number of queries.

Anyway, as I was arguing a month or two ago, "checkers is a draw" is the 
prototype of a theorem that may pose a challenge to the traditional 
viewpoint of formal verification (the QED Project, etc.).

Tim