$n=32$$n=32$

$s(32)$$s(32)$ — solved

$s(32)=6$$s(32)=6$. Established by a weighted closed cover with an exact exhaustive check, Daniel (2026), building on Burns’s and Massaccesi’s weighted exact-rational covering method. The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction. It is the first exact value this record holds for a case of the form k2−4$k^2-4$ with $k\ge 4$$k\ge 4$; the source’s own literature search found none either.

The packing

The upper bound is trivial: the $6\times 6$$6\times 6$ grid holds 36 unit squares, so it holds 32 with four cells empty, and $s(32)\le 6$$s(32)\le 6$. The record catalogue does not picture $n=32$$n=32$, and no arrangement below side 6 has ever been found. What is new is that none exists.

The lower bound

The certificate is 13,085 rationally weighted points of [0,6]2$[0,6{]}^2$, total weight 3171350535386/1011=31.713505354<32$3171350535386/{10}^{11}=31.713505354<32$, such that every closed unit square inside [0,6]2$[0,6{]}^2$, at every centre and every angle, captures weight at least $1$$1$, a point on its boundary counting. If 32 unit squares fit in a side $s<6$$s<6$, scaling by $6/s$$6/s$ gives 32 squares of side above 1 with disjoint interiors in [0,6]2$[0,6{]}^2$, each strictly containing a concentric closed unit square. Those 32 closed unit squares are pairwise disjoint, so they would capture at least 32 from a total of $31.71$$31.71$.

The margin is exactly zero at the container itself, where the grid’s tiling squares share their boundary points with the cover, so no angle net can decide it. The source’s checker zeromargin.py subdivides pose space exactly instead, over the fundamental region of the cover’s exact D4 symmetry, and certifies every one of its 7,200 root boxes with no uncertified leaf. A second, separately written checker, zmcheck, certifies 3,595 of its own 3,600 roots; the five it leaves open are interior tile germs, which zeromargin.py closes. Among the two earlier exact checkers, this cover has one complete certification and 99.86 % of a second; the source’s other cover, s32_shift_v1.txt, which proves the same theorem but is not the one in Lean, is certified completely by both checkers. A Lean theorem, s32_eq_six_of_checker, derives minSide 32 = 6 from the single hypothesis that zeromargin.py run checks; the checker programs are not formalised.

The verified field rests on two complete replays here, and stands at V3/C3. The first is of that exhaustive run (E-n032-evand-closed-cover-source-run): the same runner, checker, certificate and settings, run in four legs on 27 September, certify all 7,200 roots with the source’s totals: 164,130 boxes, maximum depth 27, and no uncertified leaf, the one root that needs depth 30 closing there. Every per-root record carries the census of the source’s record of the same root, box for box, and the records are retained in the packet’s receipts. The review of 27 September read the Lean statement, the reduction and the checker’s exact paths and found no mathematical defect. The second, on 29 September, is of the source’s third checker, zmx2, run with --pair-points over the same D4 region: it certifies all 3,600 of its roots with no uncertified box (1,405,342 boxes, maximum depth 29), its totals equal to those the source reports (E-n032-evand-closed-cover-zmx2-replay). zmx2 is a second implementation of the same pose-space subdivision, by the source’s own agent. It closes germs its own way, by a pair lemma and a pair dynamic programme over lines one unit apart where zeromargin.py uses monotone chains, and it decides by exact integer tests on outward-rounded binary64 enclosures of chord ends rather than in exact rationals, so it assumes correctly rounded binary64 arithmetic on the host. Its point test derives from zeromargin.py’s: on 1 October the source stated that zmx2’s author was permitted to read zeromargin.py. Without the flag --sym-atoms the fold cannot be taken out of zmx2’s side: run here with --full --pair-points over the cover and its mirror, no symmetry assumed, zmx2 leaves 152 boxes uncertified, 38 in each of the four reflected images of one germ at an edge cell’s centre, at angles under a third of a degree, where the float mass is at least $1.0115$$1.0115$. They are not counterexamples (receipt). The source’s Lemma A, which bounds each box with both assignments of points to lines, closes them: on 2 October zmx2 --full --pair-points --sym-atoms, built from the checker source that made the source’s run, certified all 28,800 roots of the whole pose space here, 11,268,760 boxes with none uncertified, every root’s census equal to the source’s (E-n032-evand-zmx2-full-sym-replay; packet). With that run the two checkers no longer share the D4 fold, the region or any symmetry premise. They still share the author and agent, the point-in-square formulation, the pose parametrisation and the branch-and-bound architecture, which are the common mode, so they are separately written and not independent. The two entries differ in method, so the result shows two machine methods beside its C3. The run was retained with the 28 September packet and recorded as evidence on 29 September, after the author’s registration request in jlevy/squares#238. This repository’s parent-core route cannot supply a method of its own: it proves strict bounds through shrunken cores, and at side 6 the thirty-six grid cells defeat any such threshold. The Lean build and the zmcheck sweeps were not run here.

The source gives Hosono’s rectangle-density $119/20=5.95$$119/20=5.95$ as the previous lower bound. Before 2026 it was Nagamochi’s general closed form, 1+23​≈5.795831$1+\sqrt{23}\approx 5.795831$. Corrected 2 October 2026: that closed form is now a reported bound, its published proof resting on Nagamochi’s Lemma 1, which Karakuş showed false (review). This register had recorded that proof as verified, its own error, logged as defect D-516.

Verification Code

The programs behind this case’s verified bounds, by their evidence. The code column says how the code that ran stands to the code its producer used. VERIFIERS.md says what each program is and whose it is.