Existence of Steiner systems

DefinitionExistence conjecture for Steiner systems#✓fully proved

The statement that for all natural numbers \(r < k\) there is an \(N\) such that for every \(n \ge N\) with \(\binom{k-i}{r-i} \mid \binom{n-i}{r-i}\) for all \(0 \le i < r\), there is a Steiner system \(S(r, k, n)\): a family \(F\) of \(k\)-element subsets of \(\{0, \dots, n-1\}\) such that every \(r\)-element subset of \(\{0, \dots, n-1\}\) is contained in exactly one member of \(F\) (Erdős Problem 722).

def steinerSystemsExistForLargeN : Prop :=
  ∀ r k : ℕ, r < k → ∀ᶠ n : ℕ in Filter.atTop,
    (∀ i < r, (k - i).choose (r - i) ∣ (n - i).choose (r - i)) →
      ∃ F : Finset (Finset (Fin n)), (∀ A ∈ F, A.card = k) ∧
        ∀ S : Finset (Fin n), S.card = r → ∃! A, A ∈ F ∧ S ⊆ A

Used by 1

Used byKeevash's existence theorem for Steiner systems

TheoremKeevash's existence theorem for Steiner systems#●ready to prove

For all natural numbers \(r < k\) there is an \(N\) such that for every \(n \ge N\) with \(\binom{k-i}{r-i} \mid \binom{n-i}{r-i}\) for all \(0 \le i < r\), there is a Steiner system \(S(r, k, n)\): a family \(F\) of \(k\)-element subsets of \(\{0, \dots, n-1\}\) such that every \(r\)-element subset of \(\{0, \dots, n-1\}\) is contained in exactly one member of \(F\).

Keevash proved the existence conjecture for designs, which gives this statement (earlier cases: Kirkman for \((r, k) = (2, 3)\), Hanani, Wilson for \(r = 2\)); erdosproblems.com/722 lists the problem as proved.

public theorem_wanted steinerSystemsExistForLargeN_holds : steinerSystemsExistForLargeN

Sources

• T. F. Bloom, Erdős Problems, Problem #722, https://www.erdosproblems.com/722 (status PROVED); resolution: P. Keevash, The existence of designs, arXiv:1401.3665 (2014), abstract: proves the existence conjecture for combinatorial designs (Steiner's question of 1853): the divisibility conditions suffice for all large n; erdosproblems.com/722: proved by Keevash for all (r, k), https://arxiv.org/abs/1401.3665.

Uses 1

Statement usesExistence conjecture for Steiner systems

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.