A Proof of the Dittert Conjecture in Dimension 4 via an Agent-Guided Exact Sum-of-Squares Certificate

Beibei Xiong; Jinhui Li; Zhengfeng Yang

REVIEW 3 major objections 4 minor 17 references

This paper proves that among all nonnegative 4x4 matrices with total entry sum 4, the uniform matrix uniquely maximizes the Dittert functional, via an exact rational sum-of-squares certificate.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-03 11:57 UTC pith:23L567BX

load-bearing objection A credible solution to Dittert in dimension 4, with a load-bearing but unpinned Lean artifact; the math in the paper is coherent and the result deserves peer review. the 3 major comments →

arxiv 2607.29191 v1 pith:23L567BX submitted 2026-07-31 cs.SC

A Proof of the Dittert Conjecture in Dimension 4 via an Agent-Guided Exact Sum-of-Squares Certificate

Jinhui Li , Beibei Xiong , Zhengfeng Yang This is my paper

classification cs.SC MSC 15A1590C22

keywords Dittert conjecturepermanentsum-of-squaresexact rational certificatequantitative stabilitysemidefinite programmingformal verificationnonnegative matrices

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper aims to settle the dimension-4 case of the Dittert conjecture: the functional built from row-sum products, column-sum products, and the permanent is uniquely maximized over the simplex by the uniform matrix. The proof establishes a stronger quantitative statement: 61/32 minus the functional is at least 1/52 times the squared Frobenius distance to the uniform matrix, which forces uniqueness. The inequality is reduced to certifying nonnegativity of a quartic polynomial in sixteen variables on the simplex. The authors construct an explicit rational sum-of-squares certificate, verify the polynomial identity exactly over the rationals, and check the result with a formal proof assistant, so numerical solvers are used only for discovery, not as evidence.

Core claim

The central claim is that for every nonnegative 4x4 matrix A with entries summing to 4, the gap between the maximum value 61/32 and the Dittert functional φ(A) is at least (1/52) times the squared Frobenius distance to the uniform matrix U4. Since this distance vanishes only at U4, the Dittert functional has U4 as its unique maximizer in dimension 4. The proof works by defining P4(x) = Q4(x) − (8/13)Δ4(x), where Q4 is 32 times the functional gap and Δ4 is the squared Frobenius distance, and showing that P4 belongs to the truncated pairwise preordering T2. This membership gives an exact identity P4 = σ0 + Σ xi σi + Σ xixj σij + h q, with all σ terms sums of squares and h vanishing on the simp

What carries the argument

The key object is the gap polynomial P4(x) = Q4(x) − (8/13)Δ4(x), a structured quartic in sixteen variables. The proof establishes P4 ∈ T2, where T2 is the degree-four truncated pairwise preordering: sums of squares plus multipliers by the nonnegative variables xi and xixj, plus a multiplier of the simplex equality h = 4 − Σxi. Membership in T2 guarantees nonnegativity on the simplex and yields the quantitative stability constant 1/52. The certificate is built by an agent-guided search over SOS templates and sequential rational recovery, with singular Gram matrices transformed to regular full-rank blocks and recovered exactly; the final identity is checked exactly over Q and by a formal proo

Load-bearing premise

The theorem is established only if the machine-checked certificate files are complete, compile with the stated proof-assistant toolchain, and actually verify the claimed polynomial identity; the paper itself does not print the full certificate or proof script, so a reader must run the external artifact to confirm the proof.

What would settle it

Run the published proof artifact: if the normalized certificate polynomial does not exactly equal 13Q4 − 8Δ4, or if any exact LDLᵀ decomposition reports a non-positive pivot, the proof collapses. Alternatively, a numerical search over K4 for a matrix A with 61/32 − φ(A) < (1/52)||A − U4||²_F would falsify the quantitative stability theorem and hence the claimed proof of the Dittert conjecture in dimension 4.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

If the certificate is correct, the Dittert conjecture in dimension 4 is proved, with the uniform matrix as the unique maximizer.
The stronger quantitative bound 61/32 − φ(A) ≥ (1/52)||A − U4||²_F gives explicit stability: near-maximizers must be close to the uniform matrix.
Restricting to doubly stochastic matrices recovers the van der Waerden lower bound for the permanent in dimension 4 as a special case.
The exact rational SOS identity means the result does not depend on numerical solver precision; the certificate data can in principle be checked by any exact computation system.
The proof method demonstrates that a singular, equality-constrained SOS certificate can be recovered exactly and formally verified, not just approximated numerically.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same template-search plus sequential-recovery pipeline could be applied to the Dittert problem in higher dimensions, though the number of SOS blocks and recovery denominators would grow rapidly.
The stability constant 1/52 is the one certified by the degree-4 SOS relaxation; higher-degree relaxations might yield a larger constant and a sharper quantitative description of near-maximizers.
Because the final check is a finite rational identity, the proof could likely be re-verified by other independent proof-checking systems, moving trust from the specific toolchain to the shared mathematical statement.
If one views the functional gap as a measure of disorder, the quantitative inequality says the uniform matrix is not merely the unique maximizer but is quadratically isolated in the simplex.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

A credible solution to Dittert in dimension 4, with a load-bearing but unpinned Lean artifact; the math in the paper is coherent and the result deserves peer review.

read the letter

Quick take: this is a serious paper. It proves Dittert in dimension 4 via the stronger stability bound 61/32 − φ(A) ≥ (1/52)||A−U4||_F^2, and the reduction to certifying P4 = Q4 − (8/13)Δ4 in T2 is clean. If the exact certificate exists as described, the theorem is settled; the only reason I won't call it settled is that the certificate isn't in the manuscript.

What's genuinely new: dimension 4 was open (n=2,3 and n≥17 known), and the quantitative stability statement is new. The technical adaptation is also real: equality at U4 makes all Gram matrices singular, and the certificate couples 136 small blocks with a free multiplier q of h=0, so the standard recovery methods of [9,10] don't apply directly. Sequential recovery—fix small blocks, rationalize the main block, check the residual on h=0—handles that, and the reported denominators (1331 and 32767) are specific enough to be audited.

The circularity worry is not real. The solver is used only for discovery; the certificate is checked by exact arithmetic and, supposedly, Lean. Remark 5.1 says this explicitly, and that's the right way to use numerics.

The real soft spot is the missing artifact. No exact certificate, no Gram coefficients, no q, and the Lean repo has no commit hash or manifest. The toolchain v4.30.0-rc1 is unpinned. A referee cannot reproduce the proof from this submission. That's a load-bearing verifiability gap, not a mathematical flaw. The internal reduction is coherent, and nothing suggests the identity is false or fudged.

Bottom line: send to peer review. Don't desk-reject it. Require a pinned, archived repository with full certificate data and a rebuild script. If the Lean proof rebuilds, accept; if the artifact can't be made auditable, this version doesn't establish the theorem. Either way, the paper deserves referee time.

Referee Report

3 major / 4 minor

Summary. The paper claims to prove the Dittert conjecture in dimension 4 by establishing the stronger quantitative stability bound 61/32 − φ(A) ≥ (1/52)||A − U_4||_F^2 on the simplex K_4. The proof is reduced to certifying nonnegativity of the quartic polynomial P_4 = Q_4 − (8/13)Δ_4 on the simplex, which is approached via an agent-guided symbolic–numeric method that constructs a rational sum-of-squares certificate in a truncated pairwise preordering. The manuscript describes the numerical search, the sequential exact recovery of Gram blocks (with denominators D_sm = 1331 and D_0 = 32767), and reports that the final polynomial identity is verified by exact rational arithmetic and by the Lean proof assistant. The main SOS consists of 152 weighted squares plus 136 blocks of 16 squares each.

Significance. If the certificate is correct and the Lean formalization is sound, this would settle a decades-old conjecture in its first open case, with an explicit stability constant. The methodological contribution—an agent-guided exact SOS recovery that handles singular Gram matrices and coupled constraints—is of independent interest for symbolic-numeric computation. The paper is honest about the trusted computing base: the numerical solver is used only for discovery, and the final certificate is claimed to be checked exactly in Lean. However, the significance cannot be fully realized in its current form because the actual certificate data and the Lean artifact are not included in the manuscript, making the central claim unverifiable from the paper alone.

major comments (3)

[§5, GitHub URL] The entire proof rests on an external Lean repository at https://github.com/123ljh0bot/Dittert_Conjecture_in_Dimension_4, but the manuscript provides no commit hash, file manifest, or checksum. The toolchain version v4.30.0-rc1 does not identify a unique repository state. A reader cannot check that the certificate data are complete, that the normalization identities (normalized_certificate, normalized_compactTarget) are checked for the exact target polynomial, or that the environment reproduces the claimed theorems. Since the certificate data themselves are not printed in the paper, the theorem is not established by the manuscript alone. This is load-bearing and must be fixed by including the artifact (with a pinned commit) or by providing the full certificate and proof scripts in an appendix/supplement.
[§4.2, Eq. (29)] The central polynomial identity P_4 = σ_0 + Σ_i x_i σ_i + Σ_{i<j} x_i x_j σ_{ij} + h q is asserted, along with the recovery denominators D_sm = 1331 and D_0 = 32767, but the actual rational squares, their weights, the multiplier q, and the LDL^T certificates are omitted. The text states that 'an independent exact expansion verifies (29) coefficientwise over Q,' but without the data this cannot be checked by the reader. The identity is the mathematical core of the proof; omitting it leaves the paper as a recipe rather than a proof.
[§5, 'native_decide' and 'implemented_by'] The paper states that the formal verification relies on native_decide and implemented_by, and explicitly includes these in the trusted computing base. This means the 'Lean proof' is not necessarily a fully kernel-checked proof object; it relies on the soundness of the native code generator. The manuscript should clarify whether the final theorem statements are backed by kernel-checked proof terms or by this external evaluation mechanism, and if the latter, justify why this is acceptable for a formal proof. The finite certificate checks and polynomial normalization are exactly the steps where errors could hide, so this is not a cosmetic point.

minor comments (4)

[§4.2, Eq. (24)] The definition of P_b as '(−ezb(c)^T, I_{m_b−1})' is ambiguous. It should be stated clearly that P_b is the (m_b−1) × m_b matrix whose first column is −ezb(c) and whose remaining columns form the identity matrix.
[§3.2, around Eq. (17)–(19)] The numerical value λ_2 ≈ 0.6153852 is reported, and the rational target 8/13 ≈ 0.6153846 is selected, but the selection criterion and the reliability of the numerical digits are not discussed. Please comment on the gap and on how the numerical certificate guided the choice of the target.
[§5, code for d4Poly] The displayed Lean code for d4Poly contains ellipses ('centeredSquare 0, centeredSquare 1,. . ., centeredSquare 15'), which is not syntactically valid Lean. Presumably this is a formatting artifact; please ensure all code excerpts are exact and compilable.
[§1, references] Reference [8] is described as a 'recent arXiv preprint' with an arXiv identifier; it would be helpful to give the title and author list as in the other references.

Circularity Check

0 steps flagged

No significant circularity: the exact certificate is independently verified by rational arithmetic and Lean, with numerical search explicitly outside the trusted base.

full rationale

The derivation chain is coherent and non-circular. The paper defines Q4 from the Dittert functional, defines Δ4 as squared Frobenius distance, and sets P4,λ = Q4 − λΔ4. It then proves that for λ̄ = 8/13, P4,λ̄ belongs to the truncated pairwise preordering T2, which immediately yields Theorem 1.2 and hence Theorem 1.1. The numerical SDP solver and agent-guided search are used only to discover candidate certificate data; Remark 5.1 explicitly excludes them from the trusted computing base. The final certificate is verified by exact rational LDLT decompositions, coefficientwise polynomial identity checks over Q, and machine-checked Lean proofs of the two normalization identities and weight nonnegativity. The choice of λ̄ is informed by the numerical optimum, but this is a discovery heuristic, not a fitted input disguised as a prediction: the subsequent exact verification is independent of the solver. The self-citations [9,10] are methodological references for rational SOS recovery, and the final theorem does not reduce to their correctness because the certificate is re-verified exactly. The omission of the full certificate data and the unpinned GitHub URL are reproducibility/verifiability concerns, not circularity: they do not make the derivation equivalent to its inputs by construction.

Axiom & Free-Parameter Ledger

3 free parameters · 4 axioms · 0 invented entities

The proof does not introduce new entities. It uses one hand-chosen rational stability parameter and two recovery denominators; all are subsequently certified by exact arithmetic/Lean. The only non-mathematical assumption is the correctness of the trusted Lean evaluation machinery.

free parameters (3)

Rational stability parameter λbar = 8/13
Selected as the nearby rational to the MOSEK optimum λnum≈0.6153852 in §3.2; exact certificate later proves feasibility, so it is not an empirically predicted constant.
Small-block recovery denominator Dsm = 1331
Chosen by agent search so that 136 rationalized reduced Gram matrices are positive definite (§4.2); construction parameter.
Main-block recovery denominator D0 = 32767
Chosen by agent search so that the corrected main reduced matrix is positive definite and the residual vanishes on h=0 (§4.2); construction parameter.

axioms (4)

standard math If P4,λ = σ0 + Σ xi σi + Σ xi xj σij + h q with σ's SOS and q polynomial, then P4,λ ≥ 0 on K4.
On K4, xi≥0, h=0; weights are nonnegative. This is the standard preordering argument invoked in §3.2.
standard math Exact rational LDL^T decomposition with positive pivots certifies positive definiteness of S_b; hence G_b = P_b S_b P_b^T is positive semidefinite.
Used in §4.2 to certify all SOS blocks without floating point.
domain assumption Lean's native_decide and FastPolyForSOS normalization are correct; they are trusted components as acknowledged in Remark 5.1.
The formal verification relies on these evaluators; the authors themselves include them in the trusted computing base.
domain assumption The entrywise polynomial encodings (dh4IntegerPoly, d4Poly, simplexEquality) match the mathematical definitions of Q4, Δ4, h via bridging lemmas.
If the encodings are wrong, the Lean proof wouldn't apply to the mathematical statement; bridging lemmas are claimed but not shown.

pith-pipeline@v1.3.0-daily-deepseek · 8230 in / 18674 out tokens · 195019 ms · 2026-08-03T11:57:06.433527+00:00 · methodology

0 comments

read the original abstract

The Dittert conjecture states that the Dittert functional on nonnegative $n\times n$ matrices whose entries sum to $n$ is uniquely maximized by the uniform matrix. We prove the conjecture in dimension $4$. More precisely, let $K_4$ be the simplex of nonnegative $4\times4$ real matrices whose entries sum to $4$, let $U_4$ be the uniform matrix, and let $\phi$ denote the Dittert functional. We establish $\frac{61}{32}-\phi(A)\geq \frac{1}{52}\lVert A-U_4\rVert_F^2$ for every $A\in K_4$. Consequently, $U_4$ is the unique maximizer of $\phi$ on $K_4$. The proof reduces to certifying the nonnegativity of a structured quartic polynomial in sixteen variables on a simplex. We construct an exact rational constrained sum-of-squares certificate using an agent-guided symbolic-numeric procedure that combines template selection with sequential rational recovery. The main SOS consists of $152$ positively weighted rational squares, while each of the $136$ smaller SOS blocks consists of $16$ such squares. Exact $LDL^{\mathsf{T}}$ decompositions certify positivity, and exact coefficient comparison over $\mathbb{Q}$ verifies the complete polynomial identity. The resulting exact certificate is formally verified using the Lean proof assistant.

discussion (0)

Reference graph

Works this paper leans on

17 extracted references · 1 linked inside Pith

[1]

Minc, Theory of permanents 1982–1985, Linear and Multilinear Algebra 21 (1987) 109–148

H. Minc, Theory of permanents 1982–1985, Linear and Multilinear Algebra 21 (1987) 109–148

1982
[2]

Hajek, A Conjectured Generalized Permanent Inequality and a Multi- access Problem, in: Open Problems in Communication and Computation, Springer, 1987, pp

B. Hajek, A Conjectured Generalized Permanent Inequality and a Multi- access Problem, in: Open Problems in Communication and Computation, Springer, 1987, pp. 127–129

1987
[3]

Cheon, I

G.-S. Cheon, I. M. Wanless, Some results towards the Dittert conjecture on permanents, Linear Algebra and its Applications 436 (2012) 791–801

2012
[4]

Sinkhorn, A problem related to the van der waerden permanent theorem, Linear and Multilinear Algebra 16 (1984) 167–173

R. Sinkhorn, A problem related to the van der waerden permanent theorem, Linear and Multilinear Algebra 16 (1984) 167–173

1984
[5]

S. G. Hwang, A note on a conjecture on permanents, Linear Algebra and its Applications 76 (1986) 31–44

1986
[6]

S. G. Hwang, On a Conjecture of E. Dittert, Linear Algebra and its Applications 95 (1987) 161–169. 16

1987
[7]

D. K. Udayan, K. Somasundaram, Lih Wang’s and Dittert’s conjectures on permanents, Special Matrices 12 (2024) 20240006

2024
[8]

Pang, Proof of Dittert’s conjecture for dimensionsn≥ 17(2026)

Z. Pang, Proof of Dittert’s conjecture for dimensionsn≥ 17(2026). arXiv:2606.01531

Pith/arXiv arXiv 2026
[9]

Peyrl, P

H. Peyrl, P. A. Parrilo, Computing sum of squares decompositions with rational coefficients, Theoretical Computer Science 409 (2008) 269–281

2008
[10]

E. L. Kaltofen, B. Li, Z. Yang, L. Zhi, Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients, Journal of Symbolic Computation 47 (2012) 1–15

2012
[11]

G. P. Egorychev, The solution of van der Waerden’s problem for perma- nents, Soviet Mathematics Doklady 23 (1981) 619–622

1981
[12]

D. I. Falikman, Proof of the van der Waerden conjecture regarding the permanent of a doubly stochastic matrix, Mathematical Notes 29 (1981) 475–479

1981
[13]

P. A. Parrilo, Structured Semidefinite Programs and Semialgebraic Geom- etry Methods in Robustness and Optimization, Ph.D. thesis, California Institute of Technology (2000)

2000
[14]

J. B. Lasserre, Global Optimization with Polynomials and the Problem of Moments, SIAM Journal on Optimization 11 (2001) 796–817

2001
[15]

MOSEK ApS, MOSEK Optimizer API for Python, Version 11.2.2 (2026)

2026
[16]

de Moura, S

L. de Moura, S. Ullrich, The Lean 4 Theorem Prover and Programming Language, in: Automated Deduction – CADE 28, Vol. 12699 of Lecture Notes in Computer Science, 2021, pp. 625–635

2021
[17]

The mathlib Community, The Lean Mathematical Library, in: Proceed- ings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, 2020, pp. 367–381. 17

2020

[1] [1]

Minc, Theory of permanents 1982–1985, Linear and Multilinear Algebra 21 (1987) 109–148

H. Minc, Theory of permanents 1982–1985, Linear and Multilinear Algebra 21 (1987) 109–148

1982

[2] [2]

Hajek, A Conjectured Generalized Permanent Inequality and a Multi- access Problem, in: Open Problems in Communication and Computation, Springer, 1987, pp

B. Hajek, A Conjectured Generalized Permanent Inequality and a Multi- access Problem, in: Open Problems in Communication and Computation, Springer, 1987, pp. 127–129

1987

[3] [3]

Cheon, I

G.-S. Cheon, I. M. Wanless, Some results towards the Dittert conjecture on permanents, Linear Algebra and its Applications 436 (2012) 791–801

2012

[4] [4]

Sinkhorn, A problem related to the van der waerden permanent theorem, Linear and Multilinear Algebra 16 (1984) 167–173

R. Sinkhorn, A problem related to the van der waerden permanent theorem, Linear and Multilinear Algebra 16 (1984) 167–173

1984

[5] [5]

S. G. Hwang, A note on a conjecture on permanents, Linear Algebra and its Applications 76 (1986) 31–44

1986

[6] [6]

S. G. Hwang, On a Conjecture of E. Dittert, Linear Algebra and its Applications 95 (1987) 161–169. 16

1987

[7] [7]

D. K. Udayan, K. Somasundaram, Lih Wang’s and Dittert’s conjectures on permanents, Special Matrices 12 (2024) 20240006

2024

[8] [8]

Pang, Proof of Dittert’s conjecture for dimensionsn≥ 17(2026)

Z. Pang, Proof of Dittert’s conjecture for dimensionsn≥ 17(2026). arXiv:2606.01531

Pith/arXiv arXiv 2026

[9] [9]

Peyrl, P

H. Peyrl, P. A. Parrilo, Computing sum of squares decompositions with rational coefficients, Theoretical Computer Science 409 (2008) 269–281

2008

[10] [10]

E. L. Kaltofen, B. Li, Z. Yang, L. Zhi, Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients, Journal of Symbolic Computation 47 (2012) 1–15

2012

[11] [11]

G. P. Egorychev, The solution of van der Waerden’s problem for perma- nents, Soviet Mathematics Doklady 23 (1981) 619–622

1981

[12] [12]

D. I. Falikman, Proof of the van der Waerden conjecture regarding the permanent of a doubly stochastic matrix, Mathematical Notes 29 (1981) 475–479

1981

[13] [13]

P. A. Parrilo, Structured Semidefinite Programs and Semialgebraic Geom- etry Methods in Robustness and Optimization, Ph.D. thesis, California Institute of Technology (2000)

2000

[14] [14]

J. B. Lasserre, Global Optimization with Polynomials and the Problem of Moments, SIAM Journal on Optimization 11 (2001) 796–817

2001

[15] [15]

MOSEK ApS, MOSEK Optimizer API for Python, Version 11.2.2 (2026)

2026

[16] [16]

de Moura, S

L. de Moura, S. Ullrich, The Lean 4 Theorem Prover and Programming Language, in: Automated Deduction – CADE 28, Vol. 12699 of Lecture Notes in Computer Science, 2021, pp. 625–635

2021

[17] [17]

The mathlib Community, The Lean Mathematical Library, in: Proceed- ings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, 2020, pp. 367–381. 17

2020