Colombo’s difference-power determinant conjecture

Precise statement

Let $N\ge 2$ be even and let $x_1,\ldots,x_N$ be pairwise distinct real numbers. Is the matrix $$ A_{N,D}=\bigl[(x_j-x_i)^D\bigr]_{i,j=1}^{N} $$ nonsingular for every integer $D\ge N-1$?

The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.

What AI did

WuJie AI agent; DeepSeek; Qwen; Kimi; GPT; other LLMs

The author reports that the WuJie AI agent and multiple large-language-model systems, including DeepSeek, Qwen, Kimi and GPT, played a substantial role in identifying the proof strategy and producing an initial proof draft. Qianli Ma designed and coordinated the workflow, then checked and revised the mathematical arguments and formalized the new odd-exponent proof chain in Lean 4.

Provider: unknown · Prompt public: unknown · Independence: unknown

Verification boundary

lean checked statement unaudited

The paper’s new odd-exponent theorem is formalized in Lean 4. The public endpoint proves $0<\det[(x_j-x_i)^{2r+1}]$ for every strictly increasing real $2m$-tuple and every $r\ge m-1$, matching Theorem 1.2 of the paper. The repository reports a complete 2817-job build, no `sorry`, `admit`, or project-specific axioms, and an axiom audit containing only `propext`, `Classical.choice`, and `Quot.sound`; the formalization is also registered in Palomar. The complete classification additionally imports the classical even-exponent theorem of Dyn–Goodman–Micchelli, which this repository does not formalize. The paper statement and public theorem interface were compared for this submission, but the repository was not rebuilt by the submitter and no named independent informal-to-formal statement-fidelity audit is yet identified. Therefore “Lean-checked, statement unaudited” is the conservative label.

Correctness: supported · statement fidelity: unaudited · peer review: none

Timeline

1. 2026-08-18

   Qianli Ma, “Colombo’s Determinant Problem” (arXiv:2609.00101)

   For pairwise distinct real numbers $x_1,\ldots,x_N$ and an integer $D\ge1$, Ma proves the complete classification $$ \det\bigl[(x_j-x_i)^D\bigr]_{i,j=1}^{N}\ne0 \quad\Longleftrightarrow\quad D\ge N-1\ \text{and}\ \bigl(N\text{ is even or }D\text{ is even}\bigr). $$ This fully resolves Colombo’s original conjecture for even $N$. The new part is the even-size, odd-exponent branch, strengthened to the strict Pfaffian sign theorem $$ (-1)^{\binom m2}\operatorname{Pf} \bigl[(x_j-x_i)^{2r+1}\bigr]_{i,j=1}^{2m}>0 \qquad(r\ge m-1). $$ The even-exponent branch follows from the classical work of Dyn–Goodman–Micchelli. A concurrent independent proof of the odd branch by Kun Li, Li Tie, Peng Wang and Zihan Liu is linked below.

Known method families

argument (source-reported)

Source-reported tools: argument.

Independent: unknown · difference confidence: 0

What remains uncertain

VibeMath has not independently audited the mathematical statement, proof, or novelty claim.

• The source status is candidate and must not be represented as solved.
• VibeMath has not independently verified the mathematical claim.
• AI-attempt independence and training-data exposure are unknown unless explicitly documented.
• VibeMath has not independently audited the mathematical statement, proof, or novelty claim.