Colombo's Determinant Problem

Abstract

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]\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.

16 pages, no figures. Lean 4 formalization: https://github.com/hkjtsgmc79-boop/colombo-odd-lean. Revised from the 18 Aug 2026 Zenodo deposit, which already contained the strict Pfaffian sign theorem and proof: https://doi.org/10.5281/zenodo.21993537. A separate proof of the odd-exponent branch appeared later as arXiv:2608.28274 (28 Aug 2026)