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?
"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. ;)
I guess when my parcel arrives all crumbled it's because it was along other 23 parcels instead of 22 and the courier knows his optimal square packing solutions.
I am not a mathematician. Why can a square of s = N not usually fit N * N unit squares? For example S = 4, one would naively (I guess) think it could fit 16 unit squares (4 * 4), but if I’m reading the above correct the actual solution is 15 (with what looks like a unit-square-sized space left over). Same for S = 5, and S = 6, but not for S = 2, which fits the expected 4 unit squares.
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?
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?
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 squares don't fit, 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 regions 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
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 think the only truly trivial ones are for n = k^2. Even the solutions that have integer side lengths but aren’t completely packed by unit squares seem difficult to prove that they are the optimal s(n). I don’t know much at all about the problem though, just seems like if there’s any space at all you might be able to rotate or whatever to squeeze out some space.
It's the reverse order. First you pick how many unit squares you want to fit. Then you try to fit them in the smallest container square possible.
For example for 3 unit squares, the smallest size of the container square is 2x2. (But in a 2x2 container square you obviously can also put 4 unit squares.)
49 comments
[ 1.2 ms ] story [ 36.6 ms ] threadI 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?
https://jlevy.github.io/squares/
Probably obvious for people who try to find these tilings, but I thought it was neat.
The triangular view is most interesting. And a 20 minute video on this view is at https://youtu.be/uL5wuiy34rs
https://vplevris.medium.com/eleven-squares-one-tiny-gap-and-...
https://en.wikipedia.org/wiki/Walter_Trump
https://x.com/fermatslibrary/status/2032179976028475737
More on the new proof:
https://startupfortune.com/ai-models-formally-proved-walter-...
https://jlevy.github.io/squares/cases/11.html
edit: Or maybe something wrong with the way my browser (brave) is rendering it.
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?
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 keypad that uses 11 squares packing
For example for 3 unit squares, the smallest size of the container square is 2x2. (But in a 2x2 container square you obviously can also put 4 unit squares.)
Still an achievement, just funny.