n = 45 · Case Records · The Squares Project

n = 45 proved ★O=

$s (45) = 7$

The best packing known for 45 squares, side

7

678

6.7087.708

\sqrt{n}

\sqrt{n} + 1

Proven

$s (45) = 7$

new result
optimal
exact

Citation record n-045

lowerDaniel after Burns, Massaccesi 2026, GitHub (confirmed T-053)

Bounds

Best known packing

$7$

Construction: grid
Tilt angles: $0^{\circ}$
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$7$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

$7$

Proved by: Evan Daniel 2026
Kind: counting
Scope: Unrestricted independent rotations with disjoint interiors; boundary contact allowed.
Note: evand/square-packing (28 September 2026) states $s (45) = 7$ from a mixed cover of [0,7]^2, 19,989 weighted points plus mass spread uniformly along 3,912 interior grid-line segments of length 1/50, total 2238676387/(5*10^7) = 44.77352774 < 45, exactly D4-invariant and certified at margin zero by two separately written checkers, zm_mixed.py (exact rational) and zmx2 (binary64 enclosures widened outward); nothing about this cover is in Lean. Its CREDITS.md says the work was produced with an AI agent under human direction. It supersedes wand125's reported rectangle-density 1391/200 of 27 September 2026, which stays as evidence, and Nagamochi's general 1 + sqrt(34).
Source: [evand square-packing 2026-09-28]
Evidence: E-n045-evand-mixed-cover-report

Verified lower bound

$7$

The reported value, verified here.

Evidence: E-n045-evand-mixed-cover-zmx2-replay

Gap

Solved: the verified bounds meet.

Results in the register

T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
T-053 V3 C3 Daniel after Burns, Massaccesi · 2026-09-29 · n = 45
$s (45) = 7$ , by a mixed cover of points and grid-line segments
Claim and records
Claim
$s (45) = 7$ : the lower half by Evan Daniel's mixed cover of 27 September 2026, the upper half by the $7 \times 7$ grid.

The cover is 19,989 weighted points of [0,7]^2 plus mass spread uniformly along 3,912 segments of length 1/50 on the interior grid lines, total 2238676387/(5*10^7) = 44.77352774 < 45, exactly D4-invariant. Every closed unit square in [0,7]^2 captures mass at least one, with boundary points and edge segments counting in full.

The source certifies it at margin zero with the same two checkers as T-052, zm_mixed.py over 78,400 roots of the D4 region and zmx2 over 4,900 D4 roots and 39,200 unreduced roots. Nothing about this cover is in Lean beyond lemmas proved for every side.

zmx2 was replayed here in full on 28 and 29 September 2026, over all 4,900 D4 roots and all 39,200 unreduced roots, every root's census equal to the source's; zm_mixed.py was only sampled.

Evan Daniel, evand/square-packing, building on Burns's and Massaccesi's method, with an AI agent under human direction as its CREDITS.md says.
Composition
Compound: the lower half is E-n045-evand-mixed-cover-zmx2-replay (interval-certified), the upper half the grid (E-basic-grid-upper, exact-algebraic). As for T-052, the two machine methods certify different halves; the lower half stands on one replayed method and sets the minimum, and the equality is C3. wand125's point-only lower half (T-054) is a second certificate under the same checker and is registered separately.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A complete zm_mixed.py re-sweep, about 16.5 CPU-hours at the source, recorded as a second, exact-algebraic entry, would give the lower half a second machine method; the source's own zm_mixed.py record was imported from a working-name run (review finding F1), so a fresh complete run also retires that finding. V5 would need a top theorem and the checker programs formalised, and a human expert's review of the formalization.
Significance
An exact value for a case that was open, 0.169 above Nagamochi's closed form, and the third of the family s(k^2 - 4) = k for k = 5, 6, 7 with T-051 and T-052. The technique is T-052's, which alone would argue for S3 by the calibration T-020 wrote, but that calibration exempts a case that changes character, and this one goes from open to solved; with its two siblings it is a bound family, so S4.
Novelty
previously-published Present in an identified source
Records
n = 45 register evidence 1 evidence 2 evidence 3 source review
n = 45 register evidence 1 evidence 2 evidence 3 source review
T-054 V3 C3 wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · 2026-09-29 · n = 45
$s (45) = 7$ by a second, point-only route
Claim and records
Claim
$s (45) = 7$ by a second, point-only route: the lower half by wand125's point-only measure of 28 September 2026, the upper half by the $7 \times 7$ grid.

The measure is 12,645 D4-invariant points, total 12666371418707823/2^48 = 44.99999100001 < 45. Its capture condition, every closed unit square in [0,7]^2 having mass at least one with a boundary point counting, is decided by Evan Daniel's unmodified zmx2 with --d4 --pair-points.

The source's verify.sh was replayed here in full on 28 and 29 September 2026: VERIFIED-D4 on all 4,900 roots, 1,295,460 boxes, the source's reference census.

wand125 after Evan Daniel, square-packing-bounds. The source uses Daniel's checker, states that Daniel published $s (45) = 7$ first (T-053) and claims no priority, and says parts of the work were produced with AI assistance under human direction.
Composition
Compound: the lower half is E-n045-wand125-point-cover-source-replay (interval-certified, on the source-chosen zmx2, the same implementation as T-053's replay), the upper half the grid (E-basic-grid-upper). The two machine methods certify different halves; the lower half sets the minimum at one method, and the equality is C3. The unreduced --full sweep was not run here.
Next rung
The unreduced zmx2 --full sweep would remove the reliance on the D4 reduction (review F2). A second machine method would need a checker other than zmx2 to decide this point cover; the exact zeromargin.py route reads point covers and is the reachable one. V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained.
Significance
A second certificate for a value T-053 already holds, decided by the same checker. It shows the value yields to points alone, with a uniform pointwise margin of 8.35e-4, a citable detail that changes no theorem.
Novelty
previously-published Present in an identified source
Records
n = 45 register evidence 1 evidence 2 evidence 3 source review
n = 45 register evidence 1 evidence 2 evidence 3 source review
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
T-081 V0 C1 Daniel after Burns, Massaccesi · 2026-10-03 · 14 cases
$s (k^{2} - 4) = k$ for every integer $k$ from 5 up; $k = 5 \dots 18$ are the cases held here
T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
T-085 V3 C3 Karakuş; chelokot · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$

Verification

upper: replayed here; lower: replayed here

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 38 of the retained witness (witness id 39) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 5 of its 45 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.

Evidence and sources

8 evidence entries

E-wand125-rectangle-report, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper, E-n045-evand-mixed-cover-report, E-n045-evand-mixed-cover-zmx2-replay, E-n045-wand125-point-cover-report, E-n045-wand125-point-cover-source-replay

[evand square-packing 2026-09-28] lower bound proof
[wand125 point and mixed bounds 2026-09-28] lower bound proof
[wand125 rectangle bounds 2026] lower bound proof
[Kingbird] record catalogue
[Nagamochi 2005] lower bound proof
[Friedman DS7] survey

In the frontier survey On GitHub

$s (45)$ — solved

$s (45) = 7$ . Established by a mixed cover with two exhaustive checks of its covering condition, Evan Daniel (2026), building on Sam Burns’s and Gustavo 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. With $s (21) = 5$ , registered with it, and $s (32) = 6$ , it is the third exact value this record holds for a case of the form $k^{2} - 4$ with $k \geq 4$ , as the source says.

The packing

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

The lower bound

The certificate is a mixed cover in the format of $s (21)$ ’s: 19,989 rationally weighted points of $[0, 7]^{2}$ plus mass spread uniformly along 3,912 segments of length $1 / 50$ on the interior grid lines $x, y \in {1, \dots, 6}$ , total $2238676387 / (5 \cdot 10^{7}) = 44.77352774 < 45$ , exactly invariant under the square’s eight symmetries, such that every closed unit square inside $[0, 7]^{2}$ , at every centre and every angle, captures mass at least $1$ , a point on its boundary counting and a segment along one of its edges counting in full. If 45 unit squares fit in a side $s < 7$ , scaling by $7 / s$ gives 45 pairwise disjoint closed unit squares in $[0, 7]^{2}$ , which would capture at least 45 from a total of $44.77$ . As for $s (21)$ , the margin is exactly zero at the grid, and the line mass, $32.8$ of the total, is what makes that possible.

The source certifies it with the same two checkers, byte for byte. zm_mixed.py, in exact rational arithmetic, certifies all 78,400 root boxes of the cover’s D4 fundamental region (437,510 boxes, 16.5 CPU-hours) with no uncertified leaf; that record was produced under the cover’s working file name and imported into the bundle with only its input path changed, which the source discloses. The Rust zmx2, with its binary64 enclosures widened outward, certifies all 4,900 roots of the same region and, assuming no symmetry, all 39,200 roots of the whole pose space. Nothing about this cover is in Lean: the reduction is the $m = 7$ case of lemmas the source proves in Lean for every side, but there is no data file and no top theorem, and the cover was not separately audited at the source.

The verified field rests on a complete replay here of zmx2 (E-n045-evand-mixed-cover-zmx2-replay, V3/C3). Built from the retained source with rustc 1.94.1, it certified all 4,900 D4 roots (2,071,984 boxes) and all 39,200 unreduced roots (16,648,752 boxes) on 28 and 29 September with no uncertified box, every root carrying the census of the source’s record of the same root, and the bundle’s own fast tier passed too; the receipts are in the packet. That replay is interval-certified, so it assumes correctly rounded binary64 arithmetic on the host. The exact checker was sampled here, 32 roots matching the source’s records box for box, and its complete re-sweep runs separately; recorded as a second, exact-algebraic replay, it would give this value a second machine method beside its C3. The review of 28 September found the value sound as stated, with one fewer kernel-checked link than $s (21)$ : the cover’s total and invariance rest on three independent parsers, not on Lean.

wand125 published a second, point-only route to the same value on 28 September: 12,645 D4-invariant weighted points, total $12666371418707823 / 2^{48} = 44.99999100001 \dots$ , whose capture condition is decided by Daniel’s unmodified zmx2 with its --pair-points option. It claims no priority. Its source check was replayed here in full (E-n045-wand125-point-cover-source-replay): all 4,900 D4 roots certified with the source’s reference census, 1,295,460 boxes to depth 38, and the point-only review found it sound. It is the same checker as the replay above, so it adds a second certificate for the value, not a second method. wand125’s README says parts of the work were produced with AI assistance under human direction.

Earlier lower bounds

wand125’s rectangle-density certificate in Tokoharu’s format, retained, reported $1391 / 200 = 6.955$ on 2026-09-27, with total mass $4499 / 100 = 44.99 < 45$ ; it was the case’s reported bound until this registration and stays as evidence. Its complete coverage replay never ran here. The source gives wand125’s earlier $1389 / 200$ as the previous bound. Corrected 2 October 2026: Nagamochi’s Lemma 1 is false (Karakuş 2026), so his closed form below is now a reported bound whose published proof is incomplete (review). This register had recorded that proof as verified, its own error, logged as defect D-516. Before 2026 it was Nagamochi’s general closed form, which applies to every $N \geq 4$ and gives $1 + \sqrt{34} \approx 6.830952$ here:

s (N) \geq min {⌈ \sqrt{N} ⌉, \sqrt{N - 2 ⌊ \sqrt{N} ⌋ + 1} + 1}

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.

bound	evidence	run	code	programs
verified lower	`E-n045-evand-mixed-cover-zmx2-replay`	replayed here	producer’s code	`V-evand-zmx2` (external); `V-audit-evand-mixed-covers` (first-party, premises)
verified upper	`E-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)