OK, I did a comprehensive computer check of both my algorithm and Lunnon's equivalent algorithm both of which conjecturally compute knight distance for bi-infinite chessboard. Result: when max(|x|, |y|)<20000, Lunnon's & my algorithms indeed are equivalent, and indeed do compute knight distance. At least the way I coded them in C [C is somewhat annoying for this since a/b returns result rounded toward zero, NOT floor(a/b)] the timings were WDS: 29.3 seconds Lunnon: 26.2 seconds (Lunnon's lemma 2 is unproven and the reason is global, its entire proof was just wrong. Sorry I can't be more specific, but if you want me to point out a specific error you have to make a specific error.) However, there seems no doubt now about correctness of the conjecture. Here is C code int fLunnon(int x, int y){ int X,Y,p,q; if(x<0){ x = -x; } if(y<0){ y = -y; } if(x<y){ X=y; Y=x; }else{ X=x; Y=y; } if(X<=2){ if(X==1 && Y==0){ return(3); } if(X==2 && Y==2){ return(4); } } p = X-Y; q = p-Y; if(q<0){ return( p + 2*( (q%3!=0) - q/3 ) ); } return( p - 2*(q/4) ); } int g(int x, int y){ int b,c; b = f(x-2,y-1); c = f(x-1,y-2); if(c<b){ b=c; } c = f(x+2,y-1); if(c<b){ b=c; } c = f(x+1,y-2); if(c<b){ b=c; } c = f(x+2,y+1); if(c<b){ b=c; } c = f(x+1,y+2); if(c<b){ b=c; } c = f(x-2,y+1); if(c<b){ b=c; } c = f(x-1,y+2); if(c<b){ b=c; } return( f(x,y) - b ); } TO PROVE: g(x,y)=1 unless x=y=0, then g(0,0)=-1.