Can one make high-level proofs about chess positions?

Question

I realize this question is risky (as the title and the tags indicate), but hopefully I can make it acceptable. If not, and the question cannot be salvaged, I'm sorry and ready to delete it or accept closure.

Oftentimes, when one listens to chess grandmasters commentating on games, they will say things like, "The engines give a +1 advantage to White, but the postion is dead-drawn." And they proceed to provide high-level explanations of such statements. I'm a bad chess player so I cannot really attempt to verify those, but they often sound extremely convincing. Also, when they teach simple endgames, they seem to consider analyzing the crucial ideas to be enough for proof (at least in the sense of "a completely convincing explanation") and it's difficult not to agree with that. Even certain positions with a lot of pieces on the board can apparently be treated this way. "There is no way to make progress" is something that one can frequently hear.

Sometimes these just turn out to be wrong. These statements are generally based on intuitions ("axioms") such as "you cannot give away your queen for a pawn", which are believed to be true in almost all situations and on already analyzed positions (like the Lucena position). The grandmasters' intuitions are very fine, but it can happen that they will miss a counterintuitive material sacrifice, a counterintuitive retreat or a counterintuitive something else. However, they can be extremely convincing sometimes (and never proven wrong).

It's clear that chess can't be solved this way any time soon. A clear obstacle is the "wild" or "unclear" positions, where "anything can happen". But there are also those "tame" positions, "dead-drawn" positions and "winning advantages". (Surely, some -- or maybe a lot -- of these statements are not correct or correct with incorrect reasonings behind them.) Another indication is that the humans who make these statements get beaten by computers, which primarily use low-level tree searches.

My question is how much, if anything, of this high-level reasoning can be put to a form that would make it mathematics and mathematical proof. I think brute force is clearly not the only way of evaluating positions rigorously. In a K+Q v. K endgame, one doesn't have to analyze each possible move of the lone king to show that it's doomed. It's enough to show that a stalemate is impossible when the king is not on the side of the board, that the king can be forced to the side of the board and then that whenever the king is on the side, it can be checkmated. For a rigorous proof, one can use all kinds of symmetries and translations without having to go through every single node of the tree.

The question

How much of that high-level thinking grandmasters employ can be made into mathematics?

is what I'm interested in, but this is vague -- it's not clear what "how much", "high-level thinking" or even "made into" mean. But I think people must have tried to pursue this and some clear mathematical statements must have been produced. If not, is it at least possible to say why it's difficult, infeasible or impossible?

Is there a chess position with a large (enough to be intractable to a human with just a pen and a piece of paper) tree that has been solved without brute-forcing the tree? Has a rigorous proof accessible to a human been produced?

Answer 1

Let me prove, for example, that the following 7-piece position is a draw. 7-piece positions are about the borderline of what's doable by brute force: they were tabulated around 2010.

Black draws as follows:

1) if white queen captures the rook or the pawn, recapture.

2) else, in the event of check, move the king to h7, h8, or g8 (cannot all be controlled by the queen simultaneously)

3) else, if white queen or pawn moves to 6-th rank, capture it with the rook,

4) else, move the rook to f6 or h6.

Clearly, unless white sacrifices the queen, she cannot cross the 6-th rank with the king and thus cannot break the above routine. The possible sacrifices are:

A) by capturing the g7 pawn. Recapture with the king and continue moving the rook, securing a draw.

B) by taking the rook. Any resulting pawn endgame is drawn by moving the king between h7, h8, and g8;

C) by Qa6, Qb6, Qc6, Qd6 or Qe6, followed by rook takes queen and king takes rook. The very same idea, only be sure to take g7:h6 when you can.

D) By Qg6 R:g6 h5:g6. This is also a theoretical draw. Move Kh8-h7-h8-... and be sure not to take g7:h6 at a wrong moment.

Some details are left off here, but I think the level of rigour is fairly close to how math is written.

P. S. In a game between Mamedyarov and Caruana (world N17 and N3, respectively), played last Friday, a draw was agreed in the following position:

Computers wrongly give a decisive advantage to white: the idea of cutting the king with the rook is too "high-level" for them to understand it. And I believe, if needed, one can devise a rigorous proof here similar to the one above.

Answer 2

It's not chess, but you might like the book "Mathematical Go: Chilling gets the Last Point" by Berlekamp and Wolfe, about mathematical analysis of Go endgames. IIRC they used transfinite (or was it infinitesimal) surreal numbers to study Go endgame positions that Go experts thought were always drawn, and found wins in some of them, with the winning methods understandable and usable by human players once the mathematicians had found and published them.

Answer 3

See Bleicher's "Freezer" that is a human/computer interactive proof agent: you make the "rules", and it iterates over positions. (The article from 2004 is rather old, and the given examples are solvable by brute means by now.)

Probably one can write the simplest endgames (KQ vs K and KR vs K) as induction proofs, in a manner so that they will work on bigger boards. For KBN vs K, you can proceed by "reduction" of classes of positions (say based upon opponent's king location), similar to solving a puzzle like Rubik's Cube (the KBN vs K has even been done for Kriegspiel by Ferguson).

Fortress draws are classical examples of "high-level proofs", with the KQ vs KRP example from Philidor (1777) one of the earlier ones (WQd4, WKf5, BKe8, BRe6, BPd7, though if everything is shifted a rank down, then White can spruce the Black king out, force it to d5 to stop the Re5-c5 oscillation, and win), and the above example is a 7-piece variant of this. General-purpose computer programs are well-known to do poorly in solving fortress problems, as the Behting study previously demonstrated. However, there are still some problems that computers "can't solve" (without some additional methods), and a more subtle fortress example is this study by Chekhover (1947):

7r/p3k3/2p5/1pPp4/3P4/PP4P1/3P1PB1/2K5 w - - 0 1

White to move and draw. The "natural" moves (as proposed by the computer) will lose, as though White has three pawns for the exchange, this will not avail him much when the rook's activity becomes clear. But rather 1. Kd1 Rh2 2. Ke2 (or Ke1) Rxg2 3. Kf1 Rh2 4. Kg1 Rh3 5. Kg2 Rh8 6. f3, and Black can never invade, White shuffling the king between f1/f2/g1/g2 and blocking the queenside pawns as necessary. (Also to note, is that the sacrifice Re4 by Black does not work, and likely loses.)

For the second question, by now there exist a (large) number of studies whose first X moves are tricky enough so that brute force by computer is not immediately feasible, but whose last Y moves are not very understandable to humans, being just a "random" tablebase position that happens to give the desired result.

Answer 4

Some examples do exist but they're rare. One category that has not been mentioned so far is the application of combinatorial game theory to chess.

There is a heuristic argument that proofs in chess cannot usually be compressed much. Namely, Fraenkel and Lichtenstein have proved that chess is EXPTIME-complete. Of course, this is an asymptotic result and does not rigorously imply anything about chess on an $8\times 8$ board. Nevertheless, when we examine endgame tablebases, the impression one gets is that they are extremely hard to compress. John Nunn has written some books (e.g., Secrets of Rook Endings) trying hard to make the results of these endgame calculations comprehensible to a human, but a glance at his books shows that there is still an overwhelming amount of explicit memorization required if you really want to play these endings perfectly. If this is indeed the situation with such "simple" chess positions, the prospect of short proofs for complex positions looks pretty dim.

As a thought experiment, consider the opening position with White's queen removed (i.e., White is giving Black queen odds). "Obviously" this is a win for Black. But can we prove it mathematically? No. Now, typical grandmaster analyses will conclude "Black wins" with much less of an advantage than this. So if we can't convert "Black wins with queen odds" into a mathematical proof then we surely can't convert very many grandmaster analyses into mathematical proofs.

Answer 5

Although somewhat orthogonal to the thrust of the question (determining a winning strategy for a giving legal position in chess), I think the title question is in part answered by Raymond Smullyan.

Raymond Smullyan has written much to make topics in logic more accessible. In addition, he has exemplified logical reasoning in chess with his popular books on retrograde analysis, including Chess Mysteries of Sherlock Holmes. Here the goal often is to determine how a position was arrived at, along with certain properties like whether castling is legal. I would recommend his titles to anyone wanting to practice mathematics, especially as related to chess.

Gerhard "Has Arabian Nights Themes Too" Paseman, 2016.02.04.

Answer 6

Obvious reply that most likely wasn't made as such simply because this question was posed eight years ago: wouldn't it be an appealing exercise to give a human-readable formal proof (in Lean, Coq, etc.) that certain endgames are drawn or won? I'm thinking of "cases where the algorithm is non-trivial, and where it is clear that the arguments given in endgame textbooks (a) are conceptual rather than merely brute-force, (b) could in principle be turned into actual proofs".

It seems that there is a bitnof work on this issues, but more along the lines of "formally verify brute-force databases on K v. K and Q/R/B/N endings". I'm thinking more along the lines of the Lucena or Philidor position, say.

(For perspective: eight years ago, proving in a formal proof system that the sieve of Eratosthenes always gives correct results was hard, and apparently couldn't be done in at least some systems; now it is a student project in at least one system, and something that an expert can hack overnight (in a make-do fashion) in at least another.)