Learned of The angel problem of John Horton Conway.
Here's a rephrasing of the problem, perhaps easier to understand than the one given in Wikipedia:
On a chess board of infinite size, suppose we place a king. 2 players, called angel and devil, take turns.
When it's angel's turn, he can move the king 2 times. When it is devil's turn, he can delete one square at any place. When a square is deleted, the king/angel will not be able to land on it.
If the devil can delete enough squares, such that it completely surrounds the angel, and is more than 2 steps thick, so that the angel cannot get out, the angel loses. Else the angel win.
The above is called 2-angel problem, because the angel can move 2 steps in each turn. If the angel can move n steps in each turn, that problem is called n-angel problem. Note that when the angel makes a move, she can pass thru the deleted square, just can't land on it. So, in a n-angel problem, it is not enough for the devil to circle the angel with deleted squares, but the “wall” must be n-thick.
At first i don't quite understand the problem, but in trying to understand it, it grew on me. Not a trivial problem at all. (Conway is the one who created the “Game of Life” cellular automata.)
Be sure to read the original paper by John H Conway: The Angel problem (PDF)
Apparently, it is not easy to prove that angel can win even if the angel can make 1000 steps in each turn. ⁖ the 1000-angel problem. But it seems that the angel can win for n greater than 1. This is solved, proven, in 2006. However, as implied in Wikipedia, a explicit optimal strategy for the angel is not known.
One thing i wonder about these type of problems is that, how to create a model of it in mathematical logic? More specifically, how to turn this problem into a question with Formal language. For ease of explanation, let's focus on the specific 2-angel case. So, when turned into a formal language equivalent, the question would be something like whether a particular string is possible with a given formal language.
I suspect that the process of turning such a problem as formal language problem, lots insights can be gained, though am not sure it helps deriving solutions.
When this problem is modeled as a formal language, it may become convoluted and difficult to understand. However, i think it actually makes the problem the most simple, because it condenses the problem into its logical gist. And this is why, that many math problems that are simple to state that even a child can understand the question, yet are most difficult to solve. (⁖ many number theory problems and problems in recreational math) But really, when turned into its math gist, as a logic problem, in formal language, of a bunch of strings and transformation rules, and asking whether a given string is possible, one can see that these “simple” problems are not simple to begin with, their real nature appears.
Back to the 2-angel problem. Another interesting thing is how to represent the concept of optimal strategy in terms of a question in formal language? I have no idea… but i think it be represented as generating a particular shortest or longest string, of particular pattern. Or, perhaps the least number of steps to arrive at a given string.
To get started in this… i think it would be fruitful to start with a simple similar problem. Say, suppose you have a chess board, and the question is, is it possible to lay 3 pieces so that they form a line (horizontally or vertically)? Of course, this is trivial and even idiotic a question. Our job, is to formulate a equivalent problem in formal language. This way we'll learn what is involved.