Canadian Cutting Edge Science

Jonathan Schaeffer - waiting for the solution

From Canada.com (where you can play tunes on their musical navigation buttons) comes this announcement: Canadian scientists crack Checkers code:

A team of scientists at the University of Alberta has reached a milestone in artificial intelligence by using computers to 'solve' the game of checkers.
---
To solve the game, the team had to sift through an astronomical number of checkers positions and analyse the best way to move the pieces. Almost continuously since 1989, dozens of computers have been working on the problem, constantly updating Chinook's database with more and more positions.

Seems like a funny problem to put all those computers to work on for years, but the Canuck accomplishment is an excellent example of an inelegant proof. Checkers actually presents more of a geometry problem than a scientific method problem inasmuch as its solution can be posed as a theorem susceptible of proof. A theorem whose proof is inherently inelegant is anathema to both geometers and scientists. A really inelegant proof is one that the mind cannot grasp. In this case, banks of computers working day and night is what it took to grasp the solution.

The first case of such an inelegant proof the old feeder remembers was the computerized solution of the infamous Four Color Map Problem. It has been known since men started to make maps that no more than four colors were needed to keep two contiguous countries from sharing the same color. No matter how many times cats set ink to paper to try to refute this theorem, four colors was all that was ever required. But nobody could say why.

After a number of attempted 'elegant' proofs to the four color theorem were propounded and later shown to be inadequate, computers were invented and set to work finding the solution. Its an interesting story.

The four color theorem was the first major theorem to be proven using a computer, and the proof is not accepted by all mathematicians because it would be unfeasible for a human to verify by hand (see computer-assisted proof). Ultimately, in order to believe the proof, one has to have faith in the correctness of the compiler and hardware executing the program used for the proof.

The perceived lack of mathematical elegance by the general mathematical community was another factor, and to paraphrase comments of the time, "a good mathematical proof is like a poem—this is a telephone directory!"

If you can't grasp a solution with your mind, then maybe its no good? Like everyone else caught up in this philosophical conundrum, I'm not sure. Nobody has come up with a fundamental proof of the gravitational effect that I can wrap my head around, either, but I'm still going to count on gravity to keep my stuff where I put it.
---
Beware of Canuck checkers hustlers.