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 $σ \in S_{n}$ such that $1 \leq i \leq n \prod a_{iσ (i)} \geq n^{- n} ?$

Worked, still open.

combinatorics · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 15 · solved (literature)

lemma erdos_499 :
    answer(True) ↔ (∀ n, ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ : Equiv.Perm (Fin n),
      n ^ (- n : ℤ) ≤ ∏ i, M i (σ i))

solved