-->

Another Better Lower Bound for n=17 Square Packing - Gustavo

2026/08/21

Another Better Lower Bound for n=17 Square Packing

The idea is to improve a recent result and prove that 4.5058(?)≤s(17) using these weights:

But let’s first define s(17). Quoting the old article about the topic

Let s(n) be the side of the smallest square into which we can pack n unit squares.

For n=16, the best is obviously a 4x4 array, so s(16)=4.

For n=15, the 15 unit squares can also obviously be enclosed in a 4x4 square so s(15)≤4. Proving that it’s the smaller square is not obvious at all. Anyway, Erich Friedman proved that in 1999, so s(15)=4

For n=17, the obvious enclosing square is the 5x5, but in 1998 John Bidwell found an example that shows that a square of 4.6756… is enough, so s(17)≤4.6756… It’s a very interesting arrangement of the squares, so it’s worth visiting the collection to see it and the versions for other numbers.

On the other hand, Trevor Green proved in 2000 that 4.4452…≤s(17), (more details later). So there was a huge gap 4.4452…≤s(17)≤4.6756…

A few weeks ago, Sam Burns with ChapGPT 5.6 Sol improved(?) the lower bound. The new bound is still not reviewed by the community. I took a look and it makes a lot of sense and I think it’s correct, but I may be missing a small corner case in the proof or the accompanying program, or I may be missing a huge hole. I’ll add a small (?) to the number just in case, but I’m quite optimistic and confident it’s correct so I’ll use only a half font size. So the current bound is 4.4452…≤4.4811(?)≤s(17)≤4.6756…

My main objection to Sam Burns is that it really deserved a nice graphic! So my first step will be to add a nice graphic here. Also, making a few improvements to the program, I found a new lower bound that is 4.5058 So now we have 4.4452…≤4.4811(?)≤4.5058(?)≤s(17)≤4.6756…

My new example and the modification of the code are here, but the more technical details about finding the new bound are part of a second post.<br>Trevor Green’s bound

The idea of the old proof (19+40*sqrt(2))/17≅4.4452…≤s(17) of Trevor Green is to pick 16 very interesting "unavoidable" points in a square of side 4.4452… and then he uses a lot of geometry to prove that any unit square must include at least one of them. So if we try to fit 17 unit squares there, at least two unit squares must share one of the 16 interesting points. The construction chooses 16 points out of a 4x6 grid.

I only found an image of the points in the old article, but I couldn't find the analytical definition. Looking at the formula for the side of the square, and using a rule, and some guessing, I think that the empty left/right margin is 0.5 and the empty top/bottom margin is sqrt(2)-1/2≅0.9142… With these choices, the diagonal segment in the original graphic has length 1, which is a very useful number to make triangles that have vertices that are unavoidable points. (I’d be glad to hear a confirmation.)

It uses a 6x4 grid with an empty margin of 0.9142… and 0.5000, and the total size of the grid is 2.6168… and 2.4452…

To compare the construction to the<br>newer constructions, it’s better to symmetrize it. In this symmetrized<br>version each unit square includes at least 4 points, but some points are<br>thicker, and they count as double points (more details later).

Sam Burns’ bound

The idea to prove 4.4811(?)≤s(17) posted by Sam Burns using ChatGPT picks 268 somewhat interesting points in a square of side 4.4811 The points have different weights, and the total weight is only 16.9476. After some reductions, it’s only necessary to test a finite number of directions and they use a program in Python to test "all" the possible "almost-unit" (actually .9973) squares and verify that the sum of weight inside each one of them is at least 1 (actually 1.0003). So if we try to fit 17 unit squares there, at least two unit squares must share at least one of the 268 somewhat interesting points. (More details in the second post.)

This method has false negatives. If it verifies a solution then it’s surely correct, but if the program fails there is a tiny chance that it’s a mistake. This is fine to ensure the weight proves a lower bound.

It’s not clear how the weights were selected. Comparing this solution to all the examples in the old article, the 0.5 margin is too narrow because most examples use ~1.0 or ~9.1 or something like that. The selections of weight agree with me, and all the weights in the first/last row/column of the grid are zero. In my handwaving opinion, the second/penultimate row/columns should be empty too, but there is a non-zero weight in (1, 11) of the grid and the symmetric images, I hope it is not necessary in a better example. The third/penpenultimate row/column is quite full. It’s closer to the border than in the old examples, so it looks like adding more points near the border may be a good idea to improve the bound.

I draw the images using Racket with the Metapict package. The radius of each circle is...