The Atlas of Square Packings

The Frontier Survey

For each number $n$$n$ of unit squares, $s(n)$$s(n)$ is the side of the smallest square that holds them without overlap. The frontier survey records the best-known packing and the strongest verified lower bound for each of the 324 cases the project tracks, with its provenance: 77 have a proved optimum and 247 are open. Every row is read from the case’s record, packing/frontier/n-NNN.md, when the page is built; nothing on it is typed by hand.

Audited sources. The survey audits what it records. The earliest published proof of $s(7)=3$$s(7)=3$ carries four recorded defects in its printed route, so the record for seven squares rests the case on independent later proofs. The literature archive keeps each primary source, a cleaned transcription and the unedited extraction it was checked against, and the evidence inventory shows what each claim rests on and who did the work.

Recent results. Red indicates a recent result, since 22 August 2026. Of the first hundred cases, 81 have a lower bound published or proved since then, reported or verified; 81 of those have a recent verified one; 0 of the 81 are this project’s, and 26 are new exact values. For 218 recent verified bounds, corrects Nagamochi 2005 says the bound stands in for a published result found unsound, the register’s T-007: Lemma 1, on which Theorem 2’s proof rests, is false.

Seventeen squares. Before this project’s work began, seven authors had published lower bounds for seventeen squares, some also for eighteen, all independently: Brandwijk’s $89/20$$89/20$ (18 July), Burns’s $4.4811$$4.4811$ (6 August), MacIver’s $4.4502\dots$$4.4502\dots$ (8 August), Mira’s and Fort’s sixteen-point sets (10 and 11 August), anabologyco-maker’s $4.57$$4.57$ and $9141/2000$$9141/2000$ (13 and 16 August), and Massaccesi’s $4.5058$$4.5058$ (21 August), replayed here as T-015 and T-016. The seventeen-square record lists them all; each has since been superseded. On 12 October 2026 two proofs that Bidwell’s 1998 packing is optimal were published by separate routes: Overbeck’s candidate proof (T-153) and Fitzharding’s Lean 4 proof (T-154). The case is reported proved; neither proof has yet been replayed in full here, so its verified bounds are unchanged.

Reported and verified. The best known packing and the reported lower bound are what the published sources say, credited to whoever found or proved them. The verified columns hold only exact formal bounds: a complete proof, an exact algebraic replay, or a rigorous certificate. An external certificate counts once it is replayed here in full and its mathematical assumptions are discharged, and each record says who ran the checks and how independent they were. Where the verified bound equals the reported value, the cell says ✓ same, which says nothing about who checked it. A published proof counts whether or not anyone here has read it, so where every argument behind a verified bound is a published proof nobody here has read, the cell says published proof, not read here. A reported bound that stands on a proof whose reading here found a defect, and that no verified bound reaches, says defect recorded under its credit. A finite-precision result is numerically checked and never enters a verified column.

The other columns. Recent sorts recent verified bounds first. The gap is the verified upper bound minus the verified lower bound, exact where both are closed forms and zero where the case is solved. Records links each case file. Values that are roots of a polynomial are shown as decimals, cut rather than rounded.

A row’s details. Open a row for its case record: the best packing known drawn large, the number line of its bounds, then how its packing was built, the polynomial behind a decimal, the sources, how its bounds were verified and the evidence entries behind them. The same record opens from the overview’s atlas, and has an address of its own to share.

Click a column heading to sort; the filters narrow the rows.

Best Known Results for n ≤ 324