{"id":"palomar/PALOMAR-2026-10-02-000002","url":"https://github.com/vltanh/lean4-squares-in-circles/tree/621f2340a12f661a51b613719107a75cf40ab03a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-02-000002-v1.json","repo":"https://github.com/vltanh/lean4-squares-in-circles","tags":["math.MG","msc:52C15","discrete-geometry","packing","optimization"],"score":0,"title":"Optimal packings of one to seven unit squares in a disk","trust":"high","domain":"math.MG","source":"palomar","authors":["The-Anh Vu-Le"],"reviews":0,"subject":"math.MG","summary":"For n = 1, …, 7: the least radius of a closed disk holding n unit squares with disjoint interiors, each placed and rotated freely, and every packing that attains it. The radii are √2/2, √5/2, 5√17/16, √2, √(5/2), √q* ≈ 1.68854 and √13/2, where q* is a quartic irrational. Up to rotation about the disk centre and relabelling, the optimal packing is unique for n ≤ 6: the square, the 2 × 1 rectangle, the T, the 2 × 2 block, the plus, and for six squares a central square with four neighbours, two of them pushed along its sides, and a sixth square turned by π/4 between those two. For n = 7 the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-02","reactions":{},"formalized":true}