The smallest number of 6-element blocks from a 12-element set such that every 4-element subset lies inside at least one block is 41. The value had been pinned between 40 and 41 since 1993. The lower end is now closed: no 40-block cover exists.
A covering design C(v, k, t) is a family of k-element blocks drawn from a v-element ground set with the property that every t-element subset of the ground set is contained in at least one block. The covering number C(v, k, t) is the least possible number of blocks. Here v = 12, k = 6, t = 4: the 495 four-element subsets of a twelve-point set must all be covered by six-point blocks, and the question is how few blocks suffice.
Forty-one has been known to suffice since 1993. Whether forty could also suffice was not known. It cannot.
The result is an equality, so it needs an upper bound, a lower bound, and the refutation of the one value in between.
An explicit 41-block design, taken from the La Jolla Covering Repository and re-checked here from first principles: all 41 blocks distinct, all 495 quadruples covered, zero uncovered.
This step is a finite check, not a search. It was re-run independently rather than cited.
blocks sha256 16e56e8a8a5590ed…3375ae71 · uncovered: 0Two applications of the Schönheim recursion. C(10,4,2) ≥ 9 gives C(11,5,3) ≥ 20, which gives C(12,6,4) ≥ 40.
The only step that is not arithmetic is C(10,4,2) ≥ 9, and that one is discharged by a machine-checked refutation rather than by citation.
Certificate lb-c1042-8-deg3 · UNSAT · replay verifiedThe hard part. A 40-block cover is shown to be impossible by reducing to a finite, exhaustively enumerated case tree of 247 branches and refuting every branch.
Every refutation is a resolution proof that was written out, replayed by an independent checker, and hashed.
247 of 247 branches closed · 0 missingA blind search over 40-block families from the 924 possible blocks is far too large. The proof first shows that a 40-block cover, if one existed, would be extremely rigid — rigid enough to enumerate.
A 40-block cover uses 40 × 6 = 240 point slots across 12 points, an average of 20. The blocks through any single point form a C(11,5,3) cover of the remaining 11 points, so every degree is at least C(11,5,3) = 20. Average 20 with minimum 20 forces every degree to equal 20.
Delete a point from each of the 20 blocks through it. The result is a 20-block covering design on 11 points with 5-element blocks covering all triples — the minimum possible size.
Link degrees sum to 20 × 5 = 100. Each link point's blocks form a C(10,4,2) cover, so each link degree is at least 9. Eleven values, each at least 9, summing to 100, leaves slack exactly one: ten nines and a single ten. There is no freedom left.
Fixing the degree-10 point and quotienting by a relabelling group of order 3840 turns the residual choice into a tree of root, secondary and tertiary orbits — 247 branches in total. The group used is a proper subgroup of the full symmetry group, which is the conservative direction: a smaller group gives finer orbits and more branches, never fewer.
Each branch becomes a propositional formula over 462 primary variables with exact-cardinality constraints, and each is solved to UNSAT with a proof written out and replayed. 200 branches are closed by the twelve closure jobs below; the remaining 47 are the deepest nodes, each with its own certificate.
Every entry below is an UNSAT result whose resolution proof was written to disk in DRAT format and then replayed end to end by an independent checker, which reported s VERIFIED. Nothing in this table is asserted on the solver's word alone.
| Job | What it closes | Branches | Verdict | Proof sha256 |
|---|---|---|---|---|
| lb-c1042-8-deg3 | C(10,4,2) ≥ 9 — the one non-elementary input to the lower bound | — | UNSAT · s VERIFIED | ca55b356da9d… |
| r345-tail | Root orbits 3–5: a point-1 block outside orbits 0–2 is impossible | — | UNSAT · s VERIFIED | bb41db833e12… |
| r0s0-ter-tail | Tertiary orbits under root 0 / secondary 0 | 89 | UNSAT · s VERIFIED | 66e84117eb53… |
| r1-sec-tail | Secondary orbits under root 1 | 52 | UNSAT · s VERIFIED | d12afd05a16a… |
| r0-sec-tail | Secondary orbits under root 0 | 32 | UNSAT · s VERIFIED | 18a3a0dda5a1… |
| r2plus-b20 | Root orbit 2, no canonical-representative assumption | 19 | UNSAT · s VERIFIED | 22c5344b9732… |
| r1-gap-s6 | Root 1, secondary orbit 6 | 1 | UNSAT · s VERIFIED | 11da644e8642… |
| r1-gap-s7 | Root 1, secondary orbit 7 | 1 | UNSAT · s VERIFIED | 91e9500633b0… |
| r1-gap-s9 | Root 1, secondary orbit 9 | 1 | UNSAT · s VERIFIED | fe128269579c… |
| r1-gap-s10 | Root 1, secondary orbit 10 | 1 | UNSAT · s VERIFIED | a14c97b5a1bc… |
| r1-gap-s11 | Root 1, secondary orbit 11 | 1 | UNSAT · s VERIFIED | bc9e5bdb0d41… |
| r1-gap-s12 | Root 1, secondary orbit 12 | 1 | UNSAT · s VERIFIED | d4f7c611c52c… |
| r1-gap-s13 | Root 1, secondary orbit 13 | 1 | UNSAT · s VERIFIED | ab02b8bdbffb… |
| r1-gap-s14 | Root 1, secondary orbit 14 | 1 | UNSAT · s VERIFIED | c05b407317dc… |
| frontier nodes (47) | The 47 deepest branches, each refuted under the blocker catalogue | 47 | UNSAT · s VERIFIED | 47 separate certificates |
247 of 247 branches accounted for · 0 missing · 1,364,390,619 bytes of compressed DRAT retained · every CNF re-derivable byte-identically from its branch specification
An exhaustive computer proof is only as good as the things it assumes. Both lists are given in full.
The Schönheim bound is published. Applied recursively — through C(10,4,2) and C(11,5,3) — it puts C(12,6,4) at 40 or above.
J. Schönheim, "On coverings", Pacific Journal of Mathematics 14 (1964), 1405–1411.A 41-block covering design is constructed by simulated annealing. It has stood as the best known cover ever since, and is the design catalogued for (12, 6, 4) by the La Jolla Covering Repository.
K. J. Nurmela and P. R. J. Östergård, "Constructing Covering Designs by Simulated Annealing", Technical Report B10, Helsinki University of Technology, Digital Systems Laboratory, January 1993.The bracket 40 ≤ C(12,6,4) ≤ 41 remained the published state of knowledge. The La Jolla repository's table of improved lower bounds lists no entry for (12, 6, 4), and none for (11, 5, 3) either.
The 40-block case is refuted exhaustively. C(12,6,4) = 41.
A full write-up with the complete certificate manifests, the encoding, the symmetry audit and reproduction instructions is being prepared. This page is the summary, not the paper.
Until then, the honest description of this result is: proved and machine-checked end to end, independently replayed, not yet peer reviewed. If you find an error in it, that is exactly the kind of message worth sending.