Erdős problem 499 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

499.lean

Retained formal statement1 of 3

Let $M$ be a real $n \times n$ doubly stochastic matrix. Does there exist some $σ \in S_n$ such that $\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

1True ↔ ∀ (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.

Sources

Search problems.science