AI 中文总结
该研究解决了科隆博1928年提出的行列式问题，明确了$\boldsymbol{\text{det}}[(x_j-x_i)^D]\boldsymbol{\text{≠}}0$的充要条件，其奇指数情形的证明及完整链已在Lean 4中形式化。
AI 中文摘要
我们完全解决了科隆博1928年提出的行列式问题。对于互不相同的实数$x_1,\boldsymbol{\text{...}},x_N$（$N\boldsymbol{\text{≥}}2$）和整数$D\boldsymbol{\text{≥}}1$，我们证明$\boldsymbol{\text{det}}[(x_j-x_i)^D]\boldsymbol{\text{≠}}0$当且仅当$D\boldsymbol{\text{≥}}N-1$且要么$N$为偶数，要么$D$为偶数。偶指数情形可由Dyn-Goodman-Micchelli（1986）的结果推出；剩余的奇指数情形通过严格的Pfaffian符号定理证明。新的奇指数定理及其完整证明链已在Lean 4中形式化。
英文摘要
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.
Comments16 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)
