Solving Chess Kickstarter

[syzygy]

The keyword here was "proof". "proof" doesn't mean 99.9% certain. it means 100.000%

What you refer to is generally called a "mathematical proof".

Second, 99.9% is too low indeed (and so is 100.000% for that matter), and that level is not what we're talking about. The heuristic failures you refer to don't have the confidence levels referred to either, so we can dismiss those example on those grounds.

If it were feasible to store the proof tree / verification tree, then it would be a mathematical proof that can be verified by hand (or, preferably, by computer).

But again, 30^60 is a very modest lowerbound for such a proof tree. Not feasible.

The proof tree for checkers has been stored and (I believe) can be downloaded. At least in theory everybody can therefore verify the correctness. More mathematical certainty than that you will never get.

For most theorems in ordinary mathematics the situation is considerably worse: the proofs are far from complete (i.e. leave a lot to the human reader to fill in) and have not been formalised in a way that a computer can verify them.

Schaeffer's proof consists of:
- a tree from the root to middlegame positions;
- a set of endgame databases;
- a solver program that can make the step from each middlegame position to the endgame databases.

And I will repeat once more. To find a proof there is no need to do an exhaustive search over all possible moves in all positions. I have been extremely clear in stating that finding a proof is not the same as proving that a proof cannot be found (but of course this subtlety will continue to get lost on Bob).

[Uri Blass]

The keyword here was "proof". "proof" doesn't mean 99.9% certain. it means 100.000%

What you refer to is generally called a "mathematical proof".

Second, 99.9% is too low indeed (and so is 100.000% for that matter), and that level is not what we're talking about. The heuristic failures you refer to don't have the confidence levels referred to either, so we can dismiss those example on those grounds.

If it were feasible to store the proof tree / verification tree, then it would be a mathematical proof that can be verified by hand (or, preferably, by computer).

But again, 30^60 is a very modest lowerbound for such a proof tree. Not feasible.

The proof tree for checkers has been stored and (I believe) can be downloaded. At least in theory everybody can therefore verify the correctness. More mathematical certainty than that you will never get.

For most theorems in ordinary mathematics the situation is considerably worse: the proofs are far from complete (i.e. leave a lot to the human reader to fill in) and have not been formalised in a way that a computer can verify them.

Schaeffer's proof consists of:
- a tree from the root to middlegame positions;
- a set of endgame databases;
- a solver program that can make the step from each middlegame position to the endgame databases.

And I will repeat once more. To find a proof there is no need to do an exhaustive search over all possible moves in all positions. I have been extremely clear in stating that finding a proof is not the same as proving that a proof cannot be found (but of course this subtlety will continue to get lost on Bob).

I do not agree that 30^60 is a very modest lower bound for a proof tree.
There is clearly less than 30^60 legal position in chess and every tree with 30^60 positions must have the same position many times in non leaf nodes so it is possible to make the tree shorter by tranposition tables even if I consider the 50 move rule because the same position may have only 100 options for distance to draw by the 50 move rule and multiplying the number by 100 is not going to do it bigger than 30^60.

Note that it is possible to ignore draw by repetition for the proof tree because if you can force a draw by repetition you can also force a draw by the 50 move rule except positions when the opponent made a mistake in winning position that allow you to claim a draw by repetition when you know that you lose if you do not claim a draw and these positions are not relevant for solving chess.

[duncan]

Yes. Until it is proven with an exhaustive search.

also black opening position without a queen you cannot be CERTAIN black cannot win. ?

I gave this to crafty for 5 minutes. did not find a mate. Tried self play with stockfish, gets mate in 13.

rnbqkbnr/pppppppp/8/8/8/8/PPPPPPPP/4K3 w kq - 0 1

[bob]

The keyword here was "proof". "proof" doesn't mean 99.9% certain. it means 100.000%

What you refer to is generally called a "mathematical proof".

Second, 99.9% is too low indeed (and so is 100.000% for that matter), and that level is not what we're talking about. The heuristic failures you refer to don't have the confidence levels referred to either, so we can dismiss those example on those grounds.

If it were feasible to store the proof tree / verification tree, then it would be a mathematical proof that can be verified by hand (or, preferably, by computer).

But again, 30^60 is a very modest lowerbound for such a proof tree. Not feasible.

The proof tree for checkers has been stored and (I believe) can be downloaded. At least in theory everybody can therefore verify the correctness. More mathematical certainty than that you will never get.

For most theorems in ordinary mathematics the situation is considerably worse: the proofs are far from complete (i.e. leave a lot to the human reader to fill in) and have not been formalised in a way that a computer can verify them.

Schaeffer's proof consists of:
- a tree from the root to middlegame positions;
- a set of endgame databases;
- a solver program that can make the step from each middlegame position to the endgame databases.

And I will repeat once more. To find a proof there is no need to do an exhaustive search over all possible moves in all positions. I have been extremely clear in stating that finding a proof is not the same as proving that a proof cannot be found (but of course this subtlety will continue to get lost on Bob).

Nothing was lost on me. I simply pointed out that assuming Qh5 loses is bogus. Until it is PROVEN to lose, nobody knows. So, to prove Qh5 loses, you MUST do an exhaustive search for that side, so that for any possible move at any possible depth, you prove those moves lead to a loss. No particular requirement for the other side to look at all moves, unless the goal is to find the shortest win for that side, so just one winning move (leading to mate in this case) is good enough.

[bob]

Yes. Until it is proven with an exhaustive search.

also black opening position without a queen you cannot be CERTAIN black cannot win. ?

I gave this to crafty for 5 minutes. did not find a mate. Tried self play with stockfish, gets mate in 13.

rnbqkbnr/pppppppp/8/8/8/8/PPPPPPPP/4K3 w kq - 0 1

You can't be certain until you prove every black move leads to a mate for white. That is a challenge. self-play proves exactly nothing due to pruning and searching too shallow.

[Brunetti]

You can't be certain until you prove every black move leads to a mate for white. That is a challenge. self-play proves exactly nothing due to pruning and searching too shallow.

Well, I think chess is not mathematics or another complex science: we can rely on centuries of experience, logic and also good sense and intuition. Duncan's position _is_ a certain win, I don't think it's necessary to prove it by brute force, we don't need a scientific proof for obvious facts like that. E.g., there's no need for TB's (or other exhaustive analysis) to assess K+R vs K, or KRR vs KP, KQRR vs KPP and so on.
The Qh5 example is different, I agree.

Alex

[duncan]

You can't be certain until you prove every black move leads to a mate for white.

so there is a tiny possibility that being black is an advantage/white is a disadvantage which will compensate for black's loss of a queen ?

That is a challenge. self-play proves exactly nothing due to pruning and searching too shallow.

are there any chess programs available which have a mode where there is no pruning done, allowing certainty of proof ?

[bob]

You can't be certain until you prove every black move leads to a mate for white.

so there is a tiny possibility that being black is an advantage/white is a disadvantage which will compensate for black's loss of a queen ?

That is a challenge. self-play proves exactly nothing due to pruning and searching too shallow.

are there any chess programs available which have a mode where there is no pruning done, allowing certainty of proof ?

First, as far as the queen goes, it is likely a loss. But until it is proven, it is just an assumption. As to any advantage for white/black, I don't think that would be the issue. If anything, it would be black's knight ending up at h5 probably. But if you think about it, how many games have been won by an unexpected/non-obvious queen-sac? Winning is doubtful in the given position, but only a MAJOR search would prove it is not possible.

Chest is very good for mates, but you are not going to find very deep mates since it is a difficult problem to solve. I would assume most engines let you turn off pruning. In Crafty, for example, reductions, pruning and null-move can be disabled by the user if wanted. It will be very slow to reach any reasonable depth, however.

[duncan]

First, as far as the queen goes, it is likely a loss. But until it is proven, it is just an assumption. As to any advantage for white/black, I don't think that would be the issue. If anything, it would be black's knight ending up at h5 probably.

I meant what would be black's advantage to win in this position ?

[d]rnb1kbnr/pppppppp/8/8/8/8/PPPPPPPP/RNBQKBNR w KQkq - 0 1

In Crafty, for example, reductions, pruning and null-move can be disabled by the user if wanted. It will be very slow to reach any reasonable depth, however.

how would do you do it with crafty in winboard?

[duncan]

Duncan's position _is_ a certain win, I don't think it's necessary to prove it by brute force, we don't need a scientific proof for obvious facts like that. E.g., there's no need for TB's (or other exhaustive analysis) to assess K+R vs K, or KRR vs KP, KQRR vs KPP and so on.
The Qh5 example is different, I agree.

Alex

does one need exhaustive analysis to assess this position ?

[d]rnbqkb1r/pppppppp/8/8/8/8/PPPPPPPP/4K3 b kq - 0 1