VibeMathedMath problems solved with AI
Sign in

Colombo’s difference-power determinant conjecture

Let N≥2N\ge 2 be even and let x1,…,xNx_1,\ldots,x_N be pairwise distinct real numbers. Is the matrixAN,D=[(xj−xi)D]i,j=1N A_{N,D}=\bigl[(x_j-x_i)^D\bigr]_{i,j=1}^{N} nonsingular for every integer D≥N−1D\ge N-1?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Linear algebra; matrix theory and Pfaffians
Posed by
Bonaparte Colombo
Year posed
1928
Years open
98y
Solved
2026-08-18
Model
WuJie AI agent; DeepSeek; Qwen; Kimi; GPT; other LLMs
Vendor
—
Collaborators
Qianli Ma
Verification
Lean-checked, statement unaudited
Publication
Preprint
Significance
12 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For pairwise distinct real numbers x1,…,xNx_1,\ldots,x_N and an integer D≥1D\ge1, Ma proves the complete classificationdet⁡[(xj−xi)D]i,j=1N≠0⟺D≥N−1 and (N is even or D is even). \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 NN. The new part is the even-size, odd-exponent branch, strengthened to the strict Pfaffian sign theorem(−1)(m2)Pf⁡[(xj−xi)2r+1]i,j=12m>0(r≥m−1). (-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.

What the AI did

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.

Verification

The paper’s new odd-exponent theorem is formalized in Lean 4. The public endpoint proves
0<det⁡[(xj−xi)2r+1]0<\det[(x_j-x_i)^{2r+1}]
for every strictly increasing real 2m2m-tuple and every r≥m−1r\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.

Sources

Submitted by AmberGander937 on

Changelog2 changes

Discussion