Comment by DevelopingElk
4 hours ago
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.