Forty-five unit squares fit in a 7 × 7 square: take the grid and leave four cells empty. No arrangement fits them into anything smaller: s(45) = 7. The proof is the one used for s(21) = 5, one size up: weighted points plus mass spread evenly along the grid lines, checked by the same two exact checkers. It is not in Lean yet.
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(45) ≤ 7. The work is the other direction.
Theorem. There is a mass distribution on [0,7]², made of 19,989 weighted points and 3,912 short segments of the interior grid lines carrying mass spread evenly along their length, of total mass 2238676387 / (5·10⁷), such that every closed unit square inside [0,7]², at every position and every angle, captures mass at least 1.
44.773528 < 45
Suppose 45 unit squares fit in a square of side s < 7. Spread their centres out by the factor 7/s. The squares stay inside [0,7]² and become pairwise disjoint, so no part of the mass lies in two of them. Each captures mass at least 1, so between them they capture at least 45, but there is only 44.77 in total. So there is no such packing, and s(45) = 7. "Captures" is meant for the closed square: a point on its boundary counts, and a segment lying along one of its edges counts in full.
With s(21) = 5 and s(32) = 6 this is the third exact value of s(k² − 4) for k ≥ 4. The property in the theorem was checked for every placement of a unit square, a three-parameter continuum, by two checkers written independently (§04). Unlike those two, there is no Lean theorem for this one (§05).
Friedman's survey has no lower bound for n = 42 to 46. Before 2026 the best was Nagamochi's general bound. In September 2026 rectangle-density certificates brought it close to 7:
| lower bound for s(45) | source |
|---|---|
| 6.708204 = √45 | area |
| 6.830952 = 1 + √34 | Nagamochi 2005, a general bound |
| 6.945 = 1389/200, then 6.955 = 1391/200 | wand125, rectangle-density certificates, 2026-09-25 to 27 (unrefereed) |
| 7 | this work, 2026-09-27 (unrefereed) |
We first tried weighted points alone, as for s(32). The linear program had room, but every explicit point cover the repair loop produced still let some tilted placement near the edge tiles capture less than 1. Spreading part of the mass evenly along the grid lines, as for s(21), removed those holes at once: the second round of a single linear-program run already had room below 45 (S45_COVER.md §10).
One rung further, the same recipe at side 8 gives s(60) = 8 (2026-09-28): 23,744 weighted points plus mass on the fourteen interior grid lines, total 59.8587 < 60, certified by the same two checkers with the same settings (0 uncertified boxes in either), no Lean. The best lower bound before it was 397/50 = 7.94 (wand125, 2026-09-27). Since removing a square cannot make the packing harder, it also gives s(61) = 8, the first open case of s(k² − 3) = k (proved before only up to k = 7). It has no page of its own: the certificate README is the documentation, and S60_COVER.md the research log.
Why the lines help is explained on the s(21) page: a square tilted slightly over a grid cell keeps part of one grid line and the complementary part of the parallel line one unit away, and if both carry the same even density the two parts add up to a whole edge wherever the tilt pivots.
The weights are the linear program's second round multiplied by 409/400, with masses rounded up. By bisection with the Rust checker, the unscaled cover verifies at a factor of 1.0153 and is refused just below, so this one sits about 0.7% above its threshold and 0.5% below 45. Every number in the file is an integer: coordinates in thousandths, masses in units of 10⁻⁸. The file format is the one of s(21) (FORMAT.md).
The distribution is unchanged by all eight symmetries of the square (checked exactly), so it is enough to check squares whose centre lies in [0,3.5]² and whose angle lies in [0°, 45°]; the checkers take angles up to 53.13°. The Rust checker also checks the whole pose space with no symmetry assumed. Both are the exact files, with the same settings, that certified s(21); the s(21) page describes how they work.
| search/zm_mixed.py | verify2/zmx2 | |
|---|---|---|
| language, arithmetic | Python; exact Fraction and integers, floats only to choose tests | Rust; exact integers for points and masses, outward-rounded intervals for where lines cross edges |
| region | symmetry-reduced | symmetry-reduced, and the whole pose space |
| root boxes | 78,400 | 4,900 and 39,200 |
| certified | 78,400 | 4,900 and 39,200 |
| boxes, max depth | 437,510, 19 | 2.07 M, 24; 16.6 M, 24 |
| uncertified | 0 | 0 |
| CPU | 16.5 h (83 min on 12 processes) | 19 s; 144 s |
Nothing specific to this cover has been audited separately. The checkers are the reviewed s(21) files (same hashes), but no deliberately broken versions of this cover were tried and there is no independent review of this bundle yet.
There is no Lean theorem minSide 45 = 7. The general steps are proved in Lean for any side: that a mass distribution of this kind bounds the packing, and the symmetry reduction (lean/Sqpack/MixedMeasure.lean, used for s(21)). Nothing about this cover is transcribed or checked in Lean. The kernel verifier that checks s(13) and s(32) handles weighted points only; extending it to segments would cover both s(21) and this.
Everything is in s12/certificates/s45 of evand/square-packing. certificates/s45/verify.sh re-checks in about 30 seconds on 6 cores, including a fresh zmx2 run over the whole pose space; --full also re-runs zm_mixed.py, about 16.5 CPU-hours.
| path (under s12/) | what |
|---|---|
| certificates/s45/s45_mixed_cover_7.txt | the cover: integer points, segments and masses |
| certificates/s45/zm_mixed_d4/, zmx2_*/ | the runs: every root's record, hashes and settings, the exact checker files |
| certificates/s45/README.md | the claim, what checks what, and what is trusted |
| certificates/s21/FORMAT.md | the file format, and why a valid file bounds s(n) |
| search/zm_mixed.py, verify2/src/bin/zmx2.rs | the two checkers; proofs in search/ZM_MIXED.md, search/ZMX2.md |
| search/S45_COVER.md | the research log: the point covers that failed (§§0–9) and the line cover (§10) |