I've kind of lost track of this thread. What exactly is the "Knight distance formula" to be proved?
--As C code, where dx=|x1-x2|, dy=|y1-y2|, bi-infinite chess board WDS's algorithm: Ki = max(dx,dy); L1 = dx+dy; if(Ki<3){ //handle exceptional cases where my formula fails if(L1==1){ return(3); } if(L1==4){ return(4); } //omit next line if bi-infinite chessboard: if( (InCorner(a) || InCorner(b)) && dx==1 && dy==1 ){ return(4); } } if(L1 & 1){ //different square colors, so KnightDist=odd F = ( 4+max(2*L1, 3*Ki) ) / 12; F *= 2; F++; //divide rounds downward }else{ //KnightDist=even F = ( 10+max(2*L1, 3*Ki) ) / 12; F *= 2; //divide rounds downward } return(F); Lunnon's equivalent algorithm: if(dx<dy){ X=dy; Y=dx; }else{ X=dx; Y=dy; } if(X<=2){ if(X==1 && Y==0){ return(3); } if(X==2 && Y==2){ return(4); } //omit next line if bi-infinite chessboard: if( (InCorner(a) || InCorner(b)) && X==1 && Y==1 ){ return(4); } } p = X-Y; q = p-Y; if(q<0){ return( p + 2*( (q%3!=0) - q/3 ) ); } return( p - 2*(q/4) ); In both cases the returned value is the minimum number of knight moves needed to reach (x2,y2) starting from (x1,y1). Current status: WDS produced a proof sketch unfortunately depending on a large but simple brute force computation. Lunnon produced a large number of incorrect proofs but now claims to have produced a valid proof which does not need any computer. But WDS still does not agree Lunnon's proof valid. Lunnon & WDS also interested in certain other questions about knight distance, such as how many shortest paths there are, but the validity of these formulas is foundational and needed before we can discuss all those other questions.