The result:
\[ s(17) \;>\; \frac{40\sqrt2+19}{17} + \frac{1}{200} \;=\; 4.450208382054341291\ldots \]
Here \(s(n)\) is the side of the smallest square containing \(n\) unit squares. The previous lower bound, \((40\sqrt2+19)/17 \approx 4.4452\), is due to Trevor Green (2000, recorded in Friedman's dynamic survey with no proof on record — just the value and a sixteen-point figure). The improvement is exactly \(1/200 = 0.005\), and it is the first movement of this bound in 26 years. Since \(s\) is nondecreasing, the same value is a lower bound for \(s(18)\), improving that bound too.
The proof is computer-assisted in an essential way: fourteen hash-pinned exact interval-arithmetic certificates plus a 634,562-row exact finite ledger, all replayable deterministically, with the non-computational algebraic spine formalized in Lean 4.
Let \(s(n)\) be the side of the smallest square containing \(n\) pairwise interior-disjoint unit squares, rotations allowed; trivially \(\sqrt n \le s(n) \le \lceil\sqrt n\rceil\). For \(n=17\) the best packing, found by Bidwell in 1998, has side \(\approx 4.6755\) (recorded as \(s(17) \le 4.6756\) in Friedman's survey); it is the smallest instance whose best known packing uses squares at three distinct angles. Below, the best published bound was Green's \(s(17) \ge (40\sqrt2+19)/17\), unmoved since 2000. This paper opens a gap of \(1/200\) above Green's value.
Green's idea, reconstructed here, is a set \(P\) of sixteen points placed in the container so that almost every contained unit square covers a point of \(P\) in its interior. Seventeen squares competing for sixteen points is a pigeonhole setup: if the scaffold were literally unavoidable, some packed square would have to be empty (contain no scaffold point), and one could hope to rule that out. The scaffold is arranged in four rows of four, governed by two constants \(t, u\) with \(t^2+u^2=1\); its natural triangulation has 18 faces, 17 mesh edges of length exactly one, and exactly six longer defect edges of length \(d = \sqrt{2-2u} \in (1,\sqrt2)\). The scaffold is not unavoidable: each defect edge threads a one-parameter family of empty squares (a defect tube), and there are also degenerate carriers — empty squares tangent along a unit mesh edge or a wall, classified by 23 endpoint-pair labels. The proof does not deny these failures; it charges them.
For a packing of seventeen squares, let \(E\) be the number of empty squares, \(U\) the number of scaffold points in no square's interior, and \(R = \sum_{S} (h(S)-1)\) over nonempty squares the excess incidences, where \(h(S)\) counts scaffold points interior to \(S\). Writing \(H=\sum_S h(S)\): disjoint interiors give \(U = 16 - H\), and the \(17-E\) nonempty squares give \(R = H-(17-E)\). Adding:
\[ U + R = E - 1 . \]
This exact identity is the engine. If in every case one can certify the reverse inequality \(U + R \ge E\) — each empty square forces at least a matching amount of waste elsewhere — the packing is contradictory and cannot exist. Losses are counted through a matching refinement: with \(B\) the set of "lost" points (unused, or owned by a square holding two or more points), \(U+R \ge |B| - \nu(\Gamma[B])\) where \(\Gamma\) is the co-hit graph joining scaffold points at distance \(\le\sqrt2\) (the diameter of a unit square) and \(\nu\) is the matching number. Crucially the bound is monotone in \(B\): certifying only a subset of the true losses is always sound.
At Green's side \(\Lambda=(40\sqrt2+19)/17\) the charging balances exactly. To gain an increment \(\delta\), the paper deforms the scaffold along its defining constraint: with \(w_0 = u_0 - t_0\) Green's endpoint constant, set
\[ w = w_0 + \delta,\qquad p=\sqrt{2-w^2},\qquad u=\frac{p+w}{2},\qquad t=\frac{p-w}{2}, \]
so that \(t^2+u^2=1\) and \(u-t=w\) hold exactly after deformation. Two collapses (\(u_0-4t_0=-3\) and \(\Lambda=2\sqrt2+2+w_0\)) then give the punchline: the deformed scaffold with its fence margins has width exactly \(\Lambda+\delta\) — it keeps filling the container horizontally, and the left, right, and bottom fences keep their endpoint equalities. Because \(t^2+u^2=1\) survives, the triangulation keeps the same 17 unit edges and 6 defect edges, so the whole endpoint classification machinery transfers. All the new slack accumulates at one place, the top fence, in the amount
\[ \eta = \delta + 3(t_0-t), \qquad 2\delta < \eta < 4\delta \]
(in fact \(\eta < \tfrac52\delta\); at the target \(\delta_*=1/200\), \(\eta = 0.0104035\ldots\)). A naive anchoring at the lower-left corner would instead open five new wall families of empty squares; the circle-constrained deformation opens exactly two.
A square hugging the displaced top wall must cut the top scaffold row in a chord of length at least \(1-2\eta \approx 0.9792\). The top-row gaps have lengths \(m_x, 1, 1, u, m_x\), and exact reserves show such a chord fits only in the two unit gaps \(p_{12}p_{13}\) and \(p_{13}p_{14}\). The empty squares living there form the two channels \(T12\) and \(T13\): closed two-parameter families described by an exact chart in the reduced orientation \(r\), wall slack \(\tau\ge0\), and endpoint clearances \(\alpha,\beta\ge0\):
\[ 0 \le \tau + A(r^2) \le \eta, \qquad \alpha+\beta = \frac{\eta-\tau-A(r^2)}{\kappa}, \]
with \(\kappa = (1-r^2)/2\). Each channel admits at most one packed square (any two would share the gap midpoint), and a channel square collides with every closed unit square containing both gap endpoints — the deletions the ledger will use. The classification theorem then says: at \(\delta=\delta_*\), every empty contained square is a defect tube, a carrier, or a channel square. Nothing else exists to charge.
The gatekeeper in the chart is the angular cost
\[ A(x) = \sqrt{2-x} + \frac{x}{2} - \sqrt2, \]
strictly increasing on \([0,1)\) with \(A(0)=0\): \(A(r^2)\) is the extra top clearance consumed by tilting a square to reduced orientation \(r\). Since the chart forces \(A(r^2)\le\eta\), tilting is rationed by the slack. Exact evaluation gives
\[ A\bigl((27/100)^2\bigr) - \eta = 3.31787970482\ldots\times10^{-5} > 0, \]
so every channel square satisfies \(|r| < 27/100\). The margin is real but thin: the exact feasible endpoint is \(|r| \le 0.26956\ldots\), so the rational cutoff \(R_\star = 27/100\), shared by every certificate in the proof, is nearly tight and the positive tail of radii below it must be retained, not rounded away. Both the monotonicity of \(A\) and this margin are Lean-formalized.
Each occupied tube or channel must be paid for through the identity. The six tubes are handled by certified loss clauses (e.g. an \(L0\)-tube square forces \(p_1\) lost; the middle tubes force disjunctions like "\(p_9\) or \(p_{12}\) lost") plus edge deletions in \(\Gamma\) — a threaded square contains its defect edge's midpoint deep in its interior, killing that co-hit edge. The right channel is similarly direct: certificate C1 shows a \(T13\) square forces \(p_{14}\) lost. That statement genuinely fails at \(\delta\approx0.005872\) — by an explicit configuration, not an interval artifact — which is what caps this architecture near the chosen target.
The left channel is the genuinely new difficulty: the unconditional loss "\(T12 \Rightarrow p_{13}\) lost" is false above \(\delta\approx0.0019240\), well below the target. The replacement (C2) is a certified nested three-way alternative: either \(p_{13}\) is lost; or it has a canonical singleton owner boxed into a narrow orientation window (\(57/400 \le r \le 27/100\)) with pinned escape faces; or, nested inside that, \(p_{12}\) also has a singleton owner in an even smaller box. Five further certificates (C3–C7) close the residual branches one by one: an owner-orientation guard and a low-radius \(p_{10}\) loss, a high-radius tail that excludes the tube \(L1\) outright (the proof's largest tree, 4,519,791 nodes), a special midpoint deletion, and a conditional \(p_8\) loss. A short exact bookkeeping step — the double-singleton box has \(r \le 41/200 = 0.205 < 0.21\), so the low-radius branch applies there — assembles everything into four exhaustive alternatives, each contributing forced losses, a deleted edge, and possibly a side condition, in exactly the form the ledger consumes.
The endgame is an exact enumeration. A row is a choice of: one of the 25 independent tube sets (no two adjacent tubes can both be threaded), one of the 10,339 conservative carrier sets, a subset of \(\{T12, T13\}\), and, when \(T12\) is present, one of its four branches — subject to compatibility filters (the channel–tube exclusions, no \(L1\) in the tail branch, no carrier label coinciding with a deleted edge). That gives
\[ 263{,}483 + 3\cdot102{,}601 + 63{,}276 = 634{,}562 \]
rows. For each row the script assembles the certified unused points \(A\) (carrier endpoints plus promotions), ranges over every witness tuple \(W\) — one lost point selected from each applicable loss clause, disjuncts free — and verifies, with matching numbers computed by exact integer combinatorics on the deletion-adjusted co-hit graph,
\[ |A| + |M| - \nu(\Gamma[M]) \;\ge\; \lambda, \qquad M = W\setminus A, \]
where \(\lambda\) is the row's label count. Any actual packing realizes a compatible row with \(\lambda = E\), and the row inequality then yields \(U+R \ge E\), contradicting \(U+R=E-1\). The run reports zero failures with minimum reserve exactly zero. So no packing exists at side \(\Lambda + 1/200\); a compactness (attainment) lemma — the argument's sole use of compactness — converts the exclusion into the strict inequality. The mechanism is repeatable: it was previously run at six smaller increments before \(1/200\).
Every statement delegated to computation is stated as a Certified Theorem citing one of the certificates C1–C14, with census, minimum margin, and SHA-256 hash recorded in the paper's trust appendix. All computation follows a four-rule discipline:
On 2026-08-08 the full aggregate replay
(scripts/s17_green_deformed_bound.py, invoked as
make verify-s17-green-deformed-bound) was run to completion on
the author's machine and passed: 634,562 rows, final_failures=0,
minimum_reserve=0,
minimum_farkas_margin=1.99418732628e-09. All fourteen SHA-256
hashes were independently recomputed and match. Anyone with the repository can
re-run the same replay commands; a referee who does so is independent of every
status claim above. What remains trusted code is the replay checker itself
(its outward rounding and coverage checking), and the correspondence between
the prose case analyses and the certificate trees, which the assembler's
manifest audit checks mechanically.
Lean 4 spine. The non-computational algebraic content is
formalized in PaperProofs/S17Paper.lean (Lean v4.29.1, mathlib
v4.29.1; sorry-free, standard axioms only): the deformation constants and
survival of the circle constraint (\(t^2+u^2=1\), \(u-t=w\)); the exact
horizontal fit \(2m_x+u+2=\Lambda+\delta\) via the collapses
\(u_0-4t_0=-3\) and \(2\sqrt2-1+3t_0=\Lambda\); the top-excess identity
\(\eta=\delta+3(t_0-t)\) and the bounds \(2\delta<\eta<4\delta\); the
strict monotonicity of the angular cost \(A\) and the channel-radius margin
\(A((27/100)^2)>\eta\); and the defect identity \(E=U+R+1\) as an abstract
counting lemma over a seventeen-element set.
Not formalized. The fourteen interval–Farkas certificates and the 634,562-row ledger are not in Lean; they are validated solely by the exact-arithmetic replay pipeline described above.
Independent audit (LEAN-CHECK.md). A statement-by-statement audit of the paper against the source repository confirmed the spine, the certificate hashes, censuses, and margins. It also found a genuine documentation gap: the ledger script applies a row-compatibility filter (discarding rows in which a carrier label coincides with a row-licensed deleted edge) that neither the earlier draft nor the source documents stated — the script did more than the prose admitted. The paper now defines deletions in the closed form the certificates actually prove, states the filter as a third row-compatibility condition, and proves that any packing realizes a compatible row via an injective one-label-per-empty-square assignment. The audit's remaining caveats: the certificate replays were verified against the logged run rather than re-executed within the audit itself, and the sharpened ledger-realizability paragraph is flagged as the passage most deserving of referee attention.
Human review. Incomplete. The finite computations are exactly certified and replayable and the spine is machine-checked, but the paper has not had independent human refereeing.