C(24,14,4)≥ 20

Covering designs · Lean 4

C(24,14,4) ≥ 20

Pick blocks of 14 points out of 24 so that every set of 4 points sits inside some block. How few blocks can do it? The best known answer is 23. For decades the best lower bound was 19 (Schönheim 1964, Mills 1979). A Lean proof, written by AI agents and checked by Lean’s kernel, shows that 19 is impossible. Read the blog post for background info.

Checked by Lean’s kernelRegistered on PalomarNot yet peer-reviewed

Try it

Cover every four-point set

Each row is a block: 14 of the 24 points, shown as filled cells. A set of four points is covered if some row contains all four. There are 10,626 four-point sets. Click cells to move points around, or let the computer search.

BlocksProved impossible
block123456789101112131415161718192021222324sizebest
14
14
14
14
14
14
14
14
14
14
14
14
14
14
14
14
14
14
14

264

four-point sets not covered

This is the best arrangement a computer search found. It still misses 264 sets.

A covering needs 0. The Lean proof shows that no arrangement of 19 blocks gets there, so at least 20 are needed.

The proof in eight parts

  1. 1Counting: every point is in at least 11 blocks, every pair in at least 6.
  2. 2With 19 blocks, all but one or two points are in exactly 11.
  3. 3A rank bound finds balanced groups of points.
  4. 4Regular 11-block coverings of 22 points are rigid: doubled designs.
  5. 5So there is a balanced quadruple, or one exceptional shape.
  6. 6A quadruple leads to the Petersen graph and a colour clash.
  7. 7The exceptional shape needs 18 pairs of blocks, out of 15.
  8. 8Both fail: no covering with 19 blocks.

What changes

The covering number C(v,k,t) is the fewest k-point blocks that cover every t-point subset of v points. The new bound feeds the standard Schönheim inequality and lifts four more tabulated lower bounds.

Covering numberOld lower boundNew lower boundBest known coveringStatus
C(24,14,4)192023Checked by Lean
C(25,15,5)323442Checked by Lean
C(26,16,6)525678By hand, from the line above
C(27,17,7)8389143By hand, from the line above
C(28,18,8)130139258By hand, from the line above
ReadThe proof in eight stepsCounting, a rank bound, a rigid design and the Petersen graph, with interactive figures.InspectThe Lean resultsThe main theorems with their exact statements, plus a guide to the agents’ naming.CheckWhat’s been verifiedWhat Lean, Comparator and Palomar check, and what nobody has checked yet.

Still open

Nobody knows whether C(24,14,4) is 20, 21, 22 or 23. The search that led here was looking for a covering of all 5-point subsets of 25 points with 41 blocks of 15. None has been found, and none has been ruled out. The code is on GitHub.