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!.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/499.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:499
  • PLBY Lean proofsErdosProblems.Erdos499

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page