Packing tiny reciprocal rectangles into matching squares is possible late in the sequence
Packing Tails of Reciprocal Rectangles into Squares of Equal Area
Discrete Mathematics
Summary
There is a famous puzzle asking if many tiny rectangles, each getting smaller by a specific formula, can all fit inside a square without overlapping. The authors show that if you look far enough into the sequence (only for large enough indices), you can fit all these rectangles exactly into a smaller square whose area matches the sum of all the rectangles’ areas. Their proof uses a clever mix of geometry and randomness, and they even verified the details with formal computer checking. However, this does not solve the puzzle for the entire original set starting at the first rectangle, which remains an open question.
What this means in practice
- •For geometric algorithm designers: Use the tail packing method to guide design of algorithms that approximate tight packing of many small rectangles without overlap.
- •For formal verification engineers: Leverage the Lean 4 formal proof techniques demonstrated in this geometric packing problem to verify complex constructive proofs.
A theory result. No direct application yet.
Authors
Yu Jiang
Abstract
The Meir--Moser rectangle-packing problem asks whether all rectangles with side lengths \(1/n\) and \(1/(n+1)\), for \(n\ge1\), can be packed into the unit square with pairwise disjoint interiors. We establish a tail version of this problem. Let \(R_n\) denote the rectangle with these side lengths. We prove that there exists an integer \(m_0\) such that, for every \(m\ge m_0\), the family \(\{R_n:n\ge m\}\) admits a packing, by translations and right-angle rotations, into a square of side length \(m^{-1/2}\), with pairwise disjoint interiors. The area of the square equals the sum of the areas of all the rectangles. The geometric construction recursively decomposes rectangular gaps, while local randomized quotas and random permutations assign subsequent integer indices. We separately control the total area of waiting gaps and the assignment load at each index. The proof is organized in six steps: a finite-prefix reduction, geometric row decompositions, an area bootstrap, a sharp source-load estimate, control of the actual adaptive construction, and a compactness limit. For every finite time horizon, the probability of failure has a bound that is independent of the horizon and can be made arbitrarily small. The adaptive step uses a permanent load ledger, actual fresh height queries, and a one-sided comparison with a frozen source experiment. Compactness then yields an infinite packing. The final packing statements have been checked in Lean 4. A sufficient threshold is \(m_0=10^{1000}\). This result applies only to sufficiently late tails and does not resolve the original Meir--Moser rectangle-packing problem for the full sequence starting at \(n=1\), which remains open.