Checkers is mostly solved

The NY Times reports:

Jonathan Schaeffer, a professor of computer science at the University of Alberta, set out on his checkers-playing quest in 1989, aiming to write software that could challenge the world checkers champion. He and his colleagues finished their computations 18 years later, in April.

"From my point of view, thank god it's over," Dr. Schaeffer said.

Even with the advances in computers over the past two decades, it is still impossible, in practical terms, to compute moves for all 500 billion billion board positions. Instead, the researchers took the usual starting position and then looked only at the positions that would occur during the normal course of play.

"It's a computational proof," Dr. Schaeffer said. "It's certainly not a formal mathematical proof."

Then it is not a proof at all. A proper computational proof would have examined all the possibilities, and proved that those really were all the possibilities. It appears that Schaeffer just computed end-game scenarios for some list of likely positions, and didn't prove anything at all about the other positions.

That is not a proof.

Here is another description of what they did:

The Alberta researchers exhaustively checked the final stages of play for any arrangement of 10 pieces or less, identifying which of the 3.9 x 10¹³ positions won, lost or drew.

Next they identified 19 representative opening sequences and searched through subsequent moves for the easiest-to-find connections to final positions—win, lose or draw. To save time, they ignored pointless back-and-forth moves or those that did not turn a draw into a win.

This doesn't sound like a proof to me.