It is shown that the smallest possible distance between two disjoint lattice
polytopes contained in the cube $[0,k]^3$ is exactly $$
\frac{1}{\sqrt{2(2k^2-4k+5)(2k^2-2k+1)}} $$ for every integer $k$ at least $4$.
The proof relies on modeling this as a minimization problem over a subset of
the lattice points in the hypercube $[-k,k]^9$. A precise characterization of
this subset allows to reduce the problem to computing the roots of a finite
number of degree at most $4$ polynomials, which is done using symbolic
computation.