Thirteen Squares

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. Sixteen unit squares tile a 4 × 4 square, so s(13) ≤ 4. The work is the other direction.

The theorem is Bentz's; only the proof is new. Everything rests on checking the property in the box above for every placement of a unit square, a three-parameter continuum. Two checkers written independently did that exactly (§04), and so did the kernel of the Lean 4 proof assistant, which proves s(13) = 4 with no hypothesis left over (§05).

The classical proof picks points so that every unit square in the box must cover one. Thirteen squares would then need thirteen points of their own, so a set of twelve would finish the job. The best such set for [0,4]² has 14 points (Friedman's survey, Theorem 4). Bentz closed the gap of two with a case analysis on where the squares can sit, whose six leaves the walkthrough on the Proofs page lets you click through.

Weights change the counting. Give each point a fractional weight, ask every unit square to catch weight at least 1, and a linear program can choose the weights. That idea comes from Sam Burns's and Gustavo Massaccesi's 2026 work on n = 17 (Sources §5). Our s(12) bound uses it in a box slightly smaller than 4. Here it is used in the box of side 4 itself, and that needs two more things, below.

Why the squares are closed

A point exactly on a square's edge counts as captured. That is the limit of the squares of side 1 + ε that every published proof argues about, and it is what makes 13 reachable. With open squares, the sixteen tiles of the 4 × 4 grid, shrunk a hair, are disjoint, so every cover would weigh at least 16. Closed, neighbouring tiles share their edges and the points on them. No closed cover of [0,4]² can weigh less than 12.2688 (proved exactly, COVER4.md), so this one is within 5.6% of the best possible. The same floor is why no cover of this box can say anything about twelve squares: 12.2688 is more than 12.

The cover came out of a linear program over sampled placements with column generation, plus explicit families of placements that the sampling steps over; leaving those out made every earlier candidate invalid (RUNG2.md §10). Every number in the file is an integer: coordinates in thousandths, weights in units of 10⁻⁹.

The angle-net verifier used for s(12) shrinks each square slightly, so that one square stands in for a small range of angles. In the box of side 4 that cannot work. At the corner placement the only captured point lies on the square's edge, so the slack is zero; a tilt of ε buys back only about ε², while a range of angles of width ε costs about ε.

Instead the three-dimensional space of placements is cut adaptively into boxes with rational corners. For each box the checker must prove, exactly, that every placement in it captures weight at least 1, and it splits the box when it cannot. Exhaustive means it finished with no box left uncertified; nothing is sampled, and no floating-point number is load-bearing. A box certified by one fixed set of captured points can only ever prove covers of weight 16 or more (RUNG2.md), so most boxes are certified disjunctively: either this set of points is inside, or that one is.

The two were written from the statement, not from each other: different subdivisions, different primitives, no shared code. They also agree pointwise: at four specific placements, one with a point exactly on the edge, they return the same nine-digit rationals. Twenty-three rejection tests check that the Rust checker refuses mutated certificates, two invalid covers from our own history, and nine malformed files (on which it must give no verdict at all).

$ verify2/target/release/zmcheck cert certificates/rung2/s13_closed_cover_4.txt --depth 18 --threads 8
certificate certificates/rung2/s13_closed_cover_4.txt: container [0,4]^2, 3621 points, D=1000 W=1000000000
total weight = 12955972155/1000000000 = 12.955972155
done in 1065s: boxes 30258, max depth 10
  leaves: ADM 5114  DISJ 9477  EMPTY 6938  UNCERTIFIED 0
VERIFIED: every closed unit square in [0,4]^2 captures weight >= 1; total weight 12955972155/1000000000 = 12.955972155

theorem s13_ge_4 : (4 : ℝ) ≤ minSide 13
theorem s13_eq_4 : minSide 13 = 4

In Lean 4 with Mathlib, minSide n is the infimum of the sides that hold n closed unit squares at arbitrary positions and angles with disjoint interiors: the usual s(n). The covering property is checked inside Lean's kernel: a generated tree of pose boxes, 209 chunks, each decided by decide +kernel against a zero-margin verifier whose soundness is proved once, for every tree (ZMTree.sound). The program that builds the tree is not trusted: a wrong tree only makes the check fail. The same verifier, unchanged, later checked s(32) = 6.

What remains trusted is Lean's kernel, Mathlib, and the definitions in the statement (minSide and what a packing is). No sorry, no native_decide; #print axioms gives only propext, Classical.choice, Quot.sound. Separately, lean/Sqpack/ZeroMargin.lean proves the primitives both checkers of §04 rest on. This is not the first kernel-checked proof of s(13) = 4: chelokot's archive has one following Bentz's argument (§02).

$ lean/scripts/gen_data.sh S13 && (cd lean && lake build Sqpack.S13Lower)   # ~9 min on 4 cores

• This is a computer-assisted proof and has not been peer reviewed. The covering property is checked by two independent programs and by Lean's kernel; the Lean statement rests on the definitions of minSide and of a packing, which are short and open to inspection.
• The theorem was known. What is new is a proof with no case analysis, and a method that carries on to other boxes: side 6 with points only, side 5 and side 7 with part of the weight spread along the grid lines.
• It says nothing about s(12): every cover of this box weighs more than 12.2688 (the s(12) write-up).

Everything is in s12/ of evand/square-packing. ./verify.sh runs the zmcheck sweep and the rejection tests; the Python checker is the slow path:

$ python3 search/zeromargin.py cert certificates/rung2/s13_closed_cover_4.txt --depth 18 --nproc 8 --disj --chain-from 0