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 topicLet 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)=4For 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.Trevor Green’s boundThe 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 newer constructions, it’s better to symmetrize it. In this symmetrized version each unit square includes at least 4 points, but some points are thicker, and they count as double points (more details later).Sam Burns’ boundThe 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 calculated from the weight as    r = sqrt(weight^(1/gamma)) * scaleWith gamma = 1.0 the area is proportional to the weight, but the small weights are too small in the image. After some tweaking, gamma=2.0 looks nice because the smaller weights are easier to see. The scale is not so mysterious, and I should have used pi somewhere in it, but scale=0.07 looks nice in my machine. The circles are semi-transparent, so it’s possible to see when they overlap if you ever increase the scale. The code is at the bottom, and it divides the weight by 1.0003 that is the actual minimal sum.New boundMy idea was to try different combinations of the margin and internal grid size. As I said, it’s not clear how the weights were selected in the example of Sam Burns. So for each fixed size, I decided to use linear programming to find them.Then I used a combination of brute force search and luck to get the best grid I could find. After that, I rounded the weight so they look nice and are nice fractions. (More details in the second post.)After a lot of time, the best I got is 4.5058(?)≤s(17). The new solution uses 168 somewhat interesting points in a square of side 4.5058 in a 29x29 grid. They sum only 16.9166… Each unit square includes at least a total weight of 1.There is an empty margin of 0.77565 and the internal grid has a total side of 3.9545.As I said, the weights are closer to the border than what I expected looking at the old examples, close to the second/penpenultimate row/column of the previous one. It also uses fewer weights, so I hope it’s easier to prove that it’s correct without a computer. I’d like to make a non symmetric version, that may be even better.The program published by Sam Burns assumes that the empty margin is 0.5, so I had to modify it slightly to allow arbitrary borders with a variable M that is the double of the margin. The version with that modification, the new sizes and the new table of weight is at the bottom. Running that program and making the obvious changes to the explanation posted by Sam Burns proves(?) the new bound.Conclusion and Future WorkThe distributions look quite discrete in the corner, but it has some strange bars near the center. It would be nice to increase the grid size and take a look. Also, the narrow empty margins appear to be useful.My search program in the second article is too slow (like 1 hour), so I avoided changing the size of the grid. It may be useful to explore other grid sizes in case there are some interesting coincidences. Adding more digits takes only a few minutes, I didn't bother because it looks like refining the grid or using more directions for the rotations would make bigger changes.This result also automatically improves the lower bound of s(18), s(19) and s(20). But a more deep search for those values should provide even better bounds. I’ve seen too many cases where the total sum of the weight is 18. There is something interesting about 18.I’d like to find the non-symmetrical version. I have some ideas to try, so check again in a few days. A non-symmetrical version hopefully has like 1/8 of the weight and hopefully shows the almost equilateral triangles and is easier to understand without a computer. You may like to read the second post with details about how I got the new weights. Program to verify the bound from __future__ import annotations from bisect import bisect_left, bisect_right from fractions import Fraction as F import numpy as np # Original version posted by Sam Burns 2026 # Modified by Gustavo Massaccesi 2026 # Proposed exact lower-bound certificate for packing 17 unit squares in a square. # # All geometric quantities and predicates are rational. NumPy is used only for # integer range-addition and cumulative sums; no floating-point geometry is used. L = F(45058, 10000) # side of the square M = F(15513, 10000) # both empty borders B = F(9973, 10000) T = F(207107, 500000) KMAX = 180 D = T / KMAX WEIGHT_SCALE = 576 # min weight NGRID = 29 LAST = NGRID - 1 # (i, j, w): every distinct D4 image of grid point (i,j) receives weight w/WEIGHT_SCALE.