Three Short of a Square

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. The grid gives s(k² − 3) ≤ k. The work is the other direction, and here it is done for all k ≥ 6 at once.

The same measure is used for every k: four fixed corner pieces, a band along each wall that repeats with period 1, and plain area inside (§03). The saving 4D = 3.388970 sits at the four corners and does not depend on k, so the room below k² − 3 is 0.388970 for every box. Checking the property in the theorem for k = 7 is enough for all k ≥ 6: that step is proved in Lean (§05). The check for k = 7 itself was done by one exact program (§04).

Nagamochi (2005) stated s(k² − 2) = s(k² − 1) = k for every k ≥ 2; his published proof has a gap, and both have since been proved without it (below). With three squares missing the answer was known only case by case. Friedman's survey (1998) conjectured that s(n² − k) = n implies s((n+1)² − k) = n + 1, which together with s(6) = 3 (Kearney and Shiu, 2002) would give s(k² − 3) = k for all k ≥ 3. Bentz, having proved s(13) = 4 and s(46) = 7 (2010), stated that s(m² − 3) = m should hold for all m ≥ 3, and proved m = 5, 6 in an arXiv preprint (2016). (k = 2 is not a case: s(1) = 1.)

So the cases k ≥ 8 were open until this month: David Ellsworth's Squares in Squares lists 6, 13, 22, 33 and 46 as proved and nothing for 61 or 78, and jlevy/squares lists "Can Bentz's method prove s(61) = 8?" as an open question (H-033, 2026-08-24). Since s never decreases, s(k² − 4) = k implies s(k² − 3) = k, so our s(21), s(32), s(45) and s(60) results each settle a case too. With them and our case-free s(13) = 4, none of k = 4 … 8 depends on Bentz's proofs, though his came first.

Bentz's proofs and our covers for s(45) and s(60) are one box at a time: each needs its own certificate, and the effort grows with the box. A proof for every k needs something that does not grow. Nagamochi's argument for k² − 2 is of that kind (and so is chelokot's repair of it, below): resources along the walls and at the corners, in a fixed pattern, saving 2 in every box. For k² − 3 the saving must exceed 3, that is, more than ¾ per corner. A float linear program over patterns of this shape found about 0.945 per corner; the exact family here has 0.847.

Two short: s(k² − 2) = k without Nagamochi's Lemma 1. Nagamochi's proof scores every square against a fixed pattern of resources, and his Lemma 1 asserts that each square scores more than 1. That lemma is false. chelokot gave a Lean-checked counterexample (a square of side 1.0001 in [0,4]² scoring 0.9775) and a kernel-checked replacement proof of s(k² − 2) = k for every k ≥ 2 (chelokot/square-packing-archive, September 2026). Hakan Karakuş (arXiv:2609.37410, 29 September 2026) gives a family of counterexamples near a corner of every rectangle with sides a > 3, b > 2, and concludes that the published proof of the rectangle bound is incomplete, not that the bound is false. He re-proves s(k² − 1) = k with a weaker rectangle bound, and states that his argument does not establish s(k² − 2) = k.

Our certificates give a further route that uses neither Lemma 1 nor any rectangle bound. Since s never decreases, s(k² − 3) ≤ s(k² − 2) ≤ s(k² − 1) ≤ k, so s(k² − 3) = k implies s(k² − 2) = k. That gives:

• k ≥ 6 from this family. For k ≥ 9 it is the only one of our results that applies, so there the statement rests on the single-checker certificate of §04. k = 6, 7, 8 also follow from s(32) = 6 (kernel-checked in Lean with no hypothesis), s(45) = 7 and s(60) = 8;
• k = 5 from s(21) = 5, and k = 4 from s(13) = 4 (kernel-checked in Lean with no hypothesis);
• k = 3: s(7) = 3 follows from s(6) = 3 (Kearney and Shiu, 2002), and El Moumni (1999) proved it directly; k = 2: s(2) = 2 is classical (Göbel, 1979).

Like the rest of this page, this is unrefereed.

The measure is built from three parts, each on the grid of pitch 1/5, with no weighted points at all:

• Corner modules on the 2 × 2 square at each corner: 36 pieces of mass spread along 1/5-segments, plus area density on [9/5, 2]². The same module, reflected, at all four corners.
• A periodic wall band of width 2 along each wall, between the corner modules: 52 segment pieces per unit period, plus area density on the strip from 9/5 to 2. It repeats with period 1, however long the wall is.
• Lebesgue interior: mass equal to area on [9/5, k − 9/5]². A unit square wholly inside it captures exactly 1.

Why the saving is 4D in every box. Each period of the band carries mass exactly 2, its own area, so the band neither costs nor saves anything as the walls get longer; nor does the interior. Everything saved is saved at the corners, D at each, and the total is k² − 4D for every k ≥ 6.

Why one box is enough. A unit square is less than 2 wide in each direction at any angle. So along each axis it can be moved by a whole number of units into [0,7], avoiding the places where the pattern changes (the ends of the band, the edges of the interior). After the move it sees exactly the same mass in the 7 × 7 box as it did in the k × k one. So if every unit square in the 7 × 7 box captures at least 1, so does every unit square in every larger box, and in the 6 × 6 box too. (A 6 × 6 box on its own would not be enough: a tilted square near a wall cannot always be moved without crossing a corner module.)

Zero margin, along the walls. Because the band's saving is exactly zero, there is no slack along it: the axis-parallel square [t, t+1] × [0, 1] resting on a wall captures exactly 1, for every t, and so does the one a row above it along most of the wall. In the corners, some limits as the tilt goes to zero, with the square's edges on grid lines, are exactly 1 too. Away from these, the linear program that chose the masses was made to demand growth in proportion to the tilt angle (with factor 0.2, scaled by the part of the square outside the interior), so that nothing else is tight. That demand cost about 0.06 of D; the whole price of exactness, from the float optimum 0.945 to 0.847, was about 0.1 per corner. It leaves 0.097 per corner above the ¾ needed.

All masses are rationals with denominators at most 10¹²; the files list them exactly.

The claim to check is that every closed unit square in [0,7]², at every position and angle, captures mass at least 1 under μ₇. The measure is unchanged by the eight symmetries of the square (checked exactly), so it is enough to take centres in [0, 7/2]² and angles up to 45°; the checker takes angles up to 53.13°.

At zero tilt the captured mass is, piece by piece, a product of linear functions of the centre, so its minimum is attained at finitely many one-sided limits. All 900 of them were computed exactly: the minimum is exactly 1, reached at 188.

At positive tilt a box checker subdivides the space of placements until every piece is proved. Most pieces close with the bounds of zm_mixed.py, the checker behind s(21), s(45) and s(60), imported, with one guard added after review. The places where the mass is exactly 1 need more, because a bound that loses anything at all can never reach 1 there. The new ingredient is an exact lemma: on a box of placements, for each tilt, the mass is bounded below by a function that is concave on the cells of an arrangement of lines in the plane of centres, so its minimum is at a vertex; the checker evaluates it at every vertex as an exact rational function of the tilt and proves it is at least 1. At a tight placement the bound is the exact value, with nothing lost. Two further lemmas handle squares inside or just poking out of the area-density square.

This is the run of record (2026-09-29). It repeats an earlier full run with the same result root for root, and adds a record of every leaf so that any piece of the proof can be re-checked on its own.

It caught a real error. The first exact solution of the linear program was not valid: at one corner, in the limit as the tilt goes to zero, a square near [1,2]² captured 0.999936. The float program had missed it, because its containment tolerance over-counted mass at tiny tilts. The checker refused exactly the two boxes of placements that contain the bad limit. Adding the exact limits to the linear program fixed it, at a cost of 10⁻⁵ in D; the rejected cover is kept as a test. Covers deliberately weakened by 10⁻⁶ overall, or by 10⁻⁴ on one wall piece or one seam, are refused too.

Reviews. Six AI agents, working separately, were each given one part of the argument and asked to break it: the exact lemma's mathematics; its code, line by line; the polygon bound of zm_mixed.py, used here for the first time in a certificate; the zero-tilt lemma, the area-density lemmas and the leaves; the reduction to one box and the coverage of the pose space; and an empirical attack on the cover itself. Each re-derived its part and wrote its own exact tests. None found an error. They found wording to fix, and one gap in auditability: the earlier record kept only per-root totals. The run of record keeps every leaf, and two guards suggested by the reviews were added to the code. Among their findings: the tightest placement away from the known tight set, near 45°, captures 1 + 1.03·10⁻⁴; an independent zero-tilt check over the whole box, with no symmetry, again gives exactly 1; and a cover weakened by 10⁻⁴ at a corner limit is refused where it should be.

There is no second checker yet. The Rust checker zmx2 of s(21), s(45) and s(60) is being extended to area density (the area-density square cannot be removed from this family). As of 2026-09-30 that extension certifies the zero-tilt face, and every tilt from 0.014° up, over the whole pose space with no symmetry assumed; but at tilts below 0.01°, near a few placements where a square's edges meet three grid lines at once, 120 boxes of the symmetry-reduced region are still uncertified (search/ZMX2_AREA.md). So it does not yet certify Valid7. The cases k = 6, 7, 8 are also settled by other covers: s(32) (kernel-checked in Lean with no hypothesis), s(45) and s(60) (each by two separately written checkers; one of them, zm_mixed.py, also supplies the piece bounds used here).

theorem SquarePacking.Bentz.bentz_of_valid7 (h : Valid7) :
    ∀ k : ℕ, 6 ≤ k → minSide (k ^ 2 - 3) = k

minSide is the Lean definition used for s(13) and s(32). The hypothesis Valid7 says that every closed unit square in [0,7]² captures mass at least 1 under the 7 × 7 box file, taken verbatim (800 segments and the area-density square). That is exactly the claim of §04.

Everything else is checked by Lean's kernel: the measure for every k, generated from a table of the family's masses; that for k = 7 it is the box file, segment by segment; the total k² − 4D < k² − 3; the move of any unit square into the 7 × 7 box; the scaling argument; and the grid. Standard axioms only, no sorry, no native_decide. It is in the default build and takes about two minutes.

Valid7 itself is not proved in Lean. The kernel verifier that proves the covering property for s(13) and s(32) handles weighted points; this cover would need area density, the zero-tilt lemma and the exact lemma of §04.

• The covering property of the 7 × 7 box rests on one program, search/qx2_zm.py, with about 900 lines of new code on top of the reviewed zm_mixed.py. It has been tested hard and reviewed, but not re-implemented independently. Our other exact values each have two separately written checkers that share no code (they do share the formulation of the point test, s(21) §06).
• The reviews were done by AI agents, not by outside mathematicians. Nothing here is peer reviewed.
• The Lean proof is conditional on Valid7 (§05).
• This family covers k ≥ 6 only. The statement for all k ≥ 3 also needs k = 3, 4, 5: k = 4 and k = 5 follow from this project's case-free s(13) = 4 and s(21) = 5 as well as from Bentz's proofs, and k = 3 is Kearney and Shiu's (§02).
• The consequence s(k² − 2) = k drawn in §02 rests, for k ≥ 9, on this certificate alone among our results (chelokot's Lean proof is a separate route).
• The family was found by a float linear program, and a float program can be wrong (§04). The certificate does not rely on it: every acceptance is an exact rational test.

The certificate bundle is s12/certificates/k2m3 of evand/square-packing: its README says what checks what, and verify.sh re-checks it. By default it takes seconds: hashes, the cover's total and symmetry, that the family rebuilds the box file, the Lean data, a re-run of the exact zero-tilt check, and the run record's structure and coverage (every root covered by its recorded leaves). It does not recompute the mass bound at any positive-tilt leaf, so it is not a fresh geometric check; verify.sh --full is, re-running qx2_zm.py (about 81,000 CPU-seconds) and comparing root for root. (The s(60) bundle's default check, by contrast, includes a fresh run of its Rust checker.) The 7 × 7 box file is also here. From s12/search:

python3 qx2_zm.py axis qx2_data/L4_k02_box7.txt           # zero tilt, seconds
python3 qx2_family_check.py qx2_data/L4_k02_family.txt qx2_data/L4_k02_box7.txt
python3 qx2_zm.py qx2_data/L4_k02_box7.txt --depth 18 --nproc 8 \
    --exact-umax 1/2 --exact-from 3                         # positive tilt, ~22 CPU-hours