[FOM] Checkers is a draw
Timothy Y. Chow
tchow at alum.mit.edu
Mon Jul 23 09:53:25 EDT 2007
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.).
More information about the FOM