We provide a tight result for a fundamental problem arising from packing squares into a circular container: The critical density of packing squares into a disk is $delta=frac{8}{5pi}approx 0.509$. This implies that any set of (not necessarily equal) squares of total area $A leq frac{8}{5}$ can always be packed into a disk with radius 1; in contrast, for any $varepsilon>0$ there are sets of squares of total area $frac{8}{5}+varepsilon$ that cannot be packed, even if squares may be rotated. This settles the last (and arguably, most elusive) case of packing circular or square objects into a circular or square container: The critical densities for squares in a square $left(frac{1}{2}right)$, circles in a square $left(frac{pi}{(3+2sqrt{2})}approx 0.539right)$ and circles in a circle $left(frac{1}{2}right)$ have already been established, making use of recursive subdivisions of a square container into pieces bounded by straight lines, or the ability to use recursive arguments based on similarity of objects and container; neither of these approaches can be applied when packing squares into a circular container. Our proof uses a careful manual analysis, complemented by a computer-assisted part that is based on interval arithmetic. Beyond the basic mathematical importance, our result is also useful as a blackbox lemma for the analysis of recursive packing algorithms. At the same time, our approach showcases the power of a general framework for computer-assisted proofs, based on interval arithmetic.
Download