AI-assisted proof of optimal packing for 11 squares (github.com)

It is not as arbitrary or ugly as it may seem at first - see the image here and the explanation: https://x.com/davidmbudden/status/2107646435659481548

fwiw The prime site for square in square packing is at https://kingbird.myphotos.cc/packing/squares_in_squares.html

The triangular view is most interesting. And a 20 minute video on this view is at https://youtu.be/uL5wuiy34rs

I'm working on a reproduction of the proof with some personal changes. The basic approach is the standard computer assisted "unavoidable set" approach. First, choose some regions small enough that two square's centers don't fit in the same region, the article used 16. Each region must contain or not contain a square, which is 16 choose 11 cases, about 2000. For each case you try and rule it out. You do this by identifying areas that must be covered by a square, and propagating this information. You can also use packing LPs like Stromquist did in 1989 to rule out more configurations. You then narrow in on the remaining cases and subdivide them more.

I think the only reason this wasn't done pre-AI was due to it not being a topic of serious focus. 1989's computers were too weak to handle all the cases. But all the basic ingredients were present in the Kepler conjecture proof. What AI did was lower the effort enough that amateurs who just liked square packings could perform and formally verify such a proof. I consider myself among such amateurs. So this isn't a case of AI stealing mathematicians proofs, or doing something superhuman, its a case of democratization. I am concerned about how AI is affecting math and how the AI companies are behaving, but this isn't the case to be worried about. The calculations for proving this arrangement optimal will always be too big to be checked by hand. However, I'm hoping to produce some nice visualizations of the packing LP or core overlap that rejects each configuration

A list of many square packings, with images:

https://jlevy.github.io/squares/

For a joke version of this: https://x.com/bookazoid_/status/2107771851229610331/photo/1

A keypad that uses 11 squares packing

The readme has no figures :( describing the packing?

Lot more pics here: https://jlevy.github.io/squares/

One of the greatest classes I ever took was "Cybernetics", taught by David Huffman ("the" Huffman). he started out the very first day talking about information theory, into sphere packing, and on to applications of sphere packing to communications.

I distinctly remember him concluded with something like "Sphere packing is hard, except in 11 dimenions" or something like that, but when I look at the history, I can't see how he knew that in 1994?

Did an interval-arithmetic branch and bound once, getting the rounding modes right took me weeks.

It took me a hot minute to understand what square packing really means (the Wiki is insightful) but TLDr: it's packing unit squares (1x1) into a larger, arbitrarily sized square. When the larger square has a side length that is not an integer, it becomes non-trivial to determine the most 1x1 squares that can be placed inside/packed.

Wow, I never would have imagined one could prove optimality for that accursed beautiful thing.

So this is a proof that the Walter Trump packing is the optimal packing?

A short problem description on the github page would have been nice.

Another interesting video related to these types of problems: https://youtu.be/mVH7OPx4QZU

Isn't this obvious? Why do you need a proof for it, just stack the cubes next to each other? If we're talking infinitesimally thin squares, then stack them on top of each other? Am I missing something?