Finding a good packing is a search. Proving that nothing smaller can work is a different job: you have to rule out every arrangement at once, including ones nobody has thought of. Almost every proof in this subject uses one trick, due to Frits Göbel (1979): unavoidable points.
Suppose you want to show that n unit squares can't fit in a square box of side s. Scatter some points in the box so that every possible position of a unit square — anywhere, at any angle — covers at least one of them. If you managed it with fewer than n points, you're done: n squares with no overlap would each need their own point, and there aren't enough to go round.
The whole art is choosing the points. Near a wall a unit square can't tilt much without poking out, so a row of points about 0.9 from each wall catches everything there. In the middle, a triangle of points with sides ≤ 1 can't be dodged (a unit square whose centre is in the triangle must cover a corner of it). Stitching such lemmas together over the whole box is the proof.
A sharper version asks each point to be hit not once but k times: if every unit square covers at least k of m points, then at most ⌊m/k⌋ squares fit. Below is a real one.
Drag the square around and rotate it. The points it covers light up and the count is shown. Try to get it below 7 — you can't, but the places where it is exactly 7 tell you what the points are for.
The map samples 120 × 120 positions; the real proof checks the whole continuum of positions and angles with exact integer arithmetic (an open-source verifier). The Lean proof assistant checks it all again, the covering property included, inside its kernel: s(12) ≥ 35/9 is a Lean theorem with no hypothesis. Points exactly on the square's edge count as covered. That convention is what lets a packing in any smaller box be scaled up into this one and refuted, which is why the conclusion covers every box smaller than 35/9. The skeleton is the same in every such set found: a # of lines one unit from each wall, and a small ring at the centre.
Everyone believes s(12) = 4: the plain 4 × 4 grid with four squares missing. The best proven floor is now 3.9686, our own result, computer-checked (and kernel-checked in Lean) but not refereed. It uses a weighted version of the same argument, where a linear program chooses fractional weights for the points, an idea from Sam Burns's and Gustavo Massaccesi's 2026 work on n = 17 (Sources §5). Weighted points alone cannot finish the job: at box side 4 no weighting of points totals less than 12.27 (proved exactly). Closing the last 0.03 needs something more, such as the case analysis used to prove s(13) = 4, next.
Bentz works in [0,4]² with boxes, each the inside of a square of side a little more than 1. If 13 boxes never fit, then s(13) = 4. He starts from 16 unavoidable points (in the figure). Thirteen boxes against sixteen points leave three points of slack. That is enough to force at least two boxes to sit alone with a corner point, where a replacement lemma pins them down further. The argument then splits on whether those two boxes share a corner, and the split has six leaves.
Click through the leaves and watch the number in the tree: every branch ends at 12. The bookkeeping is "free points + boxes already placed", and a contradiction needs that total to be under 13. Each configuration Bentz builds is, in effect, a certificate worth exactly 12 — so it kills a thirteenth box and nothing more. For 12 squares every leaf would have to come out at 11 instead, and only one of the six does. The loss starts at the very first step: with 12 boxes and 16 points the slack is 4, all eight corner points can pair up in four boxes, and there is no lonely box for the replacement lemma to work on. That single missing unit is why the same proof says nothing about s(12).
The six leaves above are the price of plain points. Give the points fractional weights, chosen by a linear program, and the case tree disappears: 3,621 weighted points in [0,4]², total 12.956, such that every closed unit square in the box captures weight at least 1. Thirteen squares would need 13. A point on a square's edge counts, which lets neighbouring tiles share weight. The margin is then zero, so the check is an exact subdivision of every position and angle, done by two independent checkers and by Lean's kernel. The theorem is Bentz's; only the proof is new: Thirteen Squares.
Twelve and eleven squares. Weighted points in a box a little smaller than 4 give s(12) ≥ 15680/3951 = 3.9686 (August 2026), still the best floor for twelve squares that we know of. The same method gave s(11) ≥ 3.8143, since superseded by jlevy's 3.827 and Kleddamag's 3.875.
Thirteen squares. The case-free proof above, the first of our covers of a box of side exactly k, where there is no margin to spend. It is kernel-checked in Lean; an earlier Lean proof of s(13) = 4, following Bentz's argument, is chelokot's (Sources §5).
Thirty-two squares. The same kind of cover at side 6: 13,085 weighted points of total 31.7135, so s(32) = 6. As far as we know, the first exact value of s(k² − 4) for any k ≥ 4. Kernel-checked in Lean with no hypothesis.
Twenty-one and forty-five squares. At sides 5 and 7, points alone always left a hole near some slightly tilted square. Spreading part of the weight evenly along the grid lines closes those holes: s(21) = 5 and s(45) = 7, each checked by two independent exact checkers. s(21) has a Lean theorem from the checkers' covering statement; s(45) has no Lean yet.
How they are checked. Each result is a statement about a continuum of positions and angles, so the checking is the proof. The certificates are exact files of integers. Each is checked by two programs that share no code; where the margin is zero they subdivide the space of placements until every piece is proved, with nothing sampled. Lean's kernel re-checks the covering property itself for s(11) ≥ 3040/797, s(12) ≥ 35/9 and ≥ 3920/997, s(13) = 4 and s(32) = 6; for the others Lean has only the reduction, or nothing yet, and the cover rests on the checkers. None of this is peer reviewed.
Others have used weighted certificates in 2026 too: on s(17) (Burns, Massaccesi, Mira, Guzhou0806, Kleddamag), on s(11) (jlevy, Kleddamag), and with rectangle densities for many n from 18 to 91 (tokoharu, wand125). Sources §5 lists them.