Back to Problems

vanDerWaerden

Specification

The conjecture of van der Waerden, which states that the permanent of a doubly stochastic matrix is at least $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.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
lemma vanDerWaerden (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) (hM : M ∈ doublyStochastic ℝ (Fin n)) :
    n ^ (- n : ℤ) * n ! ≤ M.permanent
ID: ErdosProblems__499__vanDerWaerden
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.