Breakthrough Tracker record
A preprint claims a complete, Lean-formalized solution to Colombo’s determinant problem
Qianli Ma proves a necessary-and-sufficient condition for the determinant of the matrix with entries (x_j−x_i)^D to be nonzero for distinct real nodes, completing Colombo’s 1928 problem. The new odd-exponent branch is accompanied by a Lean 4 formalization.
← Back to the filtered Breakthrough Tracker
- Stable ID
math-colombo-determinant-problem-solution-2026- Revision
math-colombo-determinant-problem-solution-2026.v1- Field
- Mathematics · Analysis, determinant inequalities and formalized mathematics
- Evidence
- Tier 1 · Peer reviewed: No
- Record state
- Provisional · Provisional Lean-formalized claimed solution
- Last checked
AI role
The author reports substantial use of WuJie and other AI agents plus DeepSeek, Qwen, Kimi and GPT to identify the strategy and draft the proof. The author checked and revised the argument, formalized it in Lean 4 and accepts responsibility.
Record details
- Problem or result
- Colombo’s 1928 determinant nonvanishing classification for powers of pairwise differences
- Authors
- Qianli Ma
- Institutions
- Zhejiang University; WuJie AI
- Result date
- First-version preprint submitted August 31, 2026
Why it matters
The result supplies the missing odd-exponent classification for a problem originating in hyperbolic partial differential equations. The independent odd-branch preprint and Lean artifact provide stronger corroboration than an isolated informal claim.
Limits
The complete classification remains a non-peer-reviewed preprint. The repository reports a pinned Lean 4.30/mathlib build with 2,817 jobs and no sorry/admit declarations, but this cycle reviewed the artifact metadata and source rather than independently rebuilding the full formalization.
Sources
- Primary: Ma, claimed solution to Colombo’s determinant problem
- Artifacts: Lean 4 formalization of the odd-exponent branch
- Independent: Independent proof of the odd-exponent branch
Correction and revision history
- 2026-09-04 — Added after primary-source, scope, status, AI-role and limitation review.
Machine-readable: JSON v1 · CSV v1 · Schema v1
This individual record remains noindex until a story-specific featured image passes Kingy’s rendered-pixel visual review. The source-linked tracker hub remains the public index.