Why 61 will never be enough

Picture 16 friends at a party. They want to take group photos. Every photo has exactly 5 friends in it, and a friend can be in as many photos as you like.

There is one rule. Pick any 3 of the friends. Those 3 must stand together in at least one photo. That has to be true for every group of 3 you could pick.

So here is the question. What is the smallest number of photos that follows the rule?

It sounds like a party game, but it is a real math problem, and a hard one. In 1997, a researcher named Rade Belić found a plan that uses 65 photos. Long before that, in 1964, a mathematician named Schönheim found a counting trick. It shows that you always need at least 61. Since 1997, the best known answer has been "somewhere from 61 to 65."

This new proof shows that 61 photos can never work. That moves the answer up. It is now 62, 63, 64 or 65. Nobody knows which one yet.

Why is this hard?

Let's count. You can make 560 different groups of 3 from 16 friends. One photo of 5 friends holds 10 of those groups. So you need at least 560 ÷ 10 = 56 photos.

But 56 is not enough, because photos overlap. When two photos share friends, some groups of 3 end up in both photos. That is wasted space. The hard part is knowing how much space has to be wasted.

Could a computer just try every plan? There are 4,368 different photos you could take. The number of ways to pick 61 of them is a number with 139 digits. A computer that checked a billion plans every second since the universe began would not even come close.

How the proof works

The proof uses two kinds of thinking.

First, careful counting. If 61 photos could work, there would be almost no wasted space. Counting shows that one friend would be in exactly 20 photos, and every other friend in exactly 19. The photos would have to follow a strict pattern, with almost no room to change anything.

Second, a computer search. The strict pattern cuts the whole problem down to just 4 cases. For each case, a computer program tried to finish the photo plan. All 4 times, it showed that the plan could not be finished. So no plan with 61 photos exists.

Can we trust the computer?

Computer programs can have mistakes in them, so this proof does not ask you to trust one. The program that searched did not just answer "no." It wrote down every step of its thinking, like showing your work in math class. Each of those write-ups is more than 13 million lines long.

Then a different program checked the steps. It is a checker that other researchers use for exactly this job, and it agreed with every step it needed. Two more programs that work in different ways also found no plan.

Who did the work?

Christopher Celaya, who runs the lab, led the project and checked the math. Coding assistants wrote the programs. A coding assistant is a computer program that writes code when a person tells it what to build. The checker then confirmed each of the four answers from the search.

Try it yourself

Here is a smaller version of the same puzzle. There are 7 friends. Each photo holds 3 of them. Every pair of friends must be in at least one photo together. What is the fewest photos you need?

Hint: 7 friends make 21 pairs. One photo of 3 friends holds 3 pairs. So you need at least 21 ÷ 3 = 7 photos. Can you do it with exactly 7?

The big puzzle works the same way, only bigger: 16 friends, photos of 5, and every group of 3 has to share a photo. With 7 friends you can check your plan by hand. With 16, nobody can, so the proof needed both careful counting and a computer.

Mathematicians call the friends points and the photos blocks. A plan in which every 3 points share at least one block of 5 is called a (16, 5, 3) covering, and the fewest blocks any such plan can have is the covering number, written C(16, 5, 3). This level keeps the friends and photos, but those are the words the paper uses.

Step 1: why at least 61

Pick any two friends and call them X and Y. Each of the other 14 friends has to be in some photo with both X and Y. A photo that holds X and Y has room for only 3 more people. So X and Y must share at least 14 ÷ 3 photos, which is about 4.67. Nobody can take two thirds of a photo, so round up: X and Y share at least 5 photos.

Now think about X alone. X has 15 other friends and shares at least 5 photos with each of them, so X needs at least 15 × 5 = 75 "photo partners" in total, counting repeats. Each photo with X in it gives X exactly 4 partners. So X is in at least 75 ÷ 4 = 18.75 photos, which rounds up to 19.

That is true for every friend. Sixteen friends in at least 19 photos each fill at least 16 × 19 = 304 spots. A photo has 5 spots, so there are at least 304 ÷ 5 = 60.8 photos, which rounds up to 61. This is the Schönheim bound, published in 1964.

Step 2: what 61 photos would force

Sixty-one photos have 61 × 5 = 305 spots, and the count above needs 304. So a 61-photo plan has exactly one spare spot. One friend, call them Z, is in 20 photos, and every other friend is in exactly 19.

Follow that one spare spot through the same counting, and everything locks into place:

• Every pair of friends shares either 5 or 6 photos.
• The pairs that share 6 photos form a fixed shape: Z paired with 5 friends, and the other 10 friends split into 5 pairs. The figure below draws it.
• Every group of 3 is in one photo or two, never three, and exactly 50 groups of 3 are in two.
• Take any friend other than Z, look only at that friend's 19 photos, and leave that friend out of each one. What is left is a plan for a smaller puzzle: 15 friends, photos of 4, and every pair together at least once. That smaller puzzle needs at least 19 photos, so these 19 are a smallest possible plan.

Step 3: only four ways to solve the smaller puzzle

In 1988, three mathematicians, Allston, Buskens and Stanton, showed that the smaller puzzle has exactly four different smallest plans, if two plans count as the same when one is just the other with the friends renamed. This project checked that again with two separate computer programs, and both found the same four. So any 61-photo plan has to contain one of those four patterns.

Step 4: four giant logic puzzles

Fixing one of the four patterns leaves a sharper question: can the remaining 42 photos be chosen so that every rule still holds? Each of the four cases was written as a giant true-or-false puzzle, the kind of problem called a satisfiability problem, or SAT for short. Each one has 144,553 true-or-false unknowns and 512,424 rules that tie them together.

A SAT solver, a program built to attack exactly this kind of puzzle, worked on each case for a few hours and proved that none of the four has a solution.

Step 5: checking the answer

A solver can have bugs, so each "no" came with a proof: a list of logical steps, 13.0 to 15.6 million lines long, that anyone with a computer and some patience can check. A separate, widely used checker called drat-trim went through every step it needed and reported VERIFIED for all four. Two other programs that work differently, CaDiCaL and a model built with Google's OR-Tools, also found no solution.

So a 61-photo plan does not exist, and C(16, 5, 3) is at least 62. The best known plan still uses 65 photos, so the true answer is 62, 63, 64 or 65.

What the small puzzle teaches

In the 7-friend puzzle, simple division gives the exact answer, 7, because a perfect plan exists in which every pair shares exactly one photo. In the 16-friend puzzle, division gives 56, but the true answer is at least 62. The difference is wasted space, and pinning down how much of it is unavoidable is the whole difficulty.

A (v, k, t) covering is a family of k-element subsets, called blocks, of a v-element set, such that every t-element subset lies in at least one block. The covering number C(v, k, t) is the least size of such a family. Taking complements, it equals the Turán number T(v, v − t, v − k), so the result can also be read as T(16, 13, 11) ≥ 62. The whole argument fits in six moves:

Notation

For a point x, a pair {x, y} and a triple T of a family ℬ of 5-subsets of a 16-set V, write r_x, λ_xy and μ_T for the number of blocks containing each, counted with multiplicity; r_x is the degree of x. The derived design at x is D_x = {B ∖ {x} : x ∈ B ∈ ℬ}, the r_x blocks through x with x deleted. If ℬ covers every triple, then D_x covers every pair of the other 15 points with quadruples, so it is a (15, 4, 2) covering.

The Schönheim bound, and why 61 is rigid

A pair lies in λ_xy ≥ ⌈14/3⌉ = 5 blocks, so 4r_x = ∑_y≠x λ_xy ≥ 75 and r_x ≥ 19. Summing degrees, 5|ℬ| ≥ 16 · 19, so |ℬ| ≥ 61. This is the Schönheim bound, L(16, 5, 3) = ⌈(16/5)⌈(15/4)⌈14/3⌉⌉⌉ = 61.

With exactly 61 blocks the degrees sum to 305 = 16 · 19 + 1, so one point z has degree 20 and every other point has degree 19. Put e_xy = λ_xy − 5. Then ∑_y e_xy = 4r_x − 75, which is 1 at every point except z, where it is 5. That forces the excess graph E, the pairs with λ = 6, to be a five-edge star at z plus a perfect matching of the other ten points. A second count over triples, ∑_w (μ_xyw − 1) = 3λ_xy − 14, shows that every triple is covered once or twice and that exactly 50 triples are covered twice.

For any x ≠ z, the derived design D_x has 19 blocks, so it is a minimum (15, 4, 2) covering; C(15, 4, 2) = 19 is classical, due to Mills. Its own pairs covered twice form a four-edge star plus a perfect matching of the remaining ten points.

Four classes of minimum (15, 4, 2) coverings

Every 19-block (15, 4, 2) covering has one hub of degree 6, and its doubly covered pairs form K_1,4 ∪ 5K₂. Fix that graph in a standard position. Isomorphism classes then become orbits of the group G of permutations that preserve it, of order 24 · 120 · 32 = 92,160: the four leaves of the star, the five matching edges, and the two ends of each edge can each be permuted.

Allston, Buskens and Stanton showed in 1988 that there are exactly four classes. Because the proof rests on that, the project derived it again with two programs that share no code. One enumerates the six blocks through the hub, and finds that exactly 4 of 206 configuration classes can be completed. The other solves the whole problem as an exact cover and finds 138,240 coverings in standard form, which split into G-orbits of sizes 23,040, 46,080, 46,080 and 23,040. Both give the same four classes, with automorphism groups of orders 4, 2, 2 and 4.

The reduction to SAT

Take a point a joined to z in E. Its derived design is a minimum (15, 4, 2) covering with hub z, so after renaming points it is one of the four representatives R₁ to R₄, with a = 1, z = 2, and the 19 blocks through point 1 fixed. What remains unknown is which four further points are joined to z, how the other ten points are matched, and the 42 blocks that avoid point 1.

Each case becomes a formula in conjunctive normal form, with one Boolean variable for each possible block (4,368), for each triple's "covered twice" flag (560), for each candidate star point (14) and for each candidate matching edge (91). The clauses say five things:

• The 19 known blocks are in, and every other block through point 1 is out.
• Every triple lies in one or two blocks, and its flag is true exactly when it lies in two.
• Exactly four star points are chosen.
• The matching is a perfect matching of the points that are not star points.
• Each pair lies in exactly four doubled triples if it is in E, and in exactly one otherwise.

The counting conditions are written with sequential counters, a standard way to express "at least j of these" in plain clauses. Each formula has 144,553 variables and 512,424 clauses, and the four differ only in the unit clauses that fix the 19 known blocks.

Solving and certifying

Each formula was solved by Lingeling, which records a DRAT proof: a list of clause additions and deletions that ends with the empty clause. Every added clause has to follow from the clauses present at that point by unit propagation, or more generally be a resolution asymmetric tautology. Additions of either kind preserve satisfiability, so a valid proof that reaches the empty clause shows that the formula has no satisfying assignment. drat-trim, run backward from the empty clause, checks only the steps the contradiction actually uses. It reported VERIFIED for all four, and every step in those verified cores was a plain unit-propagation step.

Two cross-checks agree, though neither is part of the proof. CaDiCaL 1.9.5 found all four formulas unsatisfiable in 1,045 to 1,255 seconds. A separately written CP-SAT model in Google OR-Tools 9.15, which shares the reduction but none of the encoding, reported all four infeasible in 1,623 to 2,089 seconds.

Checking the encoding

A proof checker certifies that a formula is unsatisfiable, not that the formula says what it was meant to say. So the encoder was audited on its own. The formulas regenerate byte for byte from the four representatives with a short script. The counter encoding was tested exhaustively on small cases. The star and matching clauses were checked against all 1,001 choices of the four star points, and against the 945 perfect matchings of the remaining ten points for each choice. Finally, 1,200 random assignments were compared constraint by constraint with the intended conditions, with no mismatches.

Statement and context

Theorem. There is no (16, 5, 3) covering with 61 blocks. Hence 62 ≤ C(16, 5, 3) ≤ 65; equivalently, T(16, 13, 11) ≥ 62.

The upper bound is Belić's 65-block covering from 1997, archived in the La Jolla Covering Repository; Bluskov obtained the same bound from the Steiner system S(3, 5, 17). The author knows of no earlier lower bound above the Schönheim value 61. General improvements do not reach it: the hypotheses of the Mills and Mullin improvement fail for these parameters, and the bounds of Horsley and Singh do not exceed 61.

Structure of a putative 61-block covering

• The blocks are distinct, since deleting one copy of a repeated block would leave a 60-block covering.
• A unique point z has r_z = 20, and r_x = 19 for every x ≠ z.
• λ_xy ∈ {5, 6}, and E = {{z, a} : a ∈ A} ∪ P with |A| = 5 and P a perfect matching of M = V ∖ (A ∪ {z}). E has ten edges and no triangle.
• μ_T ∈ {1, 2}. A pair outside E lies in exactly one doubled triple and a pair in E in exactly four, so 3D = 110 + 40 and there are D = 50 doubled triples; as a check, 10 · 61 = 560 + 50.
• For x ≠ z, D_x is a 19-block (15, 4, 2) covering whose doubled pairs form a star K_1,4 centred at the neighbour of x in E, plus a perfect matching of the other ten points. For a ∈ A the hub of D_a is z.
• Not used in the proof: the doubled triples through z form a graph X_z on V ∖ {z} with degree 4 on A and 1 on M, and if it has n₂ edges inside A then 5 ≤ n₂ ≤ 10.

Theorem 4.2, obtained three times

Only completeness is used: every 19-block (15, 4, 2) covering is isomorphic to one of R₁ to R₄, the designs Allston, Buskens and Stanton call D2, D1, B4 and B3, with |Aut| = 4, 2, 2 and 4.

Computation 1 classifies hub-block sets by coloured graphs (Γ_L, Γ_M) on the six hub blocks. There are 1,335 labelled leaf graphs in eight isomorphism classes, giving 206 classes. A depth-first search over the 13 non-hub blocks, branching on the pair with fewest candidates, completed all 206 searches with 31,989 nodes in total and extended exactly four classes, with 12, 4, 2 and 96 completions. The stabilizers have orders 48, 8, 4 and 384 and act transitively on each set of completions. A separate program replayed every search tree, and CP-SAT recounted the same 114 completions.

Computation 2, written without reference to the first, solves the exact cover problem directly: nine excess pairs covered twice and the other 96 once. Two depth-first searches with different branching rules find N = 138,240, as does a CP-SAT enumeration over representatives of the 206 G-orbits of the 5,745,600 labelled hub-block sets. The 92,160 elements of G split the coverings into orbits of sizes 23,040, 46,080, 46,080 and 23,040.

The reduction is exact

With a ∈ A relabelled to 1 and z to 2, the formula F_i fixes the 19 blocks through 1 to {1} ∪ R for R ∈ R_i. With ε_Q the constant or literal expressing Q ∈ E, its constraints are (C1) the unit clauses for the blocks through 1; (C2) 1 ≤ ∑_B⊇T x_B ≤ 2 for every triple, with d_T true if and only if the sum is at least 2; (C3) exactly four a_v; (C4) the matching conditions on the m_uv; and (C5) ∑_T⊇Q d_T = 4 when ε_Q holds and 1 otherwise.

Neither |ℬ| nor the pair multiplicities are written into F_i; they are implied. From (C3) and (C4), E has 1 + 4 + 5 = 10 edges, so (C5) gives 3D = 150, and (C2) gives 10|ℬ| = 560 + D = 610. Also 3λ_Q = 14 + 1 + 3[ε_Q], so λ_Q = 5 + [ε_Q] and r₂ = 20. Hence F_i is satisfiable if and only if there is a 61-block covering whose blocks through 1 are {1} ∪ R for R ∈ R_i and whose point of degree 20 is 2.

The cardinality conditions in (C2) and (C5) use a two-sided variant of Sinz's sequential counter: three registers over the 78 block variables of each triple, and five over the 14 doubled-triple variables of each pair. (C3) uses PySAT's sequential counter, and the at-most-one conditions of (C4) use the pairwise encoding.

What the proof relies on

Reproducing the result

• The four formulas and DRAT proofs, about 32 GB uncompressed, with SHA256 checksums, the search trees of Computation 1 and instructions for checking the proofs, are archived on Zenodo at doi:10.5281/zenodo.23191655.
• Code, solver records and drat-trim logs are in celaya-solutions/covering64 under CC BY 4.0. The SAT computations are those of commit fd7adc2; the classification and encoder checks added for the paper are in commit d490808.
• Computation 1 is in experiments/2026-10-03/link-hub-independent, Computation 2 in experiments/2026-10-06/reclassify-15-4-2, the isomorphisms from the 1988 designs in experiments/2026-10-03/literature-and-novelty, the encoder in experiments/2026-10-05/lb61-certified and its audit in experiments/2026-10-06/lb61-encoder-audit.
• paper/anc/gen_cnf.py writes the four formulas from the representatives without solving them, byte for byte when run with python-sat 1.9.dev15, since the bytes depend on its variable numbering. paper/anc/SHA256SUMS.txt lists the checksums of every formula and proof.
• Toolchain: PySAT 1.9.dev15; Lingeling bbc-9230380-160707, the SAT Competition 2016 version bundled with PySAT; drat-trim commit 2e3b2dc in backward mode with -t 1000000; CaDiCaL 1.9.5; OR-Tools 9.15.

What is open

C(16, 5, 3) is now known to be 62, 63, 64 or 65. Part of the method carries over to more blocks. For any (16, 5, 3) covering with b blocks, the identities of Section 3 give ∑ (λ_xy − 5) = 10b − 600 and ∑ (r_x − 19) = 5b − 304. At b = 62 at most six points have degree above 19, so at least ten have degree 19, and their derived designs are again isomorphic to one of R₁ to R₄. What is lost is the forced excess graph: at 62 blocks the counting allows many degree sequences and excess graphs, so the analogous case split would be considerably larger. From the other side, a covering with fewer than 65 blocks would lower the upper bound. The repository's research log records searches in that direction; they are outside the paper and not part of its claims.

Where this sits

Computer-assisted determinations of covering numbers have a history. Margot settled C(10, 5, 4) = 51 by branch-and-cut with isomorphism pruning, and Applegate, Rains and Sloane did so independently and determined several more. SAT solving with independently checkable proofs settled the Boolean Pythagorean triples problem and Keller's conjecture in dimension seven. The closest precedent is Krug's recent proof that C(12, 6, 4) = 41, by the same overall strategy: counting forces the structure of a putative smaller covering, every derived design is an optimal covering of smaller parameters, and the remaining cases are refuted by a SAT solver with certified proofs.

The full paper is on this site as a web page and as the original PDF. The code, the solver records and the proof-checking logs are on GitHub, and the formulas and proofs themselves are on Zenodo.