The Result and Proof Roadmap

Let $s\mkern1mu(11)$$s\mkern1mu(11)$$s\mkern1mu(11)$$s(11)$ be the smallest side of a square that can hold eleven unit squares, allowing the squares to rotate but not to overlap in their interiors. Write $L$$L$$L$$L$ for the exact value below. We prove

Thus eleven unit squares cannot fit in any square whose side is smaller than $L$$L$$L$$L$. This is T-026’s historical lower bound, explained in this v0.4 proof edition.

The project’s initial improvement appears to have been the first in 23 years on what was then the smallest open case of the square packing problem.¹ Stromquist published the previous bound of 3.7888543… in 2003.²³ The tightest known packing, due to Trump in 1979 (Figure 1), shows $s\mkern1mu(11) \le 3.8770835\ldots$$s\mkern1mu(11) \le 3.8770835\ldots$$s\mkern1mu(11) \le 3.8770835\ldots$$s(11)\le 3.8770835\dots$.⁴

Frontier update, September 30, 2026: The independently checked T-060 proof by Queuingtheorydotcom after Levy et al. 2026 establishes $s\mkern1mu(11)=T$$s\mkern1mu(11)=T$$s\mkern1mu(11)=T$$s(11)=T$, where $T$$T$$T$$T$ is Trump's exact degree-eight packing side specified in the case record. The decimal $3.8770835\ldots$$3.8770835\ldots$$3.8770835\ldots$$3.8770835\dots$ is a truncated display, not the definition of $T$$T$$T$$T$. Part II of this series explains Kleddamag's intermediate $s\mkern1mu(11) \gt 31/8$$s\mkern1mu(11) \gt 31/8$$s\mkern1mu(11) \gt 31/8$$s(11)>31/8$ (T-037), Part III explains that proof, and the mathematical review records its independent checks. This article retains the earlier T-018, T-025, and T-026 lower-bound proofs below.

A core is a smaller square selected strictly inside one of the packed unit squares. We explain the proof in three stages:

1. T-018: weighted points reach $3.81$$3.81$$3.81$$3.81$. This is the visual proof developed in detail below. It places 1,121 rationally weighted points in the container, checks a net of 181 rationally parameterized directions, and derives a counting contradiction from five exact conditions.

2. T-025: threshold atoms reach $3.82$$3.82$$3.82$$3.82$. Each threshold atom specifies a small set of points, a minimum count, and a weight. It contributes its weight when a core contains at least that many of the set’s points. This stronger counting rule directly excludes the container side $191/50=3.82$$191/50=3.82$$191/50=3.82$$191/50=3.82$.

3. T-026: finer directions and scaling reach $L$$L$$L$$L$. The threshold atoms are rechecked with a larger core on a finer direction net, their weights are rescaled, and an exact dilation argument proves $s\mkern1mu(11)\ge L$$s\mkern1mu(11)\ge L$$s\mkern1mu(11)\ge L$$s(11)\ge L$.

All three stages use the same contradiction: each of eleven disjoint cores would receive at least one unit of weight, while all the available weights can contribute less than eleven in total. The fully illustrated T-018 proof teaches that argument; Proof of the New Lower Bound explains what T-025 and T-026 add. The numerical $3.81$$3.81$$3.81$$3.81$ result is not a premise of T-026: the stronger theorem uses its own threshold certificate and dilation record, while reusing the general core-selection and counting ideas. Keeping T-018 in full also serves as an assurance bridge: verification of the point certificate uses exact rational arithmetic, and its one-file standard-library checker, about 330 lines long and short enough to read in one sitting, lets a reader audit that shared geometry and counting mechanism end to end. It decides the certificate file of 1,121 weighted points in about a minute. The checker does not verify the threshold certificates. The separate T-025 and T-026 claim documents each embed the shared standard-library threshold verifier and their exact input bytes.

The T-026 lower bound is registered as V3/C3: the certificate and dilation calculations used in the proof are machine-checked, with exact or interval-certified evidence and passing replay commands, and the certificate’s coverage condition is confirmed by an exact event-cell sweep and a distinct interval branch-and-bound. The two coverage methods share the certificate data and theorem. A source-distinct review of the complete claim is retained. Under the ladder of 2026-09-30, rung 4 on either axis also needs a second adversarial review by a distinct reviewer and a retained human oversight record, and rung 5 formal verification reviewed by human experts; until those records exist the result stands at V3/C3, machine-checked with its review record pending (it held V4/C5 before).

The Agentic Research Framework

This lower bound is one of 112 results the framework has registered so far, 30 of them apparently new. These include improved lower bounds for $n = 12$$n = 12$$n = 12$$n=12$, $17$$17$$17$$17$, and $19$$19$$19$$19$, two of which others have since raised.⁵ The atlas of best known packings for every $n$$n$$n$$n$ from 1 to 100 in Figure 2 comes from the same research agenda and currently includes 0 new lower bounds proved here.

The repository includes:

• A comprehensive survey of previous research
• The atlas of packings
• A hypothesis registry
• An experiment ledger
• Exact verifiers and other tools
• A retention gate that labels results according to epistemic status (levels of verification, confirmation, significance, and novelty)

Work is planned on a regular cadence, typically in blocks of 8 to 12 hours, with strategic human input on priorities and insights. Agents then break the work into defined workflows, including research survey, correctness verification, research loop, and optimization loop.

The framework relies on several agent tools for better engineering and workflows, notably tbd for task tracking, Softschema for structuring results, and Practical Prose to improve writing quality.

Even with the best agents, research requires strategic human input. The framework lets that input focus on strategy, while agents build on accumulated results and tools in a research flywheel. This approach is likely to be useful for other creative mathematical or technical problems.

The Square Packing Problem

The square packing problem asks, for each $n$$n$$n$$n$, for the side $s\mkern1mu(n)$$s\mkern1mu(n)$$s\mkern1mu(n)$$s(n)$ of the smallest square that holds $n$$n$$n$$n$ unit squares, which are free to rotate and must have disjoint interiors.⁶ Stromquist proved $s\mkern1mu(10) = 3 + 1/\sqrt{2}$$s\mkern1mu(10) = 3 + 1/\sqrt{2}$$s\mkern1mu(10) = 3 + 1/\sqrt{2}$$s(10)=3+1/\sqrt{2}$.⁷ The case $n = 11$$n = 11$$n = 11$$n=11$ was the smallest open case when the certificates explained here were developed. The frontier update above records its current status.

For values of $n$$n$$n$$n$ where $s\mkern1mu(n)$$s\mkern1mu(n)$$s\mkern1mu(n)$$s(n)$ is still unknown, results generally take the form of upper or lower bounds. Write $L_0$$L_0$$L_0$$L_0$ for a container side under consideration. An upper bound is constructive: an arrangement of $n$$n$$n$$n$ unit squares in a square of side $L_0$$L_0$$L_0$$L_0$ shows that $s\mkern1mu(n) \le L_0$$s\mkern1mu(n) \le L_0$$s\mkern1mu(n) \le L_0$$s(n)\le L_0$. Trump’s packing for $n = 11$$n = 11$$n = 11$$n=11$ in Figure 1 is one example. Such constructions may be specified with approximate numerical coordinates or derived exactly by solving the geometric relationships between touching squares. Approximate coordinates alone do not constitute a formal proof of the upper bound.

A lower bound proves that $s\mkern1mu(n) \ge L_0$$s\mkern1mu(n) \ge L_0$$s\mkern1mu(n) \ge L_0$$s(n)\ge L_0$ by ruling out every arrangement in a container of side less than $L_0$$L_0$$L_0$$L_0$. This requires an argument covering all possible placements and rotations of the squares. Such arguments range from simple area comparisons to detailed geometric proofs and computer-assisted certificates. The proof presented here is of this kind.

For eleven squares, T-026 proves $s\mkern1mu(11) \ge 3.8264474…$$s\mkern1mu(11) \ge 3.8264474…$$s\mkern1mu(11) \ge 3.8264474…$$s(11)\ge 3.8264474\dots$. We first prove the point-only rung $s\mkern1mu(11) \ge 381/100 = 3.81$$s\mkern1mu(11) \ge 381/100 = 3.81$$s\mkern1mu(11) \ge 381/100 = 3.81$$s(11)\ge 381/100=3.81$ because its geometry can be drawn and checked directly. The advanced section then explains how threshold atoms and dilation reach T-026’s bound.

(Some figures also show the simpler certificate for the weaker bound $s\mkern1mu(11) \ge 19/5$$s\mkern1mu(11) \ge 19/5$$s\mkern1mu(11) \ge 19/5$$s(11)\ge 19/5$, whose smaller numbers make the argument easier to illustrate. There is a small exact refinement in T-022.)

The Five Conditions for a Point Certificate

We prove $s\mkern1mu(11) \ge 381/100 = 3.81$$s\mkern1mu(11) \ge 381/100 = 3.81$$s\mkern1mu(11) \ge 381/100 = 3.81$$s(11)\ge 381/100=3.81$ with a new weighted-point certificate found by our automated search. The five conditions below follow the finite certificate method used by Burns and Massaccesi.⁸⁹¹⁰

The proof uses a finite certificate: for $n$$n$$n$$n$ unit squares in a container of side $L_0$$L_0$$L_0$$L_0$, a finite set of points in the container, each with a nonnegative rational weight (the atoms; every weight in this certificate is positive), a net of directions $\theta_k = 2\arctan t_k$$\theta_k = 2\arctan t_k$$\theta_k = 2\arctan t_k$${\theta }_k=2\arctan t_k$ with rational half-tangents $0 = t_0 \lt t_1 \lt \cdots \lt t_K$$0 = t_0 \lt t_1 \lt \cdots \lt t_K$$0 = t_0 \lt t_1 \lt \cdots \lt t_K$$0=t_0<t_1<\cdots <t_K$, and a shrink $B$$B$$B$$B$, such that:

Conditions 1 to 4 are exact rational comparisons. Condition 5 is one exact sweep per direction. Together the five prove $s\mkern1mu(n) \ge L_0$$s\mkern1mu(n) \ge L_0$$s\mkern1mu(n) \ge L_0$$s(n)\ge L_0$. The certificate is C-n011-fractional-381-100 (a weaker but simpler one is at C-n011-fractional-19-5). Every figure below is computed from the certificate it shows.

Atoms, Mass, and the Budget

An atom is a point in the container with a nonnegative rational weight, and here every weight is positive. The mass $\mu(R)$$\mu(R)$$\mu(R)$$\mu (R)$ of a region is the sum of the weights of the atoms in it, a finite exact sum.

Suppose eleven unit squares fit in the side-3.81 container, and suppose the atoms have been chosen so that both of these hold:

• Every unit square that can be placed in the container holds mass at least $1$$1$$1$$1$ in its interior.
• The total mass of all 1,121 atoms is below $11$$11$$11$$11$.

The second is a single sum:

Two packed squares may share an edge, and an atom on it lies in both. Their interiors are disjoint, so no atom lies in two of them, and together the eleven interiors hold mass at least $11$$11$$11$$11$. The container holds only $10.863675$$10.863675$$10.863675$$10.863675$. So eleven unit squares do not fit.

Both conditions are properties of the atoms, not of any packing. The rest of the proof makes the first one finite to check.

The Atom Set

There are 1,121 atoms in 149 orbits of $\mathbf{D}_4$$\mathbf{D}_4$$\mathbf{D}_4$${𝐃}_4$, the eight rotations and reflections of the container, with 100 distinct weights between $0.000075$$0.000075$$0.000075$$0.000075$ and $0.14672$$0.14672$$0.14672$$0.14672$. An orbit is an atom with its images under all eight, so the set is invariant under the group: Condition 1. That invariance is what lets the proof check angles only up to $\pi/4$$\pi/4$$\pi/4$$\pi /4$, since a square at any other angle reflects onto that arc and covers the same mass.

Every Placement Covers Mass at Least One

The covering requirement on the atoms, that every placement of a unit square holds mass at least $1$$1$$1$$1$ in its interior, has three continuous parameters, two of position and one of angle.

The proof makes it finite twice over. The angle is snapped to a net of 181 rational directions, and the square checked at each is a slightly smaller one, of side $B$$B$$B$$B$. The next section shows why it stands in for a unit square at any angle. Within a direction, the set of atoms under the square changes only when an atom crosses an edge, so the positions collapse to finitely many event cells, on each of which the covered mass is constant. Condition 5 says every event cell the square’s center can reach without leaving the container, at every net direction, carries mass at least $1$$1$$1$$1$.

Figure 5 evaluates it. Every weight is a whole multiple of $1/200000$$1/200000$$1/200000$$1/200000$, so the readout counts units and rounds nothing. The least covered mass over every placement and all 181 directions is attained at direction $0$$0$$0$$0$, by the square $Q$$Q$$Q$$Q$ centered at $(27/50, 27/50)$$(27/50, 27/50)$$(27/50, 27/50)$$(27/50,27/50)$:

a margin of 50 of those units above the threshold.

From a Continuum of Angles to 181

Take a unit square at any angle. A quarter turn leaves a square unchanged, so its angle may be taken below $\pi/2$$\pi/2$$\pi/2$$\pi /2$, and the net covers only the arc $[0, \pi/4]$$[0, \pi/4]$$[0, \pi/4]$$[0,\pi /4]$. A square whose angle lies past $\pi/4$$\pi/4$$\pi/4$$\pi /4$ is therefore first reflected across the container’s diagonal: the image is a unit square in the container whose angle $\varphi$$\varphi$$\varphi$$\phi$ is on the arc, and by Condition 1 it covers the same mass. Let $\theta$$\theta$$\theta$$\theta$ be the net angle nearest $\varphi$$\varphi$$\varphi$$\phi$. A smaller square of side $B$$B$$B$$B$ at angle $\theta$$\theta$$\theta$$\theta$, with the same center, covers no more mass than the unit square if it fits inside it, because the weights are nonnegative. So if every placement of the smaller square at a net angle covers mass at least 1, every unit square at any angle does too.

It fits exactly when

where $d$$d$$d$$d$ is the angle between the two, at most half the gap between two consecutive net angles. Since $\cos d + \sin d \le 1 + \tan d$$\cos d + \sin d \le 1 + \tan d$$\cos d + \sin d \le 1 + \tan d$$\cos d+\sin d\le 1+\tan d$ on $[0,\pi/4)$$[0,\pi/4)$$[0,\pi/4)$$[0,\pi /4)$, it is enough that

That is Condition 4, and it couples the two parameters: a coarser net widens the gaps, forces $B$$B$$B$$B$ smaller, and makes Condition 5 harder to meet.

The contradiction needs a little more than a fit. Two packed squares may share an edge, so the smaller square has to lie in its unit square’s interior, where no other square reaches. It does: its width across the unit square, $B(\cos d + \sin d)$$B(\cos d + \sin d)$$B(\cos d + \sin d)$$B(\cos d+\sin d)$, is $B$$B$$B$$B$ when $d = 0$$d = 0$$d = 0$$d=0$, and $B \lt 1$$B \lt 1$$B \lt 1$$B<1$ because $B(1 + D) \le 1$$B(1 + D) \le 1$$B(1 + D) \le 1$$B(1+D)\le 1$ with $D \gt 0$$D \gt 0$$D \gt 0$$D>0$; when $d \gt 0$$d \gt 0$$d \gt 0$$d>0$ it is $B\cos d\,(1 + \tan d) \lt B(1 + D) \le 1$$B\cos d\,(1 + \tan d) \lt B(1 + D) \le 1$$B\cos d\,(1 + \tan d) \lt B(1 + D) \le 1$$B\cos d(1+\tan d)<B(1+D)\le 1$, since then $\cos d \lt 1$$\cos d \lt 1$$\cos d \lt 1$$\cos d<1$. So the interior of every unit square at any angle holds mass at least $1$$1$$1$$1$, as the budget assumed. Nothing there needed the inequality in Condition 4 to be strict, so the strict form the verifier tests is a sufficient condition rather than a necessary one, and both certificates meet it.

Each angle is carried as a rational half-tangent, $\theta_k = 2\arctan t_k$$\theta_k = 2\arctan t_k$$\theta_k = 2\arctan t_k$${\theta }_k=2\arctan t_k$, so that

are exact rationals and no angle is a floating-point number. The net must reach $\pi/4$$\pi/4$$\pi/4$$\pi /4$, the end of the arc that Condition 1 reflects every angle onto. That is Condition 3, and since $\tan(\pi/8) = \sqrt{2}-1$$\tan(\pi/8) = \sqrt{2}-1$$\tan(\pi/8) = \sqrt{2}-1$$\tan (\pi /8)=\sqrt{2}-1$ is irrational it too is tested in rational form:

What a Coarser Net Costs

We use the net from Massaccesi’s certificate: 181 equally spaced half-tangents, from $0$$0$$0$$0$ to $207107/500000$$207107/500000$$207107/500000$$207107/500000$.⁹ To price a coarser net, hold a certificate’s atoms fixed, coarsen the net, set $B$$B$$B$$B$ to a seven-place value one step below the largest Condition 4 admits, and decide Condition 5 again. Figure 7 does this for each certificate, and its caption says what halving the net costs.

The Contradiction Argument

The argument shows that a container of side exactly 381/100 is too small. By compactness a packing exists at the infimum, so in fact $s\mkern1mu(11) \gt 381/100$$s\mkern1mu(11) \gt 381/100$$s\mkern1mu(11) \gt 381/100$$s(11)>381/100$; the claim is stated as $\ge$$\ge$$\ge$$\ge$ because that is what the theorem behind the verifier proves, with no appeal to compactness.

Proof of the New Lower Bound

We now prove the headline result. The visual T-018 proof selects a shrunken side-$B$$B$$B$$B$ square inside each physical unit square; call this selected square a core. With point atoms, each site contained in a core contributes its weight to that core’s total. T-025 keeps that mechanism and adds threshold atoms. A threshold atom is a finite set $S$$S$$S$$S$ of distinct points, an integer threshold $1\le k\le |S|$$1\le k\le |S|$$1\le k\le |S|$$1\le k\le |S|$, and a nonnegative weight $w$$w$$w$$w$. Its trace on a core $P$$P$$P$$P$ is the subset $P\cap S$$P\cap S$$P\cap S$$P\cap S$. The atom contributes $w$$w$$w$$w$ to the core’s total when that trace has at least $k$$k$$k$$k$ points.

The budget changes with this rule. The selected cores lie strictly inside packed squares, so they are pairwise disjoint. Their traces on $S$$S$$S$$S$ are therefore disjoint as well. If $r$$r$$r$$r$ cores meet one threshold atom’s condition, then $rk \le |S|$$rk \le |S|$$rk \le |S|$$rk\le |S|$. Thus at most $\lfloor |S|/k\rfloor$$\lfloor |S|/k\rfloor$$\lfloor |S|/k\rfloor$$\lfloor |S|/k\rfloor$ cores can receive that atom’s weight, and the atom contributes at most $w\lfloor |S|/k\rfloor$$w\lfloor |S|/k\rfloor$$w\lfloor |S|/k\rfloor$$w\lfloor |S|/k\rfloor$ to the sum over all cores. A point atom is the special case $|S|=k=1$$|S|=k=1$$|S|=k=1$$|S|=k=1$.

The certificates below keep both atom families closed under the eight symmetries of the container, with equal weights on symmetry-related atoms. Reflecting a core therefore preserves its total assigned weight, as required by the earlier core-selection argument.

This gives the general counting theorem used below. If the direction and shrink conditions select a core inside every packed unit square, every admissible core receives total weight at least $1$$1$$1$$1$, and all atoms together can contribute less than $n$$n$$n$$n$ across disjoint cores, then $n$$n$$n$$n$ packed squares would require a total of at least $n$$n$$n$$n$. Therefore no such packing exists.

T-025: a direct certificate at 3.82

The T-025 certificate has 584 point atoms with mass $271052551/31250000$$271052551/31250000$$271052551/31250000$$271052551/31250000$ and 320 threshold atoms with budget $143352577/62500000$$143352577/62500000$$143352577/62500000$$143352577/62500000$. Every threshold atom is two-of-three, so at most one of the disjoint cores can meet its condition. The total budget is

An exact event-cell sweep over 181 net directions finds that every core receives total weight at least $1+203/100000000>1$$1+203/100000000>1$$1+203/100000000>1$$1+203/100000000>1$. A separate interval calculation checks 361 canonical directions, including the net and its reflections. The same shrink-and-snap argument used above selects a legal core inside every physical square, and the threshold budget then gives the same contradiction. Thus T-025 proves $s\mkern1mu(11)\ge 191/50=3.82$$s\mkern1mu(11)\ge 191/50=3.82$$s\mkern1mu(11)\ge 191/50=3.82$$s(11)\ge 191/50=3.82$ directly. The self-contained claim gives the theorem, exact arithmetic, and both verification routes.

T-026: finer directions and the new lower bound

A finer net reduces the largest angular mismatch and permits a larger core. T-026 uses the same atom locations and thresholds on 1441 directions, raises the core side to $B=249507/250000$$B=249507/250000$$B=249507/250000$$B=249507/250000$, and rescales every weight by one common rational factor, $500000000/498684619$$500000000/498684619$$500000000/498684619$$500000000/498684619$. The minimum total assigned to any core is exactly $1$$1$$1$$1$, while the total budget remains $5483661432/498684619 = 10.9962513… < 11$$5483661432/498684619 = 10.9962513… < 11$$5483661432/498684619 = 10.9962513… < 11$$5483661432/498684619=10.9962513\dots <11$. A second method checks all 2881 directions, again including the reflected net. These facts are recorded in the finer-net certificate.

Now scale the container, the core, and every atom point together by a positive rational factor $q$$q$$q$$q$, while the physical squares remain unit squares. Containment traces do not change, so neither the assigned totals nor the budget changes. For this net, let $D=207107/720000000$$D=207107/720000000$$D=207107/720000000$$D=207107/720000000$ be the tangent of its widest angular half-gap. If $d$$d$$d$$d$ is the mismatch between a physical square and its selected net direction, then $\tan d\le D$$\tan d\le D$$\tan d\le D$$\tan d\le D$. The exact identity $\cos d+\sin d=(1+\tan d)/\sqrt{1+\tan^2d}$$\cos d+\sin d=(1+\tan d)/\sqrt{1+\tan^2d}$$\cos d+\sin d=(1+\tan d)/\sqrt{1+\tan^2d}$$\cos d+\sin d=(1+\tan d)/\sqrt{1+{\tan }^{2}d}$ gives

for every positive rational $q$$q$$q$$q$ with $0<q<c$$0<q<c$$0<q<c$$0<q<c$, where

The corresponding container side is $q\mkern1mu(191/50)$$q\mkern1mu(191/50)$$q\mkern1mu(191/50)$$q(191/50)$, and $L=(191/50)c$$L=(191/50)c$$L=(191/50)c$$L=(191/50)c$.

For every positive real side $x<(191/50)c$$x<(191/50)c$$x<(191/50)c$$x<(191/50)c$, choose a rational $q<c$$q<c$$q<c$$q<c$ with $x<q\mkern1mu(191/50)$$x<q\mkern1mu(191/50)$$x<q\mkern1mu(191/50)$$x<q(191/50)$. The scaled certificate rules out the larger side $q\mkern1mu(191/50)$$q\mkern1mu(191/50)$$q\mkern1mu(191/50)$$q(191/50)$; a packing that fit at $x$$x$$x$$x$ would fit unchanged in that larger container. Therefore

The containment inequality is strict for every positive rational $0<q<c$$0<q<c$$0<q<c$$0<q<c$. The resulting exact exclusions include rational sides above $3.82$$3.82$$3.82$$3.82$ and approach $L$$L$$L$$L$ arbitrarily closely. The rational-density argument above turns that whole family into the exact lower bound $s\mkern1mu(11)\ge L$$s\mkern1mu(11)\ge L$$s\mkern1mu(11)\ge L$$s(11)\ge L$. The T-026 self-contained claim and its machine-readable limit record carry the exact derivation.

Generator and Verifier

The generator and verifier in this section are the point-certificate tools behind Figures 4–7. The generator solves for the weights on a chosen set of sites $A$$A$$A$$A$, arranged in orbits of $\mathbf{D}_4$$\mathbf{D}_4$$\mathbf{D}_4$${𝐃}_4$. The weights, one per orbit, come from the covering linear program

with one constraint per placement of a side-$B$$B$$B$$B$ square at a direction of the net $\Theta$$\Theta$$\Theta$$\Theta$. Placements form a continuum, so constraints are generated as needed: the event-cell sweep that decides Condition 5 finds a placement whose mass falls short, and it becomes a new constraint. The sweep is the separation oracle.

Condition 1 holds by construction, Condition 5 is feasibility in this program, and Condition 2 is a bound on its objective, so on a net and shrink that satisfy Conditions 3 and 4, a certificate on these sites exists when $\tau^* \lt n$$\tau^* \lt n$$\tau^* \lt n$${\tau }^{*}<n$. The target $n$$n$$n$$n$ never enters the program; it is compared with the optimum afterwards. What the certificate carries is not that optimum but a rational point beside it: the solver’s weights, inflated slightly and rounded up to multiples of $1/200000$$1/200000$$1/200000$$1/200000$ so that every constraint holds in exact arithmetic. The verifier proves that point feasible, not minimal.

The search runs in floating point. None of it is part of the proof: the generator writes the certificate to a file, and the verifier decides Conditions 1 through 5 on it in exact rational arithmetic. The verifier rejects a point certificate that fails the conditions, regardless of how it was generated. The gate that admits a point certificate to the record asks for two verdicts: it accepts one only when the exact event-cell sweep and an interval branch-and-bound, which decide Condition 5 by distinct methods, both accept it and report the same least covered mass.

Geometric constraints can strengthen the final count. Stromquist’s six-square proof rules out a container of side less than 3 by forcing four of eight marked points into one square; each other square must contain at least one, so at most five fit. The repaired eleven-square argument similarly forces three of twelve points into one square.⁷³ These examples suggest extending the weighted method by using constraints between squares to force additional mass consumption.

A first-party package for third-party checking gathers what an outside check needs: the theorem written out, the 19/5 certificate as plain data, and a one-file verifier on Python’s standard library that decides it without importing anything else from the repository.

(It checks the simpler point example at $19/5$$19/5$$19/5$$19/5$.)

This project wrote every file in the package, so it is not itself a third-party check.

Verifiable Claim

Each point-certificate bound shown in the interactive figures has one self-contained file: the claim, the theorem with its proof, a verifier in Python’s standard library, and the certificate it decides, to paste into any coding agent or check by hand.

For $s\mkern1mu(11) \ge 381/100$$s\mkern1mu(11) \ge 381/100$$s\mkern1mu(11) \ge 381/100$$s(11)\ge 381/100$: t-018-verifiable-claim-381-100.md, 1,121 atoms. (For the weaker bound $s\mkern1mu(11) \ge 19/5$$s\mkern1mu(11) \ge 19/5$$s\mkern1mu(11) \ge 19/5$$s(11)\ge 19/5$: t-018-verifiable-claim-19-5.md, 425 atoms.)

The one-file checker minimal_verify.py verifies the 381/100 certificate in about a minute.¹¹

The T-025 claim document embeds its certificate and a standard-library exact verifier. The T-026 claim document embeds the finer-net certificate, the same verifier, and the exact dilation record.

Acknowledgments

We thank Walter Stromquist for drawing attention to his twenty-six-square construction in Memo III (private communication, September 2026). His suggestion prompted a source review and independent exact verification.

Further Reading

• The $n = 11$$n = 11$$n = 11$$n=11$ series, in reading order: Part I, this paper; Part II, a review of Kleddamag’s proof of $s\mkern1mu(11) \gt 31/8$$s\mkern1mu(11) \gt 31/8$$s\mkern1mu(11) \gt 31/8$$s(11)>31/8$ (T-037); and Part III, a review of the proof that Trump’s packing is optimal (T-060).
• Papers and sources
  • Friedman’s survey: an introduction to the problem and its literature.⁶
  • Stromquist’s geometric proofs for ten and eleven squares.²⁷
  • Nagamochi’s lower bounds for square packings in rectangles.¹⁰
  • Burns’s weighted certificates and Massaccesi’s linear program for finding their weights.⁸⁹
  • Full paper and source archive: original papers, searchable transcriptions, and captured web sources
• Elements of the project
  • Project overview: results, repository structure, and the research process
  • Problem tutorial: written as part of this project, a first-principles introduction to square packing, bounds, search, and proof obligations
  • Atlas of packings: created as part of this project, a collection of the best known packings for $n=1$$n=1$$n=1$$n=1$ through $324$$324$$324$$324$, with figures, geometry records, and provenance
• Agentic research framework
  • Workflows define entry conditions and expected outputs for each kind of research work.
  • Operating principles cover correctness, process, insight, and efficiency.
  • Epistemics classifies results by verification, confirmation, significance, and novelty.
• Agentic tooling
  • tbd: tasks, dependencies, and handoffs tracked in Git, plus engineering best practices and guidelines for agents
  • Softschema: research records in YAML and Markdown, with validation rules that can become stricter as the work matures
• Document tooling
  • Practical Prose: writing guidelines, editing workflows, and document evaluation
  • Flowmark: automated Markdown management and consistent formatting
  • KPress: web and print formatting from Markdown

Version History

• v0.4.4 — October 5, 2026. The series revision: the paper is Part I of three; its frontier update and Further Reading link Part II, on Kleddamag's T-037, and Part III, on T-060.
• v0.4.3 — October 1, 2026. The settled-case revision: the frontier update records T-060's proof that $s\mkern1mu(11)$$s\mkern1mu(11)$$s\mkern1mu(11)$$s(11)$ is Trump's side, Figure 3 marks the endpoint, T-026 is rated V3/C3, and the raised $n = 12$$n = 12$$n = 12$$n=12$ and $17$$17$$17$$17$ bounds are noted.
• v0.4.2 — September 28, 2026. The recent-results edition: a frontier update records Kleddamag's verified $s\mkern1mu(11) ≥ 3.875$$s\mkern1mu(11) ≥ 3.875$$s\mkern1mu(11) ≥ 3.875$$s(11)\ge 3.875$, built on the T-026 certificate, so the paper presents T-026's bound as historical, and the star on the atlas in Figure 2 marks every recent result.
• v0.4.0 — September 13, 2026. The T-025/T-026 proof edition: T-025 proves $s\mkern1mu(11) ≥ 191/50 = 3.82$$s\mkern1mu(11) ≥ 191/50 = 3.82$$s\mkern1mu(11) ≥ 191/50 = 3.82$$s(11)\ge 191/50=3.82$, and T-026 proves $s\mkern1mu(11) ≥ 3.8264474…$$s\mkern1mu(11) ≥ 3.8264474…$$s\mkern1mu(11) ≥ 3.8264474…$$s(11)\ge 3.8264474\dots$.
• v0.3.0 — September 5, 2026. The first edition: T-018's point certificate proves $s\mkern1mu(11) ≥ 381/100 = 3.81$$s\mkern1mu(11) ≥ 381/100 = 3.81$$s\mkern1mu(11) ≥ 381/100 = 3.81$$s(11)\ge 381/100=3.81$.

1. Our search through September 4, 2026 found no earlier improvement on Stromquist’s bound, stated in 1984 and published in 2003. We checked the project’s sources, scholarly indexes, author pages, and public packing catalogues, but may have missed work in subscription-only indexes, theses, proceedings, or unindexed sources.  ↑ 

2. Walter Stromquist states this bound in Memo III (1984), p. 10, as an adaptation of his preceding proof for $0^\circ$$0^\circ$$0^{\circ }$ and $45^\circ$$45^\circ$${45}^{\circ }$ orientations. This suggests he already had the general argument, whose details he omits. The journal proof appeared in Packing 10 or 11 unit squares in a square, Electronic Journal of Combinatorics 10 (2003), R8.  ↑   ↑ 

3. The bound is correct, but the project found that Stromquist’s printed argument does not close at his Figure 14 and repaired it with a source-distinct point set, certified exactly (T-010 in the project’s result register). The proof here does not depend on it.  ↑   ↑ 

4. Walter Trump’s packing of 1979, as recorded in Kingbird’s register of squares in squares, which also lists the degree-eight polynomial defining its side length. The rendering is the project’s own. Stromquist’s Memo III, pp. 2–4, credits Mats Gustafsson and Magnus Thulin with the same construction, reported by Gardner in November 1980; the research archive records their independent rediscovery.  ↑ 

5. The result register records $s\mkern1mu(12) \ge 3.96$$s\mkern1mu(12) \ge 3.96$$s(12)\ge 3.96$ (T-017), $s\mkern1mu(17) \ge 4.59$$s\mkern1mu(17) \ge 4.59$$s(17)\ge 4.59$ (T-019), and $s\mkern1mu(19) \ge 4.80$$s\mkern1mu(19) \ge 4.80$$s(19)\ge 4.80$ (T-020), each supported by a retained weighted-point certificate and classified as apparently novel. Evan Daniel’s independent $s\mkern1mu(12) \ge 15680/3951$$s\mkern1mu(12) \ge 15680/3951$$s(12)\ge 15680/3951$ and the line of $n = 17$$n = 17$$n=17$ certificates that Kleddamag and Guzhou0806 built on this project’s have since superseded the first two.  ↑ 

6. Erich Friedman, Packing unit squares in squares: a survey and new results, Electronic Journal of Combinatorics, Dynamic Survey DS7.  ↑   ↑ 

7. Walter Stromquist, Packing Unit Squares Inside Squares, Memo I, September 11, 1984, pp. 13–19, gives the six-square helper argument. Memo II, October 15, 1984, proves the ten-square result, later published in his 2003 paper.  ↑   ↑   ↑ 

8. Sam Burns, Proposing a Better Lower Bound for n=17 Square Packing, August 2026, presents a weighted-point certificate for seventeen squares with a rational direction net and exact coverage checks. Burns credits ChatGPT with developing the certificate.  ↑   ↑ 

9. Gustavo Massaccesi, Another Better Lower Bound for n=17 Square Packing, August 2026, improves Burns’s certificate. His Linear Programing for Square Packing describes the linear program and search used to find its weights.  ↑   ↑   ↑ 

10. Earlier counting methods include Göbel’s unavoidable points and Nagamochi’s weighted resources: F. Göbel, Geometrical packing and covering problems, in Packing and Covering in Combinatorics, Mathematical Centre Tracts 106 (1979), 179–199; Hiroshi Nagamochi, Packing unit squares in a rectangle, Electronic Journal of Combinatorics 12 (2005), R37.  ↑   ↑ 

11. The one-minute timing is for minimal_verify.py; recorded runs took 47.5–67.0 seconds under CPython 3.14 on September 5, 2026. The claim document embeds a separate verifier, verify_claim.py, which checks the same certificate in about 3 minutes on an Apple Silicon laptop.  ↑ 

The Squares Project · github.com/jlevy/squaresFormatted and typeset with Flowmark and KPress