SteinerSystem.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

8 declarations, 4 contain sorry, 0 declared as axioms

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

Imports (1)

FormalConjecturesUtil

structure SteinerSystems.SteinerSystem 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 line 45 source
Source documentation
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)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
```
structure SteinerSystem (t k n : ℕ) where
…
```
structure SteinerSystems.LargeSteinerSystemWitness 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 line 63 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure LargeSteinerSystemWitness where
…
```
theorem SteinerSystems.large_steiner_systems Construct an $S(t, k, n)$-Steiner system with $n > k > t > 5$, $t < 10$, and $n < 200$ sorry line 87 source
Source documentation
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

L4DEL explanation
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
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nonempty, SteinerSystems.LargeSteinerSystemWitness
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem large_steiner_systems : Nonempty LargeSteinerSystemWitness := by
…
```
Mentions: SteinerSystems.LargeSteinerSystemWitness
def SteinerSystems.fano_plane Sanity check: the Fano plane is an $S(2, 3, 7)$-Steiner system line 97 source
Source documentation
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.

extra axioms: _private.0.SteinerSystems.fano_plane._native.native_decide.ax_1, _private.0.SteinerSystems.fano_plane._native.native_decide.ax_2 what this means
Statement uses: SteinerSystems.SteinerSystem, OfNat.ofNat, Nat
Proof uses: SteinerSystems.SteinerSystem.mk, Insert.insert, Finset, Fin, Singleton.singleton
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def fano_plane : S(2, 3, 7) :=
…
```
theorem SteinerSystems.steiner_system_5_6_12 Existence of $S(5, 6, 12)$: The small Witt design line 110 source
Source documentation
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$.

extra axioms: _private.0.SteinerSystems.steiner_system_5_6_12._native.native_decide.ax_1, _private.0.SteinerSystems.steiner_system_5_6_12._native.native_decide.ax_2 what this means
Statement uses: Nonempty, SteinerSystems.SteinerSystem, OfNat.ofNat, Nat
Proof uses: Nonempty.intro, SteinerSystems.SteinerSystem.mk, Insert.insert, Finset, Fin, Singleton.singleton, of_decide_eq_true, Membership.mem, Eq, Finset.card, Finset.filter, LE.le
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem steiner_system_5_6_12 : Nonempty S(5, 6, 12) :=
…
```
theorem SteinerSystems.steiner_system_5_8_24 Existence of $S(5, 8, 24)$: The large Witt design sorry line 253 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Nonempty, SteinerSystems.SteinerSystem, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem steiner_system_5_8_24 : Nonempty S(5, 8, 24) := by
…
```
theorem SteinerSystems.infinitely_many_steiner_t4 There are infinitely many Steiner systems with $t = 4$ sorry line 271 source
Source documentation
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}$).
Only nontrivial systems with $4 < k < n$ are counted: for every $n$ the single block $\{1, \dots, n\}$ is an $S(4, n, n)$, and all $4$-subsets of an $n$-set form an $S(4, 4, n)$.

depends on sorry what this means
Statement uses: Set.Infinite, Sigma, Nat, SteinerSystems.SteinerSystem, OfNat.ofNat, Set.ofPred, And, LT.lt, Sigma.fst, Sigma.snd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem infinitely_many_steiner_t4 :
    {s : Σ k n : ℕ, S(4, k, n) | 4 < s.1 ∧ s.1 < s.2.1}.Infinite := by
…
```
theorem SteinerSystems.infinitely_many_steiner_t5 There are infinitely many Steiner systems with $t = 5$ sorry line 292 source
Source documentation
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.
Only nontrivial systems with $5 < k < n$ are counted, for the same reason as in infinitely_many_steiner_t4. No Steiner system with $t \geq 6$ has been explicitly constructed, though Keevash's result guarantees their existence nonconstructively as well.

depends on sorry what this means
Statement uses: Set.Infinite, Sigma, Nat, SteinerSystems.SteinerSystem, OfNat.ofNat, Set.ofPred, And, LT.lt, Sigma.fst, Sigma.snd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem infinitely_many_steiner_t5 :
    {s : Σ k n : ℕ, S(5, k, n) | 5 < s.1 ∧ s.1 < s.2.1}.Infinite := by
…
```