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.
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 simpler way to see this is to first focus on the central region of the big square that's 0.5 units away from the edge. All squares centers must lie in this region. Break this region into a grid of 25 equally sized square tiles. Each tile is now small enough that the center of two squares can't lie within the same tile. This gives 25 choose 11 possibilities. The article instead broke this region into hexagons that were still small enough that the centers of two squares can't lie in the same hexagon. This let them use only 16 tiles, which vastly reduced the space of possibilities.
"God is dead and the optimal packing of squares killed him." I will never not think of this meme when looking at these horrors. I see it, but I don't like it. ;)
It’s unintuitive that a messy configuration of squares can be more optimal than neatly arranging them aligned. And by looking at all the current best solutions it does appear that the neat configurations are usually the best , but not always. How does one explain the messy cases?? Is that about how division can result in irrational numbers, and when the number of optimal squares approach one you end up with the messy 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?
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?
parent is changing the problem by suggesting to "pack in the 3rd dimension": lay all the squares on the same square footprint, resulting in always needing only a square with side length 1 on which all the needed "packed" unit squares are laid.
Look at some of the other links people have posted for optimal packings. The optimal 11 square packing looks nothing like what you're describing ("just stack the cubes next to each other").
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.
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
I really wish there were visualizations for this.
“Choose a region, where two squares don’t fit, -> 16(??)”
I consider myself literate (maybe not adept) with advanced maths, but this confuses me and requires a lot of assumptions on my end.
A simpler way to see this is to first focus on the central region of the big square that's 0.5 units away from the edge. All squares centers must lie in this region. Break this region into a grid of 25 equally sized square tiles. Each tile is now small enough that the center of two squares can't lie within the same tile. This gives 25 choose 11 possibilities. The article instead broke this region into hexagons that were still small enough that the centers of two squares can't lie in the same hexagon. This let them use only 16 tiles, which vastly reduced the space of possibilities.
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
Is there an explanation for this that isn't on X?
This is the paper that’s being referenced: https://pingyou.com/papers/eleven-squares.pdf
It’s not obvious to me that it has any deep significance.
Not clicking an x link, but good to hear
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
Can someone explain why 83 and 87 can't get any smaller?
Because the outer perimeter must be a square. 83 and 87 could shrink the outer perimeter in one dimension, but not in both at the same time.
It is possible they can; it’s not yet proven that the listed packings for 83 and 87 are optimal.
Which of the blocks do you think you could move to shrink the solution? Or are you thinking of a completely different arrangement?
They got updated to be smaller this year, so maybe there's still more gains to be had?
More on the 11-squares packing:
https://startupfortune.com/ai-models-formally-proved-walter-...
https://vplevris.medium.com/eleven-squares-one-tiny-gap-and-... (written just days before the new proof!)
https://jlevy.github.io/squares/cases/11.html
This is cool! Something seems broken in the representation for 1850 and 1765, squares are strangely intersecting.
edit: Or maybe something wrong with the way my browser (brave) is rendering it.
"God is dead and the optimal packing of squares killed him." I will never not think of this meme when looking at these horrors. I see it, but I don't like it. ;)
A list of many square packings, with images:
https://jlevy.github.io/squares/
I like geometry. These packings show there are ugly numbers, like 51.
heh, 105 is a mess
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?
There's a cool figure here: https://x.com/ojoshe/status/2107590622005924265
Any mirrors which don't require giving clicks to neo-Twitter, please?
1 reply →
The readme also appears to be entirely LLM-written.
I really don't get it. If you think you've done something cool, why wouldn't you want to talk about it in your own words?
I had the same thought! Pics please.
EDIT: I found it a few links down. https://jlevy.github.io/squares/cases/11.html
<https://en.wikipedia.org/wiki/File:Packing_11_unit_squares_i...> from https://en.wikipedia.org/wiki/Square_packing
Pics or it didn't happen
Lot more pics here: https://jlevy.github.io/squares/
It’s unintuitive that a messy configuration of squares can be more optimal than neatly arranging them aligned. And by looking at all the current best solutions it does appear that the neat configurations are usually the best , but not always. How does one explain the messy cases?? Is that about how division can result in irrational numbers, and when the number of optimal squares approach one you end up with the messy 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.
Wow, I never would have imagined one could prove optimality for that accursed beautiful thing.
A short problem description on the github page would have been nice.
So this is a proof that the Walter Trump packing is the optimal packing?
Another interesting video related to these types of problems: https://youtu.be/mVH7OPx4QZU
[dead]
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?
It takes less time for you to try to read about the question than to type this comment. I know the link doesn't contain visualization, but... come on.
The whole point is that you can fit more than by naively stacking them...
parent is changing the problem by suggesting to "pack in the 3rd dimension": lay all the squares on the same square footprint, resulting in always needing only a square with side length 1 on which all the needed "packed" unit squares are laid.
Look at some of the other links people have posted for optimal packings. The optimal 11 square packing looks nothing like what you're describing ("just stack the cubes next to each other").