Papers With

← All papers
First page of Colombo's Determinant Problem

Colombo's Determinant Problem

Qianli Ma

math.NT Aug 31, 2026 · v1 math.CA
formalization algebra analysis
Read PDF arXiv abstract Code
TL;DR
The new odd-exponent strict Pfaffian sign theorem and its complete proof chain are formalized in Lean 4.
Abstract
We completely solve Colombo's 1928 determinant problem. For distinct real $x_1,\ldots,x_N$, $N\geq 2$, and an integer $D\geq 1$, we prove that $\det[(x_j-x_i)^D]\neq 0$ if and only if $D\geq 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.
Problem

Colombo's 1928 determinant problem asks when det[(x_j-x_i)^D] is nonzero for distinct reals and integer exponent D. The even-exponent case was known, but the odd case remained open.

Approach

The paper reduces the odd case to a strict Pfaffian sign theorem, proved via a paired split-determinant inequality established through Marsden's B-spline factorization and total nonnegativity, a Volterra propagation recurrence, and a Beta–de Bruijn integral bridge. Strictness follows from a separated-powers determinant lemma on a central simplex. The complete proof chain for the odd-exponent theorem was formalized in Lean 4.

Results

A complete classification: det[(x_j-x_i)^D] is nonzero iff D >= N-1 and either N or D is even. The odd-exponent strict positivity of the determinant (and positive Pfaffian) is established and machine-verified.