Twelve and Eleven Squares

The proof is a weighted unavoidable set: points carrying weights, such that every unit square inside the container, at every position and every angle, captures total weight at least 1. Twelve squares with disjoint interiors would capture at least 12, so a set weighing less than 12 rules them out (the idea, with a playground).

A weaker certificate is far prettier. Insist that every point carry the same weight, and the best one found is 81 points in [0, 35/9]² such that every closed unit square inside, at every angle, contains at least 7 of them. Twelve squares would need 12 × 7 = 84, so s(12) ≥ 35/9 = 3.888…, already past the 2003 bound. It is drawn in §03.

Let s(n) be the side of the smallest square holding n unit squares, rotations allowed. It is known exactly for surprisingly few n.

Because s(13) = 4 is proved and s(11) < 4, the largest n with s(n) < 4 is either 11 or 12, and deciding which is the open problem. For n = 12 the gap was [3.788854, 4]; it is now [3.9686, 4]. From the other direction, a basin-hopping search over all 36 coordinates, validated on n = 5, 10 and 11, finds nothing below side 4: every run collapses to the compressed 4 × 4 grid. Schadt's and Ellsworth's 2025–26 annealing campaigns, which improved many records, never improved 12.

Timeline and records

s(12). Our first bound, 3920/997 = 3.9318, went up on 2026-08-24 and 15680/3951 = 3.968616 on 2026-08-26, in the repository evand/square-packing-12 (since merged into this one). As far as we know these were the first lower bounds specific to twelve squares. jlevy/squares reached 99/25 = 3.96 on 2026-09-04 with its own weighted certificates. It has since replayed ours, by a second method as well as with our checker, and lists 3.968616 as the verified bound for n = 12. It is still the best lower bound for s(12) that we know of.

s(11). We found s(11) ≥ 3040/797 = 3.8143 on 2026-08-26 but first published it on 2026-09-22. By then jlevy/squares had published 3.81 (2026-09-04) and 3.8264 (2026-09-09), so ours was never the best public bound: 3.8143, since superseded by jlevy's 3.827 and Kleddamag's 3.875. Kleddamag's s(11) > 31/8 (2026-09-22) builds on jlevy's certificate and on a checker by Guzhou0806, and stands about 0.002 below Trump's 1979 packing. tokoharu's rectangle-density certificate gives 3.81. Ours remains an independent certificate of a weaker bound, and a Lean theorem (§05).

Every lower bound for n = 11 and 12 recorded in the Atlas since 2003, from the same data as the Bounds chart. The 2026 entries are unrefereed; each links to its source.

A linear program chooses the points and their fractional weights, where the classical proofs (Göbel, Stromquist, Friedman, Nagamochi, Bentz) hand-design them. The bound was sharpened in three steps: scaling the first certificate up to its critical container (3.92 → 3.9318), re-optimising the weights with the exact verifier supplying violated placements as cutting planes (3.9486), and growing the point set by column generation (3.9686); at 3.9696 column generation no longer gets under 12. The uniform certificates come from an integer program that forces equal weights: 1/7 each for the 81-point set. The 1736-point certificate does not draw as cleanly.

A bound like this is worth what its verification is worth, so the covering property is checked three independent ways, and for the smaller bounds a fourth, inside Lean (§05).

$ ./verify/target/release/verify certificates/s12_lower_3.9686.txt 12 6000 32 0
D4-symmetric atom set: true  -> angles cover [0,45] deg
atoms=1736 total weight = 119738036/10000000 = 11.973804
s = 15680/3951 = 3.968616
angles: k=0..2486 (N=6000), covering [0,45deg]
min covered weight over ALL placements = 10000056/10000000 = 1.000006  (at angle k=0)
VERIFIED: every CLOSED unit square inside C covers weight >= 1, and total weight < 12.
==> 12 unit squares cannot be packed into any square of side < 15680/3951 = 3.968615540,
    i.e.  s(12) >= 3.968615540

theorem s12_ge_15680_3951 : (15680 / 3951 : ℝ) ≤ minSide 12
theorem s12_ge_35_9       : (35 / 9 : ℝ) ≤ minSide 12
theorem s12_ge_3920_997   : (3920 / 997 : ℝ) ≤ minSide 12
theorem s11_ge_3040_797   : (3040 / 797 : ℝ) ≤ minSide 11

In Lean 4 with Mathlib, minSide n is the usual s(n). The reduction step (an unavoidable set of total weight W allows at most W squares) is formalised, including the scaling argument that lets a closed-square certificate control a packing. For all four bounds above the covering property is checked too, inside Lean's kernel (decide +kernel, no native_decide), by a verifier for trees of pose boxes proved sound once; they are Lean theorems with no hypothesis. The main certificate, 3.968616, is the largest: 328,275 leaves, about 7 CPU-hours in the kernel. No sorry; axioms are only propext, Classical.choice, Quot.sound.

It does not prove s(12) = 4, and this method never will. By LP duality a certificate at container side s weighs at least the fractional packing number ν_f(s), and an exact fractional packing of mass 12.0282 at s = 3.99 shows that no weighted cover below 12 exists at any side ≥ 3.99, whatever points or verifier are used (DUAL_EXACT.md). So the ceiling of this whole family of arguments lies in [3.968616, 3.99). It is not 4.

The container itself does not help: a cover of [0,4]² in the closed convention, where a point on a square's edge counts, weighs at least 12.2688 (COVER4.md). Case analysis layered on top, Bentz's route for thirteen, has been measured there too, and every branching tried leaves a case still worth 12 (BENTZ.md). The missing unit is rotation, mostly by less than one degree, and on the LP's extremal measure it is carried by eight squares at once, a statement no weighting of points can express. That is a real research problem, not a longer run.

The complete negative record, with every route to s(12) = 4 tried, where each one fails, and each claim labelled proved or measured, is notes/n12-gap.md.

• These results rest on computation, not on proofs a human can check by hand, and nothing here has been peer reviewed.
• The record claims in §02 rest on DS7, David Ellsworth's record tables and the 2026 repositories listed on Sources §5.

The case-free proof of s(13) = 4 that used to be here now has its own page: Thirteen Squares.

Everything is in the repository evand/square-packing (directory s12/); ./verify.sh rebuilds the verifiers and re-checks the certificates (--full adds the slow sweeps), and CI runs the fast tier on every change.

The Lean side: cd lean && lake build builds the reductions and s(12) ≥ 35/9, s(12) ≥ 3920/997 (a few minutes on 4 cores, after Mathlib). The s(11) kernel check is opt-in, with its data generated first (deterministic, gitignored):

$ lean/scripts/gen_data.sh S11 && (cd lean && lake build Sqpack.S11Lower)   # s(11) ≥ 3040/797: about 1 CPU-hour
$ lean/scripts/gen_data.sh S12H && lean/scripts/build_parts.sh S12H Sqpack.S12HLower 1   # s(12) ≥ 15680/3951: ~7 CPU-hours, up to 31 GB