Steiner Systems

A Steiner system $S(t, k, n)$ is a collection of $k$-element subsets (called blocks) of an $n$-element set such that every $t$-element subset is contained in exactly one block.

References:

• Wikipedia
• Large Steiner Systems by Kunal Marwaha

structure SteinerSystems.SteinerSystem (t k n : ℕ) : Type

An $S(t, k, n)$-Steiner system is a collection of $k$-element subsets (called blocks) of $\{0, \ldots, n-1\}$ such that every $t$-element subset is contained in exactly one block.

This is the standard notation from combinatorics, where:

• $n$ is the number of points
• $k$ is the block size
• $t$ is the covering parameter (every $t$-subset is in exactly one block)

• blocks : Finset (Finset (Fin n))

  The blocks of the Steiner system.

• block_card (B : Finset (Fin n)) : B ∈ self.blocks → B.card = k

  Every block has exactly $k$ elements.

• cover_unique (R : Finset (Fin n)) : R.card = t → {x ∈ self.blocks | R ⊆ x}.card = 1

  Every $t$-element subset is contained in exactly one block. Note: We use .filter.card = 1 instead of ∃! because ∃! B ∈ blocks, R ⊆ B desugars to a quantifier over all Finset (Fin n), which loses Decidable and breaks native_decide.

def SteinerSystems.«termS(_,_,_)» : Lean.ParserDescr

Notation for Steiner systems: S(t, k, n) denotes a Steiner system with covering parameter t, block size k, and n points.

Equations

• One or more equations did not get rendered due to their size.

structure SteinerSystems.LargeSteinerSystemWitness : Type

A constructive witness for a large Steiner system: concrete values of $n$, $k$, $t$ satisfying $n > k > t > 5$, $t < 10$, $n < 200$, together with an explicit Steiner system.

• n : ℕ

  The size of the ground set.

• k : ℕ

  The block size.

• t : ℕ

  The covering parameter.

• h_nk : self.n > self.k
• h_kt : self.k > self.t
• h_t_lower : self.t > 5
• h_t_upper : self.t < 10
• h_n_upper : self.n < 200
• system : SteinerSystem self.t self.k self.n

  The explicit Steiner system.

def SteinerSystems.large_steiner_systems : LargeSteinerSystemWitness

Construct an $S(t, k, n)$-Steiner system with $n > k > t > 5$, $t < 10$, and $n < 200$.

No example of a Steiner system with $t > 5$ is known, despite a 2014 existence theorem by Keevash showing that such systems must exist for sufficiently large $n$.

Reference: Large Steiner Systems

Equations

• SteinerSystems.large_steiner_systems = sorry

def SteinerSystems.fano_plane : SteinerSystem 2 3 7

Sanity check: the Fano plane is an $S(2, 3, 7)$-Steiner system.

The Fano plane consists of $7$ blocks of size $3$ over $7$ points, where every pair of points is contained in exactly one block.

Equations

• One or more equations did not get rendered due to their size.

theorem SteinerSystems.steiner_system_5_6_12 : Nonempty (SteinerSystem 5 6 12)

Existence of $S(5, 6, 12)$: The small Witt design.

There exists a unique Steiner system $S(5, 6, 12)$, known as the small Witt design. It was constructed by Witt (1938) and is closely related to the Mathieu group $M_{12}$. This is one of only two known Steiner systems with $t = 5$.

theorem SteinerSystems.steiner_system_5_8_24 : Nonempty (SteinerSystem 5 8 24)

Existence of $S(5, 8, 24)$: The large Witt design.

There exists a unique Steiner system $S(5, 8, 24)$, known as the large Witt design. It was constructed by Witt (1938) and is closely related to the Mathieu group $M_{24}$. This is one of only two known Steiner systems with $t = 5$.

theorem SteinerSystems.infinitely_many_steiner_t4 : ∃ (S : Set ((k : ℕ) × (n : ℕ) × SteinerSystem 4 k n)), S.Infinite

There are infinitely many Steiner systems with $t = 4$.

Keevash (2014) proved that for any fixed $t$ and $k$, a Steiner system $S(t, k, n)$ exists for all sufficiently large $n$ satisfying the necessary divisibility conditions. Since there are infinitely many such admissible $n$, this implies infinitely many $S(4, k, n)$ systems exist (for any fixed $k > 4$). The proof is nonconstructive.

Explicit examples include $S(4, 5, 11)$ (the unique system, related to the Mathieu group $M_{11}$) and $S(4, 7, 23)$ (related to the Mathieu group $M_{23}$).

theorem SteinerSystems.infinitely_many_steiner_t5 : ∃ (S : Set ((k : ℕ) × (n : ℕ) × SteinerSystem 5 k n)), S.Infinite

There are infinitely many Steiner systems with $t = 5$.

Keevash (2014) proved that for any fixed $t$ and $k$, a Steiner system $S(t, k, n)$ exists for all sufficiently large $n$ satisfying the necessary divisibility conditions. This settles the long-standing open problem of whether infinitely many $S(5, k, n)$ systems exist. The proof is nonconstructive.

Only two explicit examples are known: $S(5, 6, 12)$ and $S(5, 8, 24)$, both Witt designs related to the Mathieu groups $M_{12}$ and $M_{24}$ respectively. No Steiner system with $t \geq 6$ has been explicitly constructed, though Keevash's result guarantees their existence nonconstructively as well.