Another better lower bound for n=17 square packing

Show & Tell
1

I made an improvement of a recent blog post by Sam Burns where he uses ChatGPT 5.6 Sol to increase the lower bound from 4.4452... to 4.4811 that uses a program in Python as part of the proof.

I split my result in two parts:

The first part increases the lower bound to 4.5058 and use Racket with the Metapict package to make a few nice graphics of the weight distributions used in the proofs. It also has the program in Python with a few small modification for the new bound.

The second parts explains the use of linear programming to find the set of weight used in the new bound. (No Racket code there.) It has a version of the program in Python with more modifications and uses linprog in the scipy package.

At the start I was wondering to rewrite everything in Racket (beware of not so nice Python code in the second part), but I preferred to not add any weird corner case difference in the translation. Also, I was worry how difficult it would be to install the package for linear programming in Racket because it depends on external libraries.

Note that the post by blog post by Sam Burns uses AI and has not been published in a serious peer review journal. I reused the code, to the same remark applies for mine. I think the proof is correct, but there may be some error I did't notice.

S17-Massaccesi
S17-Massaccesi406×406 8.55 KB

2 Likes
2

Did you use any AI for your proof or code?

Does the "plt-linalg.plt” package on Planet supply the LP you need?
Or at least most of it?

— Matthias

3

Did you use any AI for your proof or code?

I didn't use AI, my modification in the code is all hand crafted. (Ignoring the free version of Gemini that runs in https://www.google.com/ . I never remember in Python how to do things, like removing a key/val from a dictionary).

Sam Burns used ChatGPT. I read the proof and the code and I think they are correct. His versions has a list of weights, and my version has just another list of weight and a different grid size. The program in the first part only has the few obvious modifications to use the new weights. The proof is exactly the same, changing a few constants here and there.

The interesting part (IMHO) is how I got the weight, that is in the second part. The idea is to use the same grid of weights, but assign to each one a variable for the linear programming method. So assuming the weight in the grid are a, b, c, d and some of them are repeated due to symmetry, at the end I have to solve something like

minimize: a+2b+c+d 
a+b+c  >= 1
a+2c   >= 1
b+c+2d >= 1
a,b,c,d>=0

but it's actually a problem with like 100 variables and 1000000 inequalities.

I think plt-linalg.plt can solve systems of equalities but not inequalities. I found GLPK that should solve my type of problem, but I was not sure about the external libraries required to run it.