Best known packing for 53 identical squares

The Square Packing Problem

The square packing problem is a simple and long-standing problem in geometry: what is the size of the smallest square that can hold $n$ unit squares, where the squares are free to rotate but cannot overlap? The side length of that smallest square is written $s (n)$ .

The value of $s (n)$ remains unknown for most $n$ . In many cases, $s (n)$ is known only to lie between an upper bound (the size of the enclosing square for the tightest packing ever discovered, such as $s (29) \leq 5.934$ ) and a lower bound (a size below which it is proved that no packing can exist, such as the reported $s (29) \geq 5.81$ ).

The Atlas of Square Packings

colors indicate distinct tilt angles shade indicates number of full-side contacts

100

Download PDF Explore the atlas

News

Fitzharding Reports a Lean Proof for 17 Squares

October 13, 2026

Optimality Verification

Fitzharding reports a Lean 4 proof that Bidwell’s 1998 packing of 17 unit squares is optimal: $s (17) = 4.67553009360455 \dots$ . It is the first proof-assistant proof of this value in the project’s records and uses a different argument from Overbeck’s candidate proof. T-154 remains reported at V0/C1; the full Lean build has not been replayed here.

The source comparison traces 32 of the 35 patterns to the project’s certified sub-pattern ledger, including eleven from Hosono (wand125). The review distinguishes those mathematical sources from Fitzharding’s formalization and reported build.

Published artifacts: Current 17-square Lean proof report.

First public: 2026-10-13 (publication evidence).

PRs and supporting records: #588 · Source and premise review.

Overbeck Reports a Candidate Proof for 17 Squares

October 13, 2026

Optimality Verification

Overbeck reports that Bidwell’s packing attains the 17-square optimum, $s (17) = L$ , where $L$ is Bidwell’s container side. T-153 retains the source, review and sampled checks as an unverified proof report at V0/C1. The optimum remains unverified here pending complete capture and tree replays.

Sampled work covers 34 capture rows checked by the producer and independently, three producer tree replays and an independently isolated root. The full capture computation and ten remaining trees have not been replayed. These samples do not confirm the whole proof.

Published artifacts: Current 17-square candidate-proof record.

Publication evidence.

PRs and supporting records: #560 · Candidate-proof review.

Ahmed Proves Trump’s Eleven-Square Packing Optimal

September 30, 2026

Optimality Verification

Ahmed’s Astra-assisted proof establishes $s (11) = T$ , where $T = 3.8770835900228141773078970601 \dots$ is the exact algebraic side attained by Trump’s construction. It rules out every smaller square container, allowing each unit square to rotate independently and permitting boundary contact.

The proof builds on work by Levy and Overbeck. A complete cover divides the problem into 2,184 cases, excludes 2,180 and handles the four symmetry-related survivors with an exact argument ruling out every side below $T$ .
The project completed all 2,180 exclusions and ten capture nodes, with an adversarial AI review of their mathematical composition. The computations share arithmetic and construction components with the source; they do not constitute a second independent proof method.
Status clarification, 1 October 2026: the revised review ladder rates T-060 at V3/C3. A second adversarial AI review and documented human oversight are still needed for V4/C4.

PRs and supporting records: #246 · Current eleven-square result · Current eleven-square optimality explainer · Ahmed’s original proof · Retained verification and reproduction limits · Mathematical audit and final acceptance · Revised verification and confirmation ladder.

All news

Recent Major Results

Date	Result	n	Credit	Rungs	Status	ID
2026-10-16 published	Fitzharding reports a Lean proof that Wainwright's packing is optimal, $s (19) = 3 + 4 \sqrt{2} / 3$	19	Fitzharding after Levy, Ahmed	V0 C1Optimality	reviewed	T-194
2026-10-13 published	Closed-form lower bound $s (N) \geq a (N)$ for every non-square $N \geq 49$ , reported	50–63, 65–80, 82–99, 101–120, 122–143, 145–168, 170–195, 197–224, 226–255, 257–288, 290–323	Hosono	V0 C1Lower bound	reviewed	T-180
2026-10-12 published	Fitzharding reports a Lean proof that $s (17) = 4.67553009360455 \dots$	17	Fitzharding after Levy, Ahmed, MacIver	V3 C1Formalization	reviewed	T-154
2026-10-12 published	Candidate proof that Bidwell's 1998 packing is optimal, $s (17) = 4.67553009360455 \dots$	17	Overbeck after Levy, Ahmed, Mira-acc, Guzhou0806, Maaz	V0 C1Optimality	reviewed	T-153
2026-10-03 published	$s (k^{2} - 4) = k$ for every integer $k$ from 5 up; $k = 5 \dots 18$ are the cases held here	21, 32, 45, 60, 77, 96, 117, 140, 165, 192, 221, 252, 285, 320	Daniel after Burns, Massaccesi	V0 C1Optimality	reviewed	T-081
2026-09-30 published	$s (k^{2} - 3) = k$ for every integer $k$ from 6 up; $k = 6 \dots 18$ are the cases held here	33, 46, 61, 78, 97, 118, 141, 166, 193, 222, 253, 286, 321	Daniel after Burns, Massaccesi	V3 C3Optimality	confirmed	T-064
2026-09-29 published	Trump's eleven-square packing is globally optimal	11	Ahmed after Levy, Overbeck	V3 C3Optimality	confirmed	T-060
2026-09-27 published	$s (21) = 5$ , by a mixed cover of points and grid-line segments	21	Daniel after Burns, Massaccesi	V3 C3Optimality	confirmed	T-052
2026-09-26 published	$s (32) = 6$	32	Daniel after Burns, Massaccesi	V3 C3Optimality	confirmed	T-051

About Result Verification All Results

Profiles

We track contributors and the authors cited in the square-packing record. Browse their profiles and credited work.

All Profiles

Report Your Results!

If you have new results or know of newer results, please file an issue to report them, including what name you wish to be used for credits. Agents will validate, tabulate, and cite your work once it is a confirmed record.

We also have a group chat. Contact ojoshe if you wish to join.

Report a Result

Papers

The first-principles tutorial introduces the problem. Three papers explain the lower bounds and optimality proof for eleven squares; the methods tutorial describes how record packings are found.

Part I

New Lower Bounds for Square Packing for $n = 11$

September 5, 2026

How weighted points and 2-of-3 threshold atoms prove T-018, T-025 and T-026,

s (11) \geq 3.8264 \dots

, with interactive figures.

Part II

A Review of the Certified Lower Bound $s (11) > 31 / 8$ for 11 Squares

October 5, 2026

Explains Marc Leonard Overbeck’s proof that

s (11) > 31 / 8

(T-037): five-site k-of-m charges, k-of-m charges on shrunken parents with strict cores, and a reoptimized certificate over 12,028 angle rows.

Part III

A Review of the Optimality Proof of the Trump Packing of 11 Squares

September 30, 2026

Explains Manasseh Ahmed’s proof that Trump’s packing is optimal,

s (11) = 3.8770835 \dots

(T-060): construction, case exclusions, capture and local isolation.

Methods tutorial

How Record Square Packings Are Found

October 8, 2026

How seeds, search, local refinement and exact checks produce record upper bounds.

Tutorial

Square Packing from First Principles

October 1, 2026

The problem, bounds, small examples, and how to read a packing result.

Advanced tutorial

Square Packing, Search, and Proof

October 14, 2026

Linear programs, exact certificates, search, regularization, and global optimality proofs.

View All Papers

Visuals

PDF

n = 1

to 324Every tracked case as its best-known packing, arranged in a triangle on one sheet.

View All PDFs View Visualizations

Squares Project Documentation

The code, the certificates, the literature archive and the documents that record all of this live in the Squares Project’s repository.

About the Project

More Resources

Repositorysq19

By Fitzharding

github.com/ofitzharding/sq19A Lean 4 proof that Wainwright's packing of nineteen squares is optimal, trusting Lean's compiler for its certificates.

1 result (at S5) · 1 record (at S5)

Repositorysq17-lean

By Fitzharding

github.com/ofitzharding/sq17-leanA Lean 4 proof that Bidwell's packing of seventeen squares is optimal, trusting Lean's compiler for its certificates.

1 result (at S5) · 1 record (at S5)

Repositorythe-seventeenth-square-candidate

By Overbeck

github.com/Kleddamag/the-seventeenth-square-candidateA candidate proof that Bidwell's packing of seventeen squares is optimal.

1 result (at S5) · 1 record (at S5)

Repository11SquaresOptimal

By Ahmed

github.com/Queuingtheorydotcom/11SquaresOptimalA computer-assisted proof that Trump's packing of eleven squares is optimal.

1 result (at S5) · 1 record (at S5) · 1 credit (at S3)

Repository11-squares-certified-bound

By Overbeck

github.com/Kleddamag/11-squares-certified-boundA certified lower bound for eleven squares.

1 result (at S5)

Repositorysquare-packing

By Daniel

github.com/evand/square-packingExact covers settling

n = 21

, 32, 45 and 60, and s(k² − 3) = k for every k ≥ 6; s(k² − 4) = k awaits its replay here.

36 results (4 at S4, 17 at S3, 14 at S2, 1 at S1) · 24 records (4 at S4, 11 at S3, 9 at S2) · 1 credit (at S3)

Repositorysquare-packing

By Hosono

github.com/wand125/square-packingCanonical certificate and checker repository; historical source pins remain valid.

28 results (1 at S4, 27 at S3) · 27 records (1 at S4, 26 at S3)

Repositorysquarepack-certs

By Fang

github.com/TheSnakeFang/squarepack-certsTwo-wedge packings of 308, 343 and 344 squares with exact certificates; the 308, below the grid, is replayed here (T-135).

2 results (1 at S4, 1 at S3) · Review pending

Repositorysquare-packing-density-bounds

By Tokoharu

github.com/tokoharu/square-packing-density-boundsRectangle-density lower-bound certificates.

1 result (at S4)

Repositorysquare-packing-bounds

By Hosono

github.com/wand125/square-packing-boundsWeighted point and rectangle-density lower-bound certificates across many n.

36 results (34 at S3, 2 at S2) · 25 records (23 at S3, 2 at S2) · Review pending

Repositorysquare-packing

By Couzo

github.com/franciscouzo/square-packingImproved packings for 49 counts from

n = 68

to 307. Exact rational certificates at 204 and 260 (T-223), replayed and reviewed here, supplied earlier house packings; Daniel's regularized views (T-225) have since replaced them. The earlier refinements of issue451 (T-128) and their follow-up (T-130), replayed here, have also been superseded.

20 results (13 at S3, 7 at S2) · 3 records (1 at S3, 2 at S2)

Repositorysquish-certs

By Chaoweeraprasit

github.com/itsnaka/squish-certsExact rational certificates for SQUISH upper-bound packings.

5 results (at S3)

Repositorysquare-packing

By Ostashev

github.com/dostashev/square-packingNew packings of 155, 156, 175, 211, 232 and 264 squares with exact certificates and a GMP checker; all six are replayed here (T-149, T-158).

4 results (at S3)

Repositorysquare-packing-certificates

By PingYou Ltd

github.com/BuddenPing/square-packing-certificatesExact rational packings of 207 and 153 squares built from Xu's packing of 70, both replayed here (T-147, T-148).

9 results (3 at S3, 3 at S2, 3 at S1)

Repositoryn17-square-packing

By Guzhou0806

github.com/Guzhou0806/n17-square-packingStrict lower bounds for seventeen squares.

5 results (3 at S3, 2 at S2) · 1 record (at S2)

Repository17-squares-certified-bound

By Overbeck

github.com/Kleddamag/17-squares-certified-boundCertified lower bounds for seventeen squares.

4 results (3 at S3, 1 at S2) · 1 record (at S2)

Repositoryn40-square-packing

By Guzhou0806

github.com/Guzhou0806/n40-square-packingStrict lower bounds for forty squares, on densities grown from Hosono's.

3 results (at S3) · 1 record (at S3)

Repositorysquare-packing-records

By Polkovskyi

github.com/Mishapolk/square-packing-recordsDecimal packings at 48 counts; exact witnesses derived here prove the printed sides at the 30 within the corpus (T-138).

4 results (2 at S3, 1 at S2, 1 at S1) · 1 record (at S1)

Repositorysquare_packing

By Xu

github.com/ry-xu/square_packingComplete rational packings and an undilated radical

n = 51

construction; finite feasibility is confirmed here (T-125, T-126).

2 results (at S3) · 1 record (at S3)

Repositorysquare_packing_records.json

By Xu

github.com/ry-xu/square_packing/blob/8dc415296f697f5140caea27c7a0193d52deb4e6/square_packing_records.jsonThe complete source report retained for the rational packing comparisons.

2 results (at S3) · 1 record (at S3)

WebsiteAnother Better Lower Bound for

n = 17

Square Packing

By Massaccesi

gus-massa.blogspot.com/2026/08/another-better-lower-bound-for-n17.html

s (17)

≥ 4.5058, by linear programming on Burns’s certificate architecture.

2 results (at S3) · 12 credits (3 at S5, 3 at S4, 6 at S3)

Repositorys12-lower-bound

By Ryu

github.com/squarepacker/s12-lower-boundDaniel's

s (12)

points rescaled and then re-weighted, the lower bound

s (12)

≥ 7943/2000 for twelve squares.

2 results (1 at S3, 1 at S2) · 1 record (at S3)

Repositorysquare-packing

By de Winter

github.com/JoostdeWinter/square-packingExact rational certificates for 227, 229 and 260 squares, replayed and reviewed here (T-196). The house packing at 260 was replaced by T-223 on 21 October; Daniel's regularized views (T-225) now supply the house packings at 227, 229 and 260.

1 result (at S3)

Repositorys95-certificate

By Greff

github.com/bengreff/s95-certificateA mixed cover of points and grid-line segments for

s (95) = 10

, with the run records of both checkers; reported, both checkers replayed in triage (T-191).

1 result (at S3) · 1 record (at S3)

Repositorys76-certificate

By Greff

github.com/bengreff/s76-certificateA mixed cover of points and grid-line segments for

s (76) = 9

, with the run records of both checkers; reported, its census replayed in triage (T-184).

1 result (at S3) · 1 record (at S3)

Repositorysquare-packing-refinements

By Gupta

github.com/SidG2k1/square-packing-refinementsSeventeen rational refinements of Chaoweeraprasit's SQUISH packings, using Daniel's optimizer; fourteen finite upper-bound improvements selected here (T-127) and three withdrawn. Exact feasibility is confirmed with independently re-implemented code; optimality is not established.

1 result (at S3)

WebsiteSQUISH dated source follow-up

By Chaoweeraprasit

#401Dated SQUISH update, including a pinned copy of the original rational n153 certificate.

1 result (at S3)

Repositorysquare-packing-211

By de Winter

github.com/JoostdeWinter/square-packing-211A packing of 211 squares in a square of side under 15.

1 result (at S3)

WebsiteSquares in Squares

By Ellsworth after Friedman

kingbird.myphotos.cc/packing/squares_in_squares.htmlThe catalogue of record packings, with their exact sides and histories: the baseline of every upper bound here.

2 results (at S2)

Repositorymy-repo

By Calle

github.com/riocalle/my-repoA decimal layout of 102 squares, another arrangement of Xu's design; certified here from the layout (T-159).

1 result (at S2)

Repositorysquare-packing-research

By Barnett

github.com/RobertBarnettProjects/square-packing-researchExact rational refinements of Xu's packings of 146 and 261 squares, replayed here (T-150).

1 result (at S2)

Repositorysquare-packing-n70

By Deleeuw

github.com/ebdeleeuw/square-packing-n70An exact rational refinement of Xu's packing of 70 squares (T-137).

1 result (at S2)

Repositorycertified-square-packing-68

By Rehwaldt

github.com/lollipoll/certified-square-packing-68An exact finite rational refinement of Couzo's

n = 68

packing, replayed here (T-118). Its analytic root and dual programs remain outside that replay.

1 result (at S2)

Repositorycouzo-five-exact-certificates

By Rehwaldt

github.com/lollipoll/couzo-five-exact-certificatesRational refinements of Couzo's packings; complete finite certificates at

n = 105

and 292 are replayed here (T-117).

1 result (at S2)

WebsiteZenodo 23038546

By Wang and Li

doi.org/10.5281/zenodo.23038546An exact lower bound for eleven squares, a reweighting of Overbeck’s certificate.

1 result (at S2)

Repositorysquares

By PingYou Ltd

github.com/BuddenPing/squaresPull request #574's tighter certificates of others' packings, recorded at 68 counts and replayed at every one of them here (T-174).

2 results (at S1) · 2 records (at S1)

Website100 Certified Larger-Count Square Packings

By Muglich

#686Exact rational upper-bound certificates for

n = 328

to 998, in an archive attached to the issue.

0 results

Repository11SquaresFormalized

Contributors: ctjlewis, Hosono, Gurevitch, Julian-JJ, Guzhou0806, Ahmed

github.com/Queuingtheorydotcom/11SquaresFormalizedA Lean 4 formalization of that proof, trusting Lean's compiler for its certificates.

0 results

Repository17squares

By ahyangyi

github.com/ahyangyi/17squaresA lower-bound proof for seventeen squares.

0 results

WebsiteErich’s Packing Center

By Friedman

web.archive.org/web/20230530194618/https://erich-friedman.github.io/packing/squinsquThe original Squares in Squares page, as archived on 30 May 2023, which Ellsworth’s catalogue continues.

0 results

Repositoryjoostdewinter.github.io

By de Winter

github.com/JoostdeWinter/joostdewinter.github.ioNineteen exact rational certificates beyond 324 squares, at 464 and from 509 to 1568 below the integer grid (#666); the eleven at or below 1024 are replayed here as dated rows beyond the case corpus.

0 results

WebsiteProposing a Better Lower Bound for