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 statement1 of 3

Let MM be a real n×nn \times n doubly stochastic matrix. Does there exist some σ∈Snσ \in S_n such that ∏1≤i≤nMi,σ(i)≥n−n? \prod_{1 \leq i \leq n} M_{i, σ(i)} \geq n^{-n}? This is true, and was proved by Marcus and Minc [MaMi62]

[MaMi62] Marcus, Marvin and Minc, Henryk, Some results on doubly stochastic matrices. Proc. Amer. Math. Soc. (1962), 571-579.

FormalConjectures/ErdosProblems/499.leanErdos499.erdos_4991 lineExact file
True ↔ ∀ (n : ℕ), ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ, ↑n ^ (-↑n) ≤ ∏ i, M i (σ i)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.