The Dittert conjecture is an inequality for the permanent of a nonnegative 
matrix whose entries sum
to 
. If 
and 
are its row and column sums, it asserts that
 |
with equality only when all entries equal 
, for 
(Dai et al. 2026). For a doubly
stochastic matrix, this reduces to 
.
Dai et al. (2026) reported a proof using boundary rigidity. Dai et al. (2026) report autonomous mathematical search and exploratory derivations by the TARS agent system. Dai reconstructed the proof, supplied omitted details, and manually verified the mathematical results.
