Skip to content

Erdős problem 499

The conjecture of van der Waerden, which states that the permanent of a doubly stochastic matrix is at least n−nn!n^{-n} n!.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

499.lean

Retained formal statement3 of 3

The conjecture of van der Waerden, which states that the permanent of a doubly stochastic matrix is at least n−nn!n^{-n} n!.

Proved by Gyires [Gy80], Egorychev [Eg81], and Falikman [Fa81].

[Gy80] Gyires, B., The common source of several inequalities concerning doubly stochastic matrices. Publ. Math. Debrecen (1980), 291-304. [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 (1981), 931-938, 957.

FormalConjectures/ErdosProblems/499.leanErdos499.vanDerWaerden1 lineExact file
∀ (n : ℕ), ∀ M ∈ doublyStochastic ℝ (Fin n), ↑n ^ (-↑n) * ↑n.factorial ≤ M.permanent
SolvedStatement only, no proof