Proof of KRK endgame theorem

  • #1
Summary:
Series of articles authored by Maliković, Janičić, Marić and Čubrilo demonstrate computer-aided proofs of KRK theorem, here I present pen and paper one
The articles:
https://lmcs.episciences.org/5328/pdf
http://argo.matf.bg.ac.rs/publications/2013/2013-icga-krk-sat.pdf
http://archive.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf

KRK endgame is a win for white regardless of starting position, with the trivial drawing exception in case when black moves first and is able to capture the rook, or is stalemated in the corner.
Proving that requires describing at least one winning strategy for white, and proving its correctness, either by computer aided method or by pen and paper non-computer-aided method.

Auxiliary Definition 1: two kings stand in opposition if they are on the same line two squares away.
Corollary 1: two kings in opposition prevent each other to move to three squares adjacent to both of them, ie to move to the line that separates them, and is perpendicular to the line they both stand on. Proof: trivially follows from Definition 1 and from the game rules.

Corollary 2: when king is not placed at the edge of the board, and is not constrained by other pieces, it has access to three lines parallel to the same edge, ie to three ranks and to three files. Proof: trivally follows from the game rules.

Obviously, these two are not corollaries of the main theorem, but of the game rules, they are also lemmas to main theorem, so I could have named them also that way.

Lemma 1: in KRK endgame checkmate is possible if and only if BK is at the edge of the board. Proof:
BK is checkmated if WK stands in opposition on the line perpendicular to the edge at which both BK and WR stand, with d(BK,WR)>1, if BK is in the corner, WK can also stand one square away from the previously described opposition square, two lines away from the edge at which both BK and WR stand, with Chebyshev d(WK,BK)=2.

In both cases WK denies BK access to penultimate line parallel to the edge BK stands on, in case of opposition according to Corrolary 1, and in the other case corner placement helps due to the fact that the third square not guarded by WK does not exist, and WR covers the edge. No other checkmate position is possible, because there are no other pieces that could prevent BK from accessing the third line BK would have access to, according to Corollary 2, had BK not been placed at the edge, and this proves Lemma 1.

Now, in order to prove the main theorem, one has to prove two more lemmas:
Lemma 2: in KRK endgame it is always possible to force BK to one edge
Lemma 3: in KRK endgame, if BK is constrained to one edge by WR standing on the penultimate line which is parallel to that edge and separates two kings, it is always possible to force position in which it is white to move and deliver checkmate, by achieving position described in Lemma 1.

Proof of Lemma 3:

In order to prepare that mate in 1 position, white will make three kinds of moves:
1.) decreasing Manhattan d(WK,BK), approaching with king without ever stepping onto penultimate line or into opposition

2.) shifting rook from one edge to another staying safe on the same penultimate line when BK threatens its capture

3.) waiting move with rook when 1.) is not possible and 2.) is not necessary, this is any move on penultimate line which does not change the ordering of pieces and keeps WR safe from capturing
It is obvious that applying 2.) white can always obtain tempo to approach with the king to a line adjacent to that which rook holds, two lines away from the edge where BK stands, from any other line further away, and to transpose to a position in which WK stands between BK and WR in terms of lines perpendicular to the edge where BK stands, although WR stands all the time between WK and BK in terms of lines parallel to that edge.

From that position, black has two choices moving king along the edge, either to increase or decrease Manhattan d(WK,BK). If it tries to increase it, white will follow with 1.), but black is limited in this strategy with the corner, if it tries to decrease it, white will either follow with 1.) if possible, or 3.) otherwise, limit to this strategy is black stepping into opposition, when white follows with checkmate, which proves Lemma 3.

In the same vein, one can prove Lemma 2, and complete the theorem:
It is always possible to place safely from capturing WR on the line that separates two kings, that conclusion is rather trivial. From there white will apply exactly the same strategy as in Lemma 3, the only difference is that instead of checkmate it will result in squeezing BK one line nearer the edge, the limit of this strategy is BK ending at the edge.

Questions:
how rigorous
how original
is this proof?
 
Last edited:

Answers and Replies

  • #2
Office_Shredder
Staff Emeritus
Science Advisor
Gold Member
4,623
630
Summary:: Series of articles authored by Maliković, Janičić, Marić and Čubrilo demonstrate computer-aided proofs of KRK theorem, here I present pen and paper one

The articles:
https://lmcs.episciences.org/5328/pdf
http://argo.matf.bg.ac.rs/publications/2013/2013-icga-krk-sat.pdf
http://archive.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf.

I'm a little worried the point is being missed here. Constructing a winning KRK checkmate is not that interesting. I think the main point of those papers is the computer aided proof technique.

Questions:
how rigorous
how original
is this proof?

Definitely not original, you just described how to do something every chess player has known how to do for a thousand years. If your goal was to practice writing a proof though, it's fine.
 
  • Like
Likes jim mcnamara, mfb and berkeman
  • #3
So, can you do the same for KBNK?
 
  • #4
Office_Shredder
Staff Emeritus
Science Advisor
Gold Member
4,623
630
So, can you do the same for KBNK?

Can I? No, because I haven't learned the pattern to get checkmate. The algorithm is known though, someone could write it out in detail and demonstrate the correctness of it. That one might be more suitable to a computer aiding the check though, since I think there are more choices you have to analyze?
 
  • #5
There are more choices even with KRK which is far more basic than KBNK, because there is more than just this one strategy which I described and, you say, demonstrated fine proof of correctness. Maliković and others use Bratko’s strategy which is far less known and understood and which leads to a decomposition of main theorem into a different set of lemmas, corresponding to different stages of strategic plan, comparing to “mine”, which you say knows every chess player, and I agree with that. What they show is definitely somewhat different, not just because of usage of computer aided techniques, for which I have no idea how you came up with the idea that I think they are not their primary focus.
Besides that, even if the strategy I described is well known, that still does not mean the proof is not original, if nobody else so far presented it the way I did, and showed the real connection between math and chess. Because, so called mathematical chess problems are rather artifical link between the two areas, they are math problems that have very little to do with chess https://en.wikipedia.org/wiki/Mathematical_chess_problem, what I showed is a chess subject presented in mathematical way. And all that chess’n math organizations, I don’t know what they actually teach, that’s why I ask, but receive a wrong answer. Could you post a link to a page where already exists a similar proof? I couldn’t find it, otherwise, I wouldn’t bother to write it by myself and ask such things.
 
  • #7
pbuk
Science Advisor
Gold Member
2,352
1,088
Besides that, even if the strategy I described is well known, that still does not mean the proof is not original, if nobody else so far presented it the way I did, and showed the real connection between math and chess.
...
what I showed is a chess subject presented in mathematical way
But your proof does not contain any mathematics, it is just a strategy written in a semi-formal language. An example of a mathematical solution to a chess problem is solving domination by queens using the properties of a Salem-Spencer set, or the methods shown in this paper on combinatorial game theory in chess endgames.

Could you post a link to a page where already exists a similar proof? I couldn’t find it, otherwise, I wouldn’t bother to write it by myself and ask such things.
I hope to find there similar proofs for other endings ...
Chess endgames were analysed long before the internet, you would do better to look in a book such as How to Play Chess Endings in the set by Znosko-Borovsky or Max Euwe's A guide to chess endings.
 
  • Like
  • Informative
Likes Delta2 and jim mcnamara
  • #8
Office_Shredder
Staff Emeritus
Science Advisor
Gold Member
4,623
630
What they show is definitely somewhat different, not just because of usage of computer aided techniques, for which I have no idea how you came up with the idea that I think they are not their primary focus.

I was giving them the benefit of the doubt. If their goal was really to prove that endgame has a checkmate solution then their paper seems pretty pointless to me.

Besides, it even says this in the first one
. One of our goals and contributions is modelling the chess rules and chess
endgames so that the correctness proofs can be made as automated, efficient and reliable as
possible.

Though to be honest, this feels like a pretty underwhelming paper anyway. If they had a really good method at the end they probably would have used it to solve something more interesting.
 
Last edited:
  • Like
Likes jim mcnamara and pbuk
  • #9
pbuk
Science Advisor
Gold Member
2,352
1,088
Though you be honest, this feels like a pretty underwhelming paper anyway.
Agreed. Here is my alternative abstract: "We use a black-box computer proof assistant to prove something that has already been proven demonstrating that (i) it is still true and (ii) we read the manual properly".

If they had a really good method at the end they probably would have used it to solve something more interesting.
Their goal is not solutions, it is merely the verification of existing solutions using 'provably correct' proof assistants. For chess this is almost worthless because all endgames have already been exhaustively analysed using demonstrably correct chess engines.

For me a more interesting, and earlier (2005) result is Gonthier's proof of the four-colour theorem using the proof assistant Coq: this removes the reliance on bespoke code in previous proofs (noting that the original 1976 proof was flawed).
 
  • #10
But your proof does not contain any mathematics, it is just a strategy written in a semi-formal language.
Yeah well, my proof was supposed to be a proof of correctness of that strategy, not the strategy itself. And that was supposed to prove the theorem (that claim that is a subject of proof, in our concrete case it says that KRK is a win for white), that was its final purpose. And what does that even mean “a proof does not contain any mathematics”? I thought it can only be the other way around: mathematics can contain certain theorems and their proofs, if they are rigorous enough to be acceptable, no? And what improvement would you suggest in order to upgrade it to a fully formal language, if I may ask? Shredder said it was fine, now you say it is only of semi quality.
An example of a mathematical solution to a chess problem is solving domination by queens
OK, I can take it, my proof is not mathematics, because mathematics is only that what mathematicians consider as such. Following that logic, this is not a chess problem. No chess professional would consider its solution very relevant for their business, because they rarely deal with more than two queens of the same color, although it may be a fine mathematical problem.
So OK, I thought it was only a question of rigorosity, not of the actual content of the theory, perhaps I was wrong.
The other paper looks interesting though, I will take a look at it, thanks.
 
  • #11
Still, I don’t see how the same theorem proven by using automated proof assistant or a constraint programming system would count as mathematics, and without it, it is not.
 
  • #12
pbuk
Science Advisor
Gold Member
2,352
1,088
Shredder said it was fine, now you say it is only of semi quality.
I did not say it was of 'semi quality', I said it was written in a semi-formal language.

And what improvement would you suggest in order to upgrade it to a fully formal language, if I may ask?
Using the language of formal proof would definitely not be an improvement. For instance
Corollary 2: when king is not placed at the edge of the board, and is not constrained by other pieces, it has access to three lines parallel to the same edge, ie to three ranks and to three files. Proof: trivally follows from the game rules.
is perfectly acceptable to anyone who understands chess, and it is reasonable to assume that anyone who is interested in this proof understands chess. However this is a long way away from the language of formal proof.

And what does that even mean “a proof does not contain any mathematics”?
Well if your proof contained something like the following we might say there was some mathematics (specifically combinatorics) in there:

there are 64 x 63 x 62 = 249,984 possible placings of KRK on a chessboard, although we can reduce this by a factor of 8 for the two reflectional and two rotational symmetries. This leaves 31,248 placings but many of these are not possible starting positions
(note this is probably NOT the best way to calculate legal starting positions for this problem!)

But this wouldn't make it a better proof, there is nothing special about mathematics, it is just a big toolbox containing things that have (mostly!) already been proved which can often help.

The other paper looks interesting though, I will take a look at it, thanks.
No problem. You might be interested in this one on formal proof too: https://cmartinez.web.wesleyan.edu/documents/FP.pdf
 
  • #13
Office_Shredder
Staff Emeritus
Science Advisor
Gold Member
4,623
630
Still, I don’t see how the same theorem proven by using automated proof assistant or a constraint programming system would count as mathematics, and without it, it is not.

I don't think anyone here thinks those papers are interesting new mathematics.

The author of the third paper
https://www.google.com/amp/s/www.researchgate.net/profile/Marko-Malikovic/amp

Is a professor of psychology? And they have a bizarre number of publications that prove correctness of KRK endgame using different tools. I'm not sure what their career is supposed to be, but it isn't in research mathematics

I haven't looked at the other authors.
 

Related Threads on Proof of KRK endgame theorem

  • Last Post
Replies
14
Views
5K
Constructive Proofs Proof of Correspondence theorem
Replies
1
Views
238
M
  • Last Post
Replies
9
Views
6K
  • Last Post
2
Replies
25
Views
15K
Replies
1
Views
750
  • Last Post
Replies
6
Views
17K
  • Last Post
Replies
10
Views
3K
  • Last Post
Replies
3
Views
1K
  • Last Post
Replies
2
Views
1K
Replies
15
Views
6K
Top