Twenty-One Squares

s(n) is the side of the smallest square that holds n unit squares, each at any position and any angle, overlapping at most along their edges. Leaving cells of a grid empty gives s(21) ≤ 5. The work is the other direction.

This is the second exact value of s(k² − 4) for k ≥ 4, after s(32) = 6. As there, everything rests on checking the property in the theorem for every placement of a unit square, a three-parameter continuum. That check was done twice, by two checkers written independently (§04), and Lean 4 assembles the proof (§05).

With four squares missing from a k × k grid, the only value known before 2026 was s(5) = 2 + 1/√2 (Göbel 1979), where tilting beats the grid. For k = 5 the lower bounds climbed quickly in September 2026, from several directions, and stalled just short of 5:

The method is the one behind s(32) = 6: find weights such that every unit square in the container captures weight at least 1, with total below n. For side 5 exactly, with points only, it did not work. The linear program that chooses the weights converges to about 20.74, comfortably below 21, but a program can only look at finitely many placements, and the weights it returns always let some unsampled placement capture a little less than 1. Repairing that costs weight. For s(32) the repair cost about 1.6% and there was 2.4% of room. For s(21) the best point covers needed 1.4% of repair and there was 1.3% of room: the best point cover the repair loop produced cost about 21.02.

Where do the stubborn placements sit? Almost all of them are squares lying nearly on a cell of the grid, tilted by an angle of about a thousandth of a radian. At exactly zero tilt such a square has all four grid lines of its cell on its boundary and gets all of their weight. Tilt it slightly and each edge swings off its line, pivoting about some point. On the left line it keeps the part above the pivot; on the right line, one unit away, the matching edge keeps the part below the same height. Where the pivot falls depends on the ratio of offset to angle, so it can be anywhere.

If the weight on the lines sits on discrete points, the captured amount is a step function of where the pivot falls, and some pivot position always lands between steps: a hole. The linear program patches one hole and opens another. If instead the weight is spread evenly along the lines, the two partial edges add up to a whole edge whatever the pivot, and there is nothing to slip through. With piecewise-constant densities the captured amount near a tilted cell becomes a piecewise-linear function with finitely many corners, so a finite set of test placements pins it down completely.

Spreading weight out is not new in itself: the rectangle-density certificates of tokoharu and wand125 spread it evenly over rectangles. The difference here is that the density is one-dimensional and sits on the grid lines themselves, mixed with ordinary points, which is what a proof at exactly side 5 needs.

The effect is large. The repair cost over the linear program fell from 1.4–2.9% to 0.04–0.15% (for side 4 and side 5 alike), while the program's own value hardly moved. Everything left over is an ordinary tilted placement of the kind the closing loop handles routinely.

The weights came out of the linear program at about 1.0025× its confirmed minimum and were then multiplied by a further 1.003, to leave the exact checkers some room: 20.83 became 20.89, still 0.5% below 21. Every number in the file is an integer: coordinates in thousandths, masses in units of 10⁻¹¹.

Symmetry first. The distribution is unchanged by all eight symmetries of the square (checked exactly, points and segments). So it is enough to check squares whose centre lies in [0,2.5]² and whose angle lies in [0°, 45°]; the checkers take angles up to 53.13°, so that u = tan(θ/2) runs over [0, ½]. One of them also checks the whole pose space with no symmetry assumed.

Then exhaustion, at margin zero. The region is cut into boxes of placements, and each box is subdivided until the checker can prove that every placement in it captures mass at least 1. Points are handled much as for s(32). For the lines, the checkers use the same observation as the cover: for two parallel grid lines one unit apart, one pivot height governs both at once, so the pair's mass is bounded below by a minimum over that single height of an explicit piecewise-linear function, computed exactly. That is what lets the boxes around a nearly untilted cell close after a handful of subdivisions; without it, thousands stay open.

zmx2 was written separately, from the statement of the problem alone, without seeing zm_mixed.py or its write-up; it has its own parser, its own proofs and its own arithmetic. Both checkers certify the cover completely. With every mass scaled down by 0.6% the cover is refused by zmx2 exactly at its known weakest tilted placement (centre (0.574, 1.441), angle 9.2°, exact mass 0.99969), and zm_mixed.py, run around that placement, leaves it open.

Checking the checkers. A fresh adversarial review re-derived every lemma of zm_mixed.py against its code and found no gap. It then tested each certified component of the bounds, not just the total, against the exact mass at about 115 million adversarial rational placements on this cover, with no violation and several bounds that were exactly tight. It also made three deliberately broken versions of the cover: one with a tilted dip below 1, one in the hardest tilted cell, and one with a hole at a pivot that exists only at positive tilt. Each was refused, with the exact hole inside a box the checker left open. zmx2 has its own tests (holes refused at the right placement, an exact rational harness, agreement with the point checkers on the published s(13) and s(32) covers) and a separate review.

$ certificates/s21/verify.sh
cover: ... 7536 points, 1872 segments (1872 axis-parallel), 0 polygons; all in [0,5]^2, masses >= 0
total = 522368729933/25000000000 = 20.894749197320  (< 21: True)
lean/Sqpack/S21Data.lean matches certificates/s21/s21_mixed_cover_5.txt (sha256 8b415cee…fc23)
zm_mixed D4 RECORDS CLEAN: every root of the D4 region certified
VERIFIED: every closed unit square in [0,s]^2 has mu >= 1 (unreduced sweep, all roots)
s(21) bundle: OK

theorem s21_eq_five_of_checker (h : S21CheckerCover) : minSide 21 = 5

minSide n is the same Lean definition as for s(32): the infimum of the sides that hold n closed unit squares at arbitrary positions and angles with disjoint interiors. New here: the scaling argument for any measure, not just finitely many points; the symmetry reduction for measures; the measure of a segment as the even spread of its mass; and the symmetry and total of this cover, transcribed from the file. Standard axioms only, no sorry, no native_decide.

The one hypothesis, S21CheckerCover, says that every closed unit square in [0,5]² with centre in [0,2.5]² and angle 2·arctan u, u ∈ [0,½], captures mass at least 1: the points inside it plus, for each segment, its mass times the fraction of the segment inside it. That is what both checkers establish. The checker programs themselves are not formally verified.

For s(32) = 6 and s(13) = 4 the corresponding hypothesis has since been proved inside Lean's kernel, by a verifier for pose-box trees whose soundness is proved once. That verifier handles weighted points only. Extending it to segments, which would do the same for this cover and for s(45) = 7, is future work; until then s(21) = 5 rests on the two checkers for the covering property.

• This is a computer-assisted proof and has not been peer reviewed. The claim is only as good as the two checker programs, which are open to inspection and re-running.
• zmx2 is not purely rational. It works out where a grid line crosses the edges of a rotated square in IEEE-754 double-precision interval arithmetic, rounding every operation outward. Its verdict is rigorous provided the processor and compiler round + − × ÷ √ correctly, which IEEE-754 requires and Rust does not undo. zm_mixed.py uses exact rationals throughout, so the two rest on different kinds of trust.
• The lower bounds in §02 from 2026 are unrefereed, like this one.
• Nothing here settles s(12) (the s(12) write-up). The same line-density method has since given s(45) = 7, checked by the same two checkers, with no Lean yet.

Everything is in s12/certificates/s21 of evand/square-packing. certificates/s21/verify.sh re-checks in about a minute, including a fresh zmx2 run over the whole pose space; --full also re-runs zm_mixed.py, about 20 CPU-hours. CI runs the fast check on every change.