Call the answer s(n). For a perfect square number of squares it is obvious; for most other n nobody knows. There is only the best packing anyone has found and a proven floor beneath it. This atlas draws every record packing from Erich Friedman's and David Ellsworth's catalogue, lets you take them apart and shows how the exact results are proved. It also has computer-checked results of our own: proofs that 21, 32 and 45 squares need sides 5, 6 and 7, a better floor for 12 squares, and a proof for 13 with no case analysis. All are unrefereed.
Thirty-two unit squares need a square of side 6. As far as we know the first exact value of s(k² − 4) for any k ≥ 4; checked by two independent exact checkers and in full inside Lean's kernel.
Twenty-one unit squares need a square of side 5. The proof puts most of its weight evenly along the grid lines instead of on points; two independent exact checkers, and a Lean theorem from their covering statement.
Forty-five unit squares need a square of side 7: the s(21) method one size up, checked by the same two exact checkers. Not in Lean yet.
A floor for twelve squares, up from 3.7889 and still the best we know of, checked exactly over every position and angle and in full inside Lean's kernel. Also our floor for eleven squares, since overtaken by others.
Bentz's theorem from one weighted cover, with no case analysis; checked by two exact checkers and in full inside Lean's kernel.
Every record packing, with its angles, contacts, free squares and smallest gaps measured. Start with the famous 17.
All the packings found for one n, oldest first, and a slider that morphs one into another.
Best packing versus proven floor for n up to 100, and how the gap has closed over time.
How you prove no better packing exists: unavoidable points, with a playground for the 12-square case, and what the method has proved.
Who found what, when; papers, pages, videos. One list.