Problem 499

../

claims/: The 4 claim pages of Problem 499, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $M=(a_{ij})$ be a real $n\times n$ doubly stochastic matrix (i.e. the entries are non-negative and each column and row sums to $1$). Does there exist some $\sigma\in S_n$ such that

$$\prod_{1\leq i\leq n}a_{i\sigma(i)}\geq n^{-n}?$$

Status. Proved on the site (label PROVED (LEAN)). The site credits the answer yes to Marcus and Minc [MaMi62]; the Lean qualifier refers to a third-party proof described under Formalization. The accepted claims are [[problems/set_systems/E0499/claims/1962_08_01_marcus_minc|the Marcus–Minc theorem]], on its refereed publication and the curator's credit, and the two proofs of van der Waerden's conjecture, which implies the statement: Egorychev and Falikman, each on its refereed publication. The site also credits Gyires with a proof of the conjecture; his paper does not contain one, and that attribution is rejected on its claim page.

Source. erdosproblems.com/499, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #499, https://www.erdosproblems.com/499.

References.

• [Eg81] Egorychev, G. P., The solution of the van der Waerden problem for permanents. Dokl. Akad. Nauk SSSR (1981), 1041-1044.
• [Fa81] Falikman, D. I., Proof of the van der Waerden conjecture on the permanent of a doubly stochastic matrix. Mat. Zametki 29 (1981), no. 6, 931-938, 957.
• [Gy80] Gyires, B., The common source of several inequalities concerning doubly stochastic matrices. Publ. Math. Debrecen (1980), 291-304.
• [MaMi62] Marcus, Marvin and Minc, Henryk, Some results on doubly stochastic matrices. Proc. Amer. Math. Soc. (1962), 571-579.
• [MaRe59] Marcus, M. and Ree, R., Diagonals of doubly stochastic matrices. Quart. J. Math. Oxford Ser. (2) (1959), 296-302.

Formalization. Statement in formal-conjectures, left unproved in that file, whose attribute names as its formal proof the Lean 4 proof in Boris Alexeev's repository (the copy under src/v4.29.1, at the repository's main branch). That proof was generated by Aristotle, the system of Harmonic, from the statement; its header credits the informal proof to Marcus and Minc, and Alexeev posted it on the site's thread on 2025-11-29. It is linked at the commit that added it from the [[problems/set_systems/E0499/claims/1962_08_01_marcus_minc|Marcus–Minc claim page]]; the corpus did not build or audit it.

Current assessment

The site's formulation asks whether every real $n\times n$ doubly stochastic matrix has a permutation $\sigma$ along which the product of entries is at least $n^{-n}$. The answer is yes: [[problems/set_systems/E0499/claims/1962_08_01_marcus_minc|Marcus and Minc 1962]] prove it directly, refereed in Proc. Amer. Math. Soc. and credited by the site's curator, and the problem's standing derives from that accepted claim. The statement is a weak form of van der Waerden's conjecture, $\operatorname{per}(M)\ge n!\,n^{-n}$, since the permanent is the sum of the $n!$ diagonal products and the bound forces one of them to be at least $n^{-n}$; the conjecture's proofs by Egorychev and Falikman are therefore accepted claims as well, each on its refereed publication and without the curator's credit for the problem itself. The site also credits Gyires (1980) with a proof of the conjecture, but his paper derives it from conjectures of its own that it leaves open, proving the bound only for symmetric positive semidefinite matrices and for the matrices $(1-x)A_0+xA$ with $x$ small, where $A_0$ has every entry $1/n$; that attribution is rejected on its claim page. The still weaker statement, a permutation with every entry nonzero and sum at least $1$, is due to Marcus and Ree [MaRe59] and is not part of the question.

Search scope, 2026-10-07: the site's page and discussion thread (Alexeev's Lean posting of 2025-11-29, no proof claims), the community database (teorth/erdosproblems, which lists the problem as proved with a Lean proof from 2025-11-29), the formal-conjectures statement file, the lean-proofs collection, Crossref and zbMATH. No other claim on the problem was found. One third-party Lean proof of the Marcus–Minc theorem is linked from the claim page; the corpus did not build or audit it, and the site's Lean qualifier rests on it.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• falikman_1981_proof_van_der_waerden_conjecture_permanent
• falikman_1981_proof_van_der_waerden_conjecture_permanent / theorem_1