What is the conjecture
The Dittert conjecture concerns the optimization of a function on matrices with constrained sums. Let $K_n$ denote the set of $n \times n$ matrices with nonnegative entries whose sum equals $n$. For a matrix $A \in K_n$, let $r_i$ denote the $i$-th row sum and $c_j$ denote the $j$-th column sum. The permanent of $A$ is $\text{per}(A) = \sum_{\sigma \in S_n} \prod_{i=1}^n a_{i,\sigma(i)}$.
Define the function $\varphi(A) = \left(\prod_{i=1}^n r_i\right) + \left(\prod_{j=1}^n c_j\right) - \text{per}(A)$.
The Dittert conjecture asserts that $\varphi$ attains its unique maximum on $K_n$ at $A = J_n$, where $J_n$ is the $n \times n$ matrix with all entries equal to $1/n$.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 2.5/5 (0 is best) (as of 2026-02-12)
Building blocks (1-3; from search results):
Matrix type and matrix operations (sums, products of row/column sums)Finset.prod for products of sequences- Real/nonnegative matrix constraints
Missing pieces (exactly 2; unclear/absent from search results):
- Permanent function (
per(A)) is not defined in Mathlib and would need to be added
- Optimization/maximization framework for stating unique optimality on the constrained set $K_n$
Rating justification (1-2 sentences): The basic matrix infrastructure exists in Mathlib, but the permanent function requires a custom definition with combinatorial structure. The optimization claim would need a formal framework for expressing uniqueness of maxima over convex/constrained sets, which requires moderate additional infrastructure beyond existing definitions.
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link
What is the conjecture
The Dittert conjecture concerns the optimization of a function on matrices with constrained sums. Let$K_n$ denote the set of $n \times n$ matrices with nonnegative entries whose sum equals $n$ . For a matrix $A \in K_n$ , let $r_i$ denote the $i$ -th row sum and $c_j$ denote the $j$ -th column sum. The permanent of $A$ is $\text{per}(A) = \sum_{\sigma \in S_n} \prod_{i=1}^n a_{i,\sigma(i)}$ .
Define the function$\varphi(A) = \left(\prod_{i=1}^n r_i\right) + \left(\prod_{j=1}^n c_j\right) - \text{per}(A)$ .
The Dittert conjecture asserts that$\varphi$ attains its unique maximum on $K_n$ at $A = J_n$ , where $J_n$ is the $n \times n$ matrix with all entries equal to $1/n$ .
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 2.5/5 (0 is best) (as of 2026-02-12)
Building blocks (1-3; from search results):
Matrixtype and matrix operations (sums, products of row/column sums)Finset.prodfor products of sequencesMissing pieces (exactly 2; unclear/absent from search results):
per(A)) is not defined in Mathlib and would need to be addedRating justification (1-2 sentences): The basic matrix infrastructure exists in Mathlib, but the permanent function requires a custom definition with combinatorial structure. The optimization claim would need a formal framework for expressing uniqueness of maxima over convex/constrained sets, which requires moderate additional infrastructure beyond existing definitions.
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link