Dittert conjecture: optimization of row/column product function on matrices

### 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:**
- https://en.wikipedia.org/wiki/Dittert_conjecture, https://arxiv.org/abs/2312.00464, https://research.monash.edu/en/publications/some-results-towards-the-dittert-conjecture-on-permanents

### 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.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-15

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)