Squares in Rectangles

Call the rectangle's sides s ≤ ℓ (short and long). The squares are closed unit squares at any positions and angles, inside the rectangle, with disjoint interiors. Every square needs s ≥ 1, and two squares need ℓ ≥ 2, since otherwise every unit square in the box contains the box's centre in its interior. For three squares or more, tilting starts to pay.

In the plot, a point is a rectangle: short side across, long side up. The shaded region is the set of rectangles that hold n squares; its lower edge is the boundary, with the tilted pieces in gold. Click or drag along the boundary, or use the slider, to see the packing that sits exactly on it. Every packing is drawn from the construction proved in Lean.

Each boundary point is attained: the packings drawn are in the closed rectangle, touching where they look as if they touch. Inside the shaded region more room is to spare; below the boundary, the theorem says no packing exists at all, at any angles. The vertical pieces at s = 2 are where the short side reaches 2 and the squares can be stacked two high.

All three boundaries, and every packing on them, are in Erich Friedman's Math Magic problem of the month for June 2010. Friedman asks for the region S_n of rectangles that hold at most n unit squares, so the boundary of S_n−1 is the boundary we want for n; his x is our long side ℓ and his y our short side s. The page names that month's solvers as Maurizio Morandi, Evert Stenlund, David W. Cantrell and Hiroaki Hosono, and gives an author for some of the pieces in its table:

The table gives authors by initials only. MM matches Maurizio Morandi, the only named solver with those initials. The page was last updated in February 2019 and gives constructions, not proofs.

Other earlier work bears on these three cases:

• s(5). The square case of the five-square theorem, s(5) = 2 + 1/√2, is Göbel's (1979). Our proof for both sides at least 2 starts from the same four unavoidable points, in the form given in Friedman's survey of square packing (§04).
• The 1:2 rectangle for four squares. Friedman's page Squares in Dominoes lists four unit squares in 1.930 × 3.861, found by Evert Stenlund in 2010. It lies on the four-square boundary (marked in the plot).
• Three squares. Yang (arXiv:2608.13595, 2026) determines the largest total side of three squares of any sizes in a 1 × x rectangle. Rescaled, this settles three equal squares in every rectangle except the region 1.5 ≤ s < 2, max(s, 3 − s/2) ≤ ℓ < 3 (dotted in the plot for n = 3). Friedman's wedge lies inside that region.
• Constructions with certificates. wand125's square-packing repository (problems/rectangles/) lists the same boundary pieces, with closed forms and certified constructions, and no lower bounds.

Our part. We came to the three-square case by a numerical search, found the 45° wedge, and took it for new; a day later we learned it was in Friedman's table (posted in 2010, last updated in 2019). We then used his tables as the target for four and five. What is new here is the other direction: the proof that nothing below the boundary can be packed. As far as we know these are the first proofs of these lower bounds, for n = 3, 4 and 5, and the first theorems about squares in non-square rectangles in any proof assistant.

When the short side is 2 or more, all three answers are easy for n = 3 and 4: two rows fit. The work is in strips [0, L] × [0, H] with H < 2. There the squares cannot be stacked: each centre lies between heights ½ and H − ½, so any two centres differ in height by less than H − 1 < 1. That makes the squares a chain, left to right.

1. Sort and separate. Sort the squares by the x-coordinate of their centres. Two squares with disjoint interiors are separated by a line (in Lean: Hahn–Banach, from Mathlib). Because neighbours are less than one unit apart in height, the line between them always has the left square on its left.
2. The shelf. Take the first square a and its line. Replace a by an upright unit square pushed against the left wall, level with the top or the bottom of a. The upright square is still on a's side of the line. (This is one elementary trigonometric inequality, upright_repl.) So the second square b, on the other side, cannot reach left of x = 1 anywhere within that unit band of heights. That is a shelf. The last square gives a shelf at x = L − 1 on the other side.

Three squares. Now b sits alone between two shelves, and the whole question is how short L can be. Which point of b a shelf stops is one of three: the corner of b that points at the shelf, if it is at a height inside the band, or else the point of an adjacent edge at the band's top or bottom. That gives 3 × 3 cases, each a real inequality in b's angle. Seven give L ≥ 3 outright. The two where b stands on the floor or hangs from the ceiling with an edge on each shelf give L + 2H ≥ 4 + 2√2, with equality only at 45°: Friedman's wedge.

The step that makes this short is the shelf: once the neighbours may be taken upright, a single square against two shelves carries the whole boundary. The Lean proof of rect3_iff is 171 lines, on top of 418 lines of chain tools reused below.

Four squares. Sort a, b, c, d. Square b has a shelf on its left (from a), c a shelf on its right (from d), and a line at some angle t separates b from c. Two more steps:

• One square against a line (one_square). A unit square in the strip with a left shelf, lying to the left of a line at angle t, pushes the line at least as far right as one of two explicit squares would: an upright square at the ceiling, or the square tilted by t on the ceiling against the shelf's corner, with an edge along the line. The proof is the same three witness cases, plus two inequalities in two angles that factor after the half-angle substitution u = tan(θ/2).
• A half turn. Rotate the right half of the picture by 180° about the centre of the rectangle. Then c becomes a square with a left shelf, against a line parallel to the first. The one-square bound applies to both b and the turned c, and the two bounds add up to L ≥ 4 or L ≥ L(t, H).

So the minimum of L(t, H) over t is exactly the boundary, and rect4_friedman shows that the packing exists for every t with L(t, H) < 4. The tilted piece runs from H = 1.8816489, where it meets the row of four, up to H = 2, where t = 45° and L = 4√2 − 2 ≈ 3.657. Lean: 592 lines.

With both sides at least 2 the chain breaks: squares can stack. For five squares this part of the boundary contains the square 2 + 1/√2, and we use the method that proves s(5): unavoidable points, here with weights.

Four points (for 4 − √2 ≤ a ≤ 2 + 1/√2 on the line). The points (1, 1), (a − 1, 1), (1, b − 1), (a − 1, b − 1), weight 1 each. Split the possible centres into nine cells: near a corner the corner point is caught; along a wall, one of the two points on that wall (the side-strip lemma of Friedman's survey, which needs the gap between them at most 2√2 − 2); in the middle, a new lemma: a unit square whose centre lies in an X × Y rectangle with X, Y ≤ 1 and X + Y ≤ √2 contains one of the rectangle's corners. At a = b this gives s(5) = 2 + 1/√2, by essentially the classical argument with the centre handled by the rectangle lemma.

Cover C (for 1 + √2 ≤ a ≤ 4 − √2). Here the side-strip lemma fails: a square at 45° sitting against a long wall slips between the two points on it, and a numerical search found no set of four points that works. A linear program over fractional weights found covers, and one simplifies to ten points:

• weight 2/3 at (0.91, 1) and its three mirror images;
• weight 1/3 at the four points above, (1, 1) and mirrors;
• weight 1/3 at (1, b/2) and (a − 1, b/2) on the midline.

Total 14/3 < 5. Every closed unit square in the box contains a whole block of weight exactly 1: a row pair {(0.91, 1), (1, 1)}, a wall pair {(0.91, 1 or b − 1), (1, b/2)}, or a centre triple {(1, 1 or b − 1), (1, b/2), (a − 1, b/2)}, up to mirror images. The Lean proof splits the centres into three cells, each closed by short lemmas of the same kinds as above (corner, side strip, and a variant of the centre lemma).

Drag the square, turn it with the slider (or the mouse wheel), and try to catch less than weight 1. The small map shows the weight caught for every centre at the current angle; gold is exactly 1, where the cover is tight. The box follows the boundary line a + b = 4 + √2 (for cover C and the four points) or the strip 5 × H (§05). The page samples; the Lean proof covers every position and angle.

Low strips, H < 2√2 − 1 ≈ 1.828. Four points on the midline, (1, H/2), …, (4, H/2), in the 5 × H box: every unit square in it contains one (select "low strip" above). Between two midline points this is the side-strip lemma again, with gap 1 at height H/2, and its condition 1/2 + H/2 ≤ √2 is exactly H ≤ 2√2 − 1. So in low strips five squares need length 5. Lean: 98 lines.

High strips, 2√2 − 1 ≤ H < 2. This contains the zigzag, Friedman's piece ℓ + 4s = 4 + 6√2 for s ≥ (6√2 − 1)/4 ≈ 1.8713.

The chain applies as before: shelves on b and d, lines between b and c and between c and d. A concavity argument (in Lean) shows that the middle square is narrowest between the two lines when it is upright or parallel to one of them. What is left is one real inequality in the two lines' angles and the height. But the two halves now see different lines, coupled through the middle square, and the natural ways to decouple them lose (numerically, by 0.1 or more); one split that loses nothing has not been turned into a proof yet. We proved the remaining inequality by machine:

• half-angle substitution makes it polynomial; it splits into 64 case theorems and 160 polynomial inequalities on boxes;
• 144 are not tight and are linear in H, so it is enough to prove them at the two ends of its range. All but two are proved there by Handelman certificates: the polynomial is written as a positive combination of products of the box constraints (u ≥ 0, 1 − u ≥ 0, …), found by a linear program and checked by Lean's linarith;
• 16 are tight: they hold with equality along the zigzag, at both angles 45°, for every H in the zigzag range. Those are proved by an exact factorisation that exhibits a squared factor;
• the remaining two vanish only at corners of their box and are proved by hand.

That is 14,411 lines of generated Lean, about 5 minutes to build on 16 cores (70 CPU-minutes). It was not a surprise to need certificates at n = 5, though we had hoped to put them off to larger n. A structured proof of this step is open.

git clone https://github.com/evand/square-packing && cd square-packing/lean
lake exe cache get              # Mathlib
lake build Sqpack.Rect3         # rect3_iff     ~15 s
lake build Sqpack.Rect4         # rect4_iff     ~15 s
lake build Sqpack.Rect5Thm      # rect5_iff     ~5 min on 16 cores, mostly the generated files
lake build && lake env lean Axioms.lean

The statements use one definition, RectPacks n w h: n closed unit squares, at any centres and angles, each inside [0, w] × [0, h], with pairwise disjoint interiors.

Research notes: search/rectfront/RECTFRONT.md (the log), LESSONS.md (techniques, what failed), r5pts/R5PTS.md (point covers, with paper proofs), r5strip/FINAL5.md (the certificates).

• These are machine-checked proofs, not peer reviewed. What Lean checks is the statement of rect3_iff, rect4_iff and rect5_iff against the definition of RectPacks; read those (a few lines each) to see that they say what this page says.
• The high-strip part of the five-square proof is generated and teaches little. The rest is written by hand.
• Credit for the boundaries is as far as we could trace it (Friedman's page, §02). If you know of earlier proofs of any of these lower bounds, please tell us.
• Six squares and up are open here. Friedman's table lists boundaries up to S₉ (n = 10), with higher-degree algebraic curves from n = 7 on; wand125's lists go to n = 15 and lower one piece for n = 7.