Sixty unit squares fit in an 8 × 8 square: take the grid and leave four cells empty. No arrangement fits them into anything smaller: s(60) = 8, and so s(61) = 8 as well. The proof is the one used for s(21) = 5 and s(45) = 7, one size up again, 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(60) ≤ 8. The work is the other direction.
Theorem. There is a mass distribution on [0,8]², made of 23,744 weighted points and 5,216 short segments of the interior grid lines carrying mass spread evenly along their length, of total mass 748233441 / 12500000, such that every closed unit square inside [0,8]², at every position and every angle, captures mass at least 1.
59.858675 < 60
Suppose 60 unit squares fit in a square of side s < 8. Spread their centres out by the factor 8/s. The squares stay inside [0,8]² 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 60, but there is only 59.86 in total. So there is no such packing, and s(60) = 8. "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.
Corollary: s(61) = 8. Removing a square from a packing leaves a packing, so s(61) ≥ s(60) = 8, and the 8 × 8 grid holds 61. Before this, s(k² − 3) = k was proved only up to k = 7; it has since been proved for every k ≥ 6 by a different cover, checked by a different program, qx2_zm.py, which reuses the piece bounds of zm_mixed.py (Three Short of a Square). A third route uses points only: wand125's point cover of [0,8]² (2026-09-30), which we replayed with our two point checkers, zeromargin.py and zmcheck (search/S61_WAND125_REPLAY.md).
With s(21) = 5, s(32) = 6 and s(45) = 7 this is the fourth exact value of s(k² − 4) for k ≥ 4.
| lower bound for s(60) | source |
|---|---|
| 7.745967 = √60 | area |
| 7.855655 = 1 + √47 | Nagamochi 2005, a general bound (its published proof has a gap: Karakuş 2026) |
| 7.94 = 397/50 | wand125, rectangle-density certificates, raised in steps from 2026-09-26 to 27 (unrefereed) |
| 8 | this work, 2026-09-28 (unrefereed) |
The cover is the s(45) recipe at side 8: the linear program was seeded with the s(45) cover, its centre cell duplicated, plus a coarse uniform family of rows, and the line densities again did the work. The research log is S60_COVER.md.
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 fourth round multiplied by 41/40, with masses rounded up. By bisection with the Rust checker, the unscaled cover verifies at a factor of 1.0171875 and is refused at 1.016875, so this one sits about 0.77% above its threshold and 0.24% below 60. 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,4]² 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) and s(45); 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 | 102,400 | 6,400 and 51,200 |
| certified | 102,400 | 6,400 and 51,200 |
| boxes, max depth | 500,134, 18 | 2.62 M, 24; 21.0 M, 24 |
| uncertified | 0 | 0 |
| CPU | 19.6 h (107 min on 12 processes) | 22 s; 177 s |
Nothing specific to this cover has been audited separately. The checkers are the reviewed s(21) files (same hashes, and the zm_mixed.py run repeated after one guard was added in review, with an identical census root for root), 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 60 = 8. As for s(45), the general steps are proved in Lean for any side (lean/Sqpack/MixedMeasure.lean), but nothing about this cover is transcribed or checked there. For s(61) = 8 the situation differs: the k² − 3 family has a kernel-checked reduction to one finite statement about a 7 × 7 box.
Everything is in s12/certificates/s60 of evand/square-packing. certificates/s60/verify.sh re-checks in about 35 seconds on 7 cores, including a fresh zmx2 run over the whole pose space; --full also re-runs zm_mixed.py, about 19.6 CPU-hours.
| path (under s12/) | what |
|---|---|
| certificates/s60/s60_mixed_cover_8.txt | the cover: integer points, segments and masses |
| certificates/s60/zm_mixed_d4/, zmx2_*/ | the runs: every root's record, hashes and settings, the exact checker files |
| certificates/s60/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/S60_COVER.md | the research log: how the cover was built |