Here is a sketch of how to prove the knight distance formula using MAPLE9. I am not going to prove it, I am merely going to explain how somebody better than I with symbolic manip programs, could prove it. Define f := proc(x,y) local X,Y,p,q,r; X := max(abs(x), abs(y)); Y := min(abs(x), abs(y)); if(X=1 and Y=0) then return(3); fi; if(X=2 and Y=2) then return(4); fi; p := X-Y; q := p-Y; r := (7+sign(2*q+1))/2; return( p - 2*floor(q/r) ); end proc; g := (x,y) -> f(x,y) - min( f(x-2,y-1), f(x-1,y-2), f(x+2,y-1), f(x+1,y-2), f(x+2,y+1), f(x+1,y+2), f(x-2,y+1), f(x-1,y+2) ); Now TO PROVE: g(x,y)=1 unless x=y=0. See? Trivial. It is "merely" an exercise in symbolic simplification. "All" you have to do it to tell MAPLE9 to simplify g(x,y), and then you are done. Absolutely trivial. The trouble is, the MAPLE9 simplifier is way way too stupid to be able to get anywhere near being able to do this "trivial" simplification. It delivers g(x,y) = max(| x |, | y |) - min(| x |, | y |) - 2 floor(1/4 max(| x |, | y |) - 1/2 min(| x |, | y |)) - min(max(| x + 2 |, | y + 1 |) - min(| x + 2 |, | y + 1 |) - 2 floor(1/4 max(| x + 2 |, | y + 1 |) - 1/2 min(| x + 2 |, | y + 1 |)), max(| x - 2 |, | y + 1 |) - min(| x - 2 |, | y + 1 |) - 2 floor(1/4 max(| x - 2 |, | y + 1 |) - 1/2 min(| x - 2 |, | y + 1 |)), max(| x + 1 |, | y + 2 |) - min(| x + 1 |, | y + 2 |) - 2 floor(1/4 max(| x + 1 |, | y + 2 |) - 1/2 min(| x + 1 |, | y + 2 |)), max(| y - 1 |, | x + 2 |) - min(| y - 1 |, | x + 2 |) - 2 floor(1/4 max(| y - 1 |, | x + 2 |) - 1/2 min(| y - 1 |, | x + 2 |)), max(| x - 1 |, | y - 2 |) - min(| x - 1 |, | y - 2 |) - 2 floor(1/4 max(| x - 1 |, | y - 2 |) - 1/2 min(| x - 1 |, | y - 2 |)), max(| x - 1 |, | y + 2 |) - min(| x - 1 |, | y + 2 |) - 2 floor(1/4 max(| x - 1 |, | y + 2 |) - 1/2 min(| x - 1 |, | y + 2 |)), max(| y - 2 |, | x + 1 |) - min(| y - 2 |, | x + 1 |) - 2 floor(1/4 max(| y - 2 |, | x + 1 |) - 1/2 min(| y - 2 |, | x + 1 |)), max(| x - 2 |, | y - 1 |) - min(| x - 2 |, | y - 1 |) - 2 floor(1/4 max(| x - 2 |, | y - 1 |) - 1/2 min(| x - 2 |, | y - 1 |))) ok? Now we can manually help MAPLE9 try to simplify it. We would begin by dividing into cases. The most important case is assume(x>=y+3); assume(y>=3); but there are many more cases that would need to be considered as well. But let us just work on this one case in the present message. We continue with: assume(x>=6); #MAPLE9 too dumb to deduce that by itself! g(x,y); subs(max(y-2,x+1) = x+1, %); subs(max(y,x)=x, %); subs(min(y,x)=y, %); subs(max(y+2,x+1)=x+1, %); subs(min(y+2,x+1)=y+2, %); subs(min(x-2,y+1)=y+1, %); subs(max(x-2,y+1)=x-2, %); subs(max(x-1,y+2)=x-1, %); subs(min(x-1,y+2)=y+2, %); subs(max(y-1,x+2)=x+2, %); subs(min(y-1,x+2)=y-1, %); subs(max(x-1,y-2)=x-1, %); subs(min(x-1,y-2)=y-2, %); subs(min(x-2,y-1)=y-1, %); subs(max(x-2,y-1)=x-2, %); subs(max(x+2,y+1)=x+1, %); subs(min(x+2,y+1)=y+1, %); subs(min(y-2,x+1)=y-2, %); subs(max(y-2,x+1)=x+1, %); subs(max(x-2,y+1)=x-2, %); notice how I have to do almost every goddamn thing by myself because MAPLE9 is too stupid -- and now this case has been simplified down to h := (x,y) -> x-y-2*floor(1/4*x-1/2*y)-min(x+1-y-2*floor(1/3*x+1/3-2/3*y), x-1-y-2*floor(1/4*x-1/2*y),1+x-y-2* floor(3/4+1/4*x-1/2*y),1+x-y-2*floor(1/4+1/4*x-1/2*y),-1+x-y-2*floor(1/3*x-2/3*y)); Notice how MAPLE9's simplifier is so stupid it does not even realize that 1/4*x = x/4 or that -1+x = x-1. It is mind-boggling to me, the incompetence of MAPLE9's designers. But I digress. But anyhow we've got rid of all the maxes and mins except one, and still have a lot of floor functions, namely this list floor(1/4*x-1/2*y), floor(1/3*x+1/3-2/3*y), floor(1/4*x-1/2*y), floor(3/4+1/4*x-1/2*y), floor(1/4+1/4*x-1/2*y), floor(1/3*x-2/3*y), We can now subdivide our case into subcases mod 12. Specifically, there are 144 subcases depending on (x,y) mod 12. We do: for xx from 0 to 11 do for yy from 0 to 11 do print( h(xx,yy) ); od; od; at which point it prints out a long string of 1s, thus proving that h(x,y)=1 mod 12 in our case. EXCEPT actually it does not -- some of the 1s it prints are 3s. Oops. That means somewhere in the manual simplifications above, I made a typo. That is the problem with humans doing the job. Anyhow, ignoring that, at this point we would realize that h(x,y) mod 12=1 if x>=y+3>=6. Furthermore, we would then apply the grey cells to realize via a humanly done proof (or maybe computer could somehow see it, if MAPLE9 got any brains) that |h(x,y)| is upper bounded by a small constant. In fact if we went to mod 24 not mod 12 or something large enough to overwhelm that constant , it'd then become obvious that h(x,y)=1 always. The proves g(x,y), proving our theorem in our one (the main) case. we would then do the other cases such as x=y>=8, or x=y+1>=8 in the same fashion. OK? So I hope I've made it clear (a) exactly how to prove this now (b) Lunnon should see what is inadequate about his "proof", (c) what is inadequate about MAPLE9 simplifier ... this whole proof would have been a triviality if it had a good simplifier. But designing a good simplifier, evidently is not a trivial matter. There are many simplification tasks which are Turing undecidable (diophantine equations). I just find it interesting that the knight distance problem, which on the surface seems so trivial, leads us into utter simplification hell trying to prove it. By the way, if you can do this, then you should also do the (A,B)knight as opposed to the usual (2,1)knight used in chess.