Talk:Imo 2009 q6
It seems to me that proof #1 says 'let's make as much progress as possible', and by working with sets of partial paths extends the counting approach used in proof #2 case 4 to do more work. It might generalise more easily eg in more dimensions, where the blocking sets might be more complex, and working back from the end might not be so easy to achieve nicely. Proof #2 has been converted into an algorithm and programmed in Mathematica (unchecked by me) [1] by jc, whereas proof #1 is non constructive. Proof #1 gives no special status to the longest leap.
The discussion on the Mathlinks Math Forum here [2] has another proof a bit similar to #2 where the inductive step is to remove the mine closest to the beginning (the proof by qwerty414 as stated has it at the end) and to look at two cases: the first where doing the longest leap first lands on one of the remaining mines, and the second where it doesn't. This seems to reduce the number of cases, but the argument is not quite so straightforward.