Thirty-Two 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(32) ≤ 6. The work is the other direction.

Everything rests on checking the property in the theorem for every placement of a unit square, a three-parameter continuum. That check is exact and exhaustive, and it was done twice, by two checkers written independently (§04). It was then done a third time inside the kernel of the Lean 4 proof assistant, which proves s(32) = 6 with no hypothesis left over (§05).

Exact values of s(n) are rare. Just below a perfect square k² the answer is known to be k for k² − 1 and k² − 2 (Nagamochi 2005), and for k² − 3 when 3 ≤ k ≤ 7 (Bentz 2010, and a 2016 preprint). With four squares missing, the only known value was s(5) = 2 + 1/√2 (Göbel 1979), where tilting beats the grid. From k = 4 on the grid is conjectured optimal, and nothing was proved: not s(12), s(21), s(32) or s(45). Friedman's survey conjectures that once s(k² − c) = k holds for one k, it holds for every larger one. If that is right, s(32) = 6 would carry on to s(45) = 7, s(60) = 8, and so on.

The classical tool is an unavoidable set: points that every unit square must hit. For k² − 4 squares it would need k² − 5 points, and a lattice that sparse leaves gaps a square can slip through. Weights solve the counting problem. They make a harder checking problem, and exactness costs one more thing. A smooth density can never certify side 6 exactly: each of the 36 grid cells would have to carry weight 1 on its own, 36 in all. The weight has to sit on the grid lines, where neighbouring cells share it.

The cover was found by linear programming over sampled placements, with points added where the worst placement fell short, and then closed up until no placement tested in a fine scan captured less than 1. The converged LP value is about 31.22, so there is 2.4% of room below 32; s(21), the previous rung, had only 1.3% and could not be closed with points; it was closed later by spreading part of the weight evenly along the grid lines (s(21) = 5). Every number in the file is an integer: coordinates in thousandths, weights in units of 10⁻¹¹.

Symmetry first. The cover is unchanged by all eight symmetries of the square (checked exactly, weights included). So it is enough to check squares whose centre lies in the quarter [0,3]² and whose angle lies in [0°, 45°]. The checkers take a little more, angles up to 53.13°, which keeps the parameter u = tan(θ/2) in [0, ½].

Then exhaustion, at margin zero. That region is cut into root boxes of placements, and each box is subdivided until the checker can prove, in exact rational or integer arithmetic, that every placement in the box captures weight at least 1. Near the tiling that is tight: a square sitting exactly on a grid cell captures points only on its own edges, so there is no slack to spend. Most boxes are proved disjunctively ("either these points are inside, or those are"). The s(13) write-up explains the method, used there on a cover of side 4.

zeromargin.py alone covers the whole region. zmcheck, a separate program in another language sharing no code with it, gets within five root boxes. The holdouts sit at the hardest spots: placements within 0.003 of an interior tile centre, tilted less than 0.56°, where all four edges lie on grid lines at once. A second cover, s32_shift_v1.txt (total 31.698), is certified completely by both checkers, zmcheck using a different (opt-in) branch order.

Checking the checkers. Before publishing, a fresh review traced every step where the fast path accepts a box and confirmed each is an exact test. A self-check mode, which runs the slow all-Fraction reference beside the fast path at every call, reproduced the shipped results root for root. Three deliberately broken covers were also tried, each keeping the symmetry: a corner orbit removed, a tile-centre orbit removed, and orbits removed so that one square at 52° captures less than 1. All three were refused.

$ certificates/s32/verify.sh
s32_closed_cover_6.txt: OK   ...
lean/Sqpack/S32Data.lean matches certificates/s32/s32_closed_cover_6.txt (sha256 a0d2d38f…2144)
region: 7200 roots = [0,3]^2 x u in [0,1/2]; present 7200, missing 0, with uncertified boxes 0, ...
totals: boxes 164130, max depth 27, leaves ADM 12201 P1 0 MIX 0 CHAIN 70007 EMPTY 3457 UNCERTIFIED 0
D4 RECHECK CLEAN: every root of the D4 region certified

theorem s32_checkerCover : S32CheckerCover
theorem s32_eq_6 : minSide 32 = 6

In Lean 4 with Mathlib, minSide n is the infimum of the sides that hold n closed unit squares at arbitrary positions and angles with disjoint interiors: the usual s(n). Lean proves the grid packing, the scaling argument, the symmetry reduction, and the symmetry and total weight of this cover, which is transcribed into Lean from the certificate file (S32.lean).

That file proves minSide 32 = 6 from one hypothesis, S32CheckerCover, the region statement: every closed unit square in [0,6]² with centre in [0,3]² and angle 2·arctan u, u ∈ [0,½], captures weight at least 1. That is exactly what the checker runs of §04 establish. S32Lower.lean now proves the hypothesis itself: a generated tree of pose boxes, about 6,000 chunks, each decided by the kernel (decide +kernel) against a small verifier whose soundness is proved once, for every tree (ZMTree.sound, the zero-margin verifier also used for s(13) = 4). The program that builds the tree is not trusted: a wrong tree only makes the check fail. So the whole covering property is checked inside Lean's kernel, and s32_eq_6 has no hypothesis.

What remains trusted is Lean's kernel, Mathlib, and the definitions in the statement (minSide and what a packing is). No sorry, no native_decide; #print axioms gives only propext, Classical.choice, Quot.sound. The check is heavy, so it is opt-in and not part of the default build:

$ lean/scripts/gen_data.sh S32Z                                 # generate the tree, ~70 min on 4 cores
$ lean/scripts/build_parts.sh S32Z Sqpack.S32Lower 4             # 13.8 CPU-hours, ≤ 15 GB per process

• This is a computer-assisted proof and has not been peer reviewed. The covering property is checked by two independent programs and by Lean's kernel; the Lean statement rests on the definitions of minSide and of a packing, which are short and open to inspection (lean/Sqpack/S32.lean).
• "First exact s(k² − 4) for k ≥ 4" rests on our literature search (journals, arXiv, the Friedman/Ellsworth catalogue, and the 2026 certificate repositories). If we missed one, please tell us.
• Nothing here settles s(12). There the same approach runs out of room: see the s(12) write-up, where the proven floor stands at 3.9686. (s(21) and s(45) have since been settled with line densities: s(21) = 5 and s(45) = 7.)

Everything is in s12/certificates/s32 of evand/square-packing. certificates/s32/verify.sh re-checks in seconds, re-running two germ roots; --full re-runs the whole sweep for both covers, about 5 CPU-hours. CI runs the fast check on every change.