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)

The blocks of the Steiner system.

Every block has exactly $k$ elements.

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.

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

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.

The size of the ground set.

The block size.

The covering parameter.

The explicit Steiner system.

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

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.

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

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

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}$).

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.