Colombo's Determinant Problem

We completely solve Colombo’s 1928 determinant problem. For distinct real $x_1,\dots ,x_N$, $N\ge 2$, and an integer $D\ge 1$, we prove that $\det [(x_j-x_i{)}^D]\mathrm{\ne }0$ if and only if $D\ge N-1$ and either $N$ is even or $D$ is even. The even-exponent case follows from Dyn–Goodman–Micchelli (1986); the remaining odd case is proved by a strict Pfaffian sign theorem. The new odd-exponent theorem and its complete proof chain have also been formalized in Lean 4.