---

Claim. The answer is yes. For every real $n\times n$ doubly stochastic matrix $M=(a_{ij})$ there is a permutation $\sigma\in S_n$ with

$$\prod_{1\le i\le n}a_{i\sigma(i)}\ge n^{-n}.$$

Marvin Marcus and Henryk Minc prove this in Some results on doubly stochastic matrices, the paper the site cites as [MaMi62] for the resolution of Problem 499. The statement is a weak form of van der Waerden's conjecture, since the permanent of $M$ is the sum of the $n!$ diagonal products and $\operatorname{per}(M)\ge n!\,n^{-n}$ forces one of them to be at least $n^{-n}$; the Marcus–Minc argument predates the proofs of that conjecture by two decades and does not rely on it. The still weaker statement that some $\sigma$ has every $a_{i\sigma(i)}$ nonzero and $\sum_i a_{i\sigma(i)}\ge1$ is due to Marcus and Ree (1959), as the problem page's reference [MaRe59] records.

Acceptance. Refereed: Proc. Amer. Math. Soc. 13 (1962), no. 4, 571–579; the issue is dated August 1962, and the page is dated to the first day of that month. Reviewed: Thomas Bloom, the site's curator, marks the problem proved and credits the proof to Marcus and Minc.

Formalization. Boris Alexeev posted on the site's thread, on 2025-11-29, a Lean 4 proof of the statement generated by Aristotle, the system of Harmonic, from the statement file of the formal-conjectures project; its header credits the informal proof to Marcus and Minc and cites their PAMS paper [MaMi62], and it also lists Inequalities for the permanent function (Ann. of Math. 75 (1962), 47–62) and credits it to Marcus and Minc, although that paper is by Marcus and Newman. The file is linked above at the commit that added it, compiled against Lean 4.24.0 and its Mathlib release. The site's label carries the Lean qualification on this account, and the community database (teorth/erdosproblems) lists the problem as proved with a Lean proof from 2025-11-29. The corpus did not build or audit that development, so the page lists no formalized evidence; the acceptance rests on the refereed paper and the curator's credit. The formal-conjectures statement file for the problem leaves the theorem unproved and names, in its attribute, a later copy of this development (src/v4.29.1/ErdosProblems/Erdos499.lean, at the repository's main branch) as the problem's formal proof.