High-girth Steiner triple systems

DefinitionErdős Problem 207#✓fully proved

The statement that for every integer \(g \ge 2\) there is an \(N\) such that for every \(n \ge N\) with \(n \equiv 1\) or \(n \equiv 3 \pmod 6\) there is a Steiner triple system on the \(n\) points \(\{0, \dots, n-1\}\) (three-point blocks, every pair of distinct points in exactly one block) in which every set of \(j\) distinct blocks, with \(2 \le j \le g\), covers at least \(j + 3\) points.

def highGirthSteinerTripleSystemsExist : Prop :=
  ∀ g : ℕ, 2 ≤ g → ∀ᶠ n : ℕ in atTop, (n % 6 = 1 ∨ n % 6 = 3) →
    ∃ H : Finset (Finset (Fin n)), SetFamily.IsSteinerTripleSystem H ∧
      ∀ E ⊆ H, 2 ≤ E.card → E.card ≤ g → E.card + 3 ≤ (E.biUnion id).card

Uses 1 · Used by 1

Statement usesSteiner triple system

Used byHigh-girth Steiner triple systems exist

TheoremHigh-girth Steiner triple systems exist#●ready to prove

For every integer \(g \ge 2\) there is an \(N\) such that for every \(n \ge N\) with \(n \equiv 1\) or \(n \equiv 3 \pmod 6\) there is a Steiner triple system on the \(n\) points \(\{0, \dots, n-1\}\) in which every set of \(j\) distinct blocks, with \(2 \le j \le g\), covers at least \(j + 3\) points.

Kwan, Sah, Sawhney and Simkin proved this conjecture of Erdős; in their terms, the Steiner triple system has girth greater than \(g\) (for \(j \le 3\) the condition holds in every Steiner triple system).

public theorem_wanted highGirthSteinerTripleSystemsExist_holds : highGirthSteinerTripleSystemsExist

Sources

• T. F. Bloom, Erdős Problems, Problem #207, https://www.erdosproblems.com/207 (status PROVED); resolution: M. Kwan, A. Sah, M. Sawhney and M. Simkin, High-girth Steiner triple systems, Ann. of Math. (2) 200 (2024), 1059-1156, arXiv:2201.04554, main theorem: Erdős's 1973 conjecture, Steiner triple systems of girth greater than g on all large admissible n, https://doi.org/10.4007/annals.2024.200.3.4.

Uses 1

Statement usesErdős Problem 207

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.