Resources

By Jatloe, Gurevitch, Lewis, Ahmed

github.com/Queuingtheorydotcom/Jatloe12SquaresFormalizedA Lean 4 proof of

s (12) = 4

, trusting Lean's compiler for its certificates.

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

Repositorysq19

By Oscar 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 record (at S5) · 1 result (at S5)

Repositorysq17-lean

By Oscar 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 record (at S5) · 1 result (at S5)

Repositorythe-seventeenth-square-candidate

By Marc Leonard Overbeck

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

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

Repository11SquaresOptimal

By Manasseh Ahmed

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

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

Repository11-squares-certified-bound

By Marc Leonard Overbeck

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

1 result (at S5)

Repositorysquare-packing

By Evan 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.

33 records (4 at S4, 16 at S3, 13 at S2) · 47 results (4 at S4, 24 at S3, 18 at S2, 1 at S1) · 4 credits (2 at S3, 2 at S1)

Repositorysquare-packing

By Hiroaki Hosono

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

31 records (1 at S4, 29 at S3, 1 at S2) · 33 results (1 at S4, 31 at S3, 1 at S2)

Repositorysquarepack-certs

By Kevin 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).

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

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 Hiroaki Hosono

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

27 records (24 at S3, 3 at S2) · 38 results (35 at S3, 3 at S2)

Repositorysquare-packing

By Francisco 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.

5 records (3 at S3, 2 at S2) · 25 results (20 at S3, 5 at S2)

Repositorysquish-certs

By Nate Chaoweeraprasit

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

5 results (at S3)

Repositorysquare-packing

By Daniil 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 Ryan 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.

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

Repository17-squares-certified-bound

By Marc Leonard Overbeck

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

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

Repositoryn40-square-packing

By Guzhou0806

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

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

WebsitearXiv 2609.37410

By Hakan Karakuş

arxiv.org/abs/2609.37410A counterexample to Nagamochi’s scoring lemma, and a strip-measure lower bound for every nonsquare count from eight.

3 records (at S3) · 3 results (at S3)

Repositorysquare-packing-records

By Mykhailo 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).

5 records (1 at S2, 4 at S1) · 8 results (2 at S3, 2 at S2, 4 at S1)

Repositorysquare-packing-archive

By Andrey Vlasenko

github.com/chelokot/square-packing-archiveA counterexample to Nagamochi's scoring lemma, and a Lean proof that s(k^2 - 2) = k.

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

Repositorysquare_packing

By Ryan 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).

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

Repositorysquare_packing_records.json

By Ryan Xu

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

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

WebsiteAnother Better Lower Bound for

n = 17

Square Packing

By Gustavo 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 Sungjoon

github.com/squarepacker/s12-lower-boundEvan Daniel's

s (12)

points rescaled and then re-weighted, the lower bound

s (12)

≥ 7943/2000 for twelve squares.

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

Repositorys44-equals-7

By Mohsen Khalili and Sara Gharabaghi

github.com/moh63-dev/s44-equals-7A closed mixed cover of points and grid-line segments for

s (44) = 7

, with the run records of both of Evan Daniel's checkers; zmx2 replayed here (T-252).

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

Repositorysquare-packing

By Joost 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 Benjamin 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 record (at S3) · 1 result (at S3)

Repositorys76-certificate

By Benjamin 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 record (at S3) · 1 result (at S3)

Repositorysquare-packing-refinements

By Siddharth Gupta

github.com/SidG2k1/square-packing-refinementsSeventeen rational refinements of Nate Chaoweeraprasit's SQUISH packings, using Evan 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 Nate Chaoweeraprasit

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

1 result (at S3)

Repositorysquare-packing-211

By Joost de Winter

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

1 result (at S3)

Repositorysquare-packing-tools

By Hiroaki Hosono

github.com/wand125/square-packing-toolsTools for Tokoharu's rectangle-density solver, and an exact point and threshold-charge row checker.

2 records (at S2) · 2 results (at S2)

WebsiteSquares in Squares

By David Ellsworth after Erich 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)

WebsiteExact Side of the Record Packing at 297

By Hyukdong Kim

#804The degree-21 minimal polynomial of the record side at

n = 297

, with an exact configuration attached.

1 record (at S2) · 1 result (at S2)

WebsiteExact Sides of Five Record Packings

By Hyukdong Kim

#804Minimal polynomials of the record sides at

n = 88

, 126, 172, 199 and 263, found numerically, in an archive attached to the issue.

1 record (at S2) · 1 result (at S2)

Repository78f9f0e7b4669f2f509a281845081768

By Amund Kristiansen

gist.github.com/amundsk/78f9f0e7b4669f2f509a281845081768An exact certificate for 303 squares, another arrangement of Evan Daniel's packing found from it, replayed and reviewed here (T-239).

1 result (at S2)

Repositoryn204.cert

By Mykhailo Polkovskyi

github.com/Mishapolk/square-packing-records/blob/12fc46678fa8eefa3f156ff37dfffd84c8f3a580/certificates/n204.certThe lower of the two 204 certificates issue 719's release published, retained and replayed here, and the record packing at 204 (T-231).

1 result (at S2)

Repositorymy-repo

By Rio Calle

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

1 result (at S2)

Repositorysquare-packing-research

By Robert Barnett

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

1 result (at S2)

Repositorysquare-packing-n70

By Eric Deleeuw

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

1 result (at S2)

Repositorycertified-square-packing-68

By Seth 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 Seth 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 Ke Wang and Can 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 records (at S1) · 2 results (at S1)

Website100 Certified Larger-Count Square Packings

By Darius Muglich

#686Exact rational upper-bound certificates for

n = 328

to 998, in an archive attached to the issue.

0 results

Repository11SquaresFormalized

Contributors: Lewis, Hiroaki Hosono, Benjamin Gurevitch, Julian-JJ, Guzhou0806, Manasseh 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

Repository18ada41ec384b6ff2c96f58b7ce7d1a6

By Amund Kristiansen

gist.github.com/amundsk/18ada41ec384b6ff2c96f58b7ce7d1a6An exact certificate at 344, beyond the corpus, of the 307 record design stretched one step, the author says (#819); the row at the count.

0 results

Repositorye4df936fb09c68446598d4c8309d0166

By Amund Kristiansen

gist.github.com/amundsk/e4df936fb09c68446598d4c8309d0166Exact certificates for fourteen counts from 334 to 504, each, the author says, found from the packing at the count in Francisco Couzo's 964ee2b index (#763); twelve are rows beyond the corpus.

0 results

WebsiteErich’s Packing Center

By Erich 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 Joost 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

Repositorypacking

By E. Summins

github.com/Esummins/packingThe

n = 11

lab's simple-square stratification series, with a replay of Overbeck's eleven-square certificate.

0 results

WebsiteProposing a Better Lower Bound for

n = 17

Square Packing

By Sam Burns

sam-burns.com/posts/proposing-better-lower-bound-for-n17-square-packingA weighted certificate for

s (17)

≥ 4.4811, the method Massaccesi’s bound builds on.

0 results · 14 credits (3 at S5, 3 at S4, 8 at S3)

WebsiteSquare Packing Atlas

By Evan Daniel

evand.github.io/square-packingEvery record packing drawn beside the proven floor beneath it, with a page of open problems.

0 results

Repositorysquare-packing

By Griffin Casson

github.com/griffcass/square-packingImproved packings for

n = 103

, 105 and other cases.

0 results

Repositorysquare-packing-research

By David R. MacIver

github.com/DRMacIver/square-packing-researchA lower bound for seventeen squares, with its paper and a Lean check.

0 results

Repositorysquare17-lower-bound

By anabologyco-maker

github.com/anabologyco-maker/square17-lower-boundA weighted fractional lower bound for seventeen squares.

0 results

Repositorysquarepack-lean

By Kevin Fang

github.com/TheSnakeFang/squarepack-leanA Lean 4 proof of Fang’s Theorem 1, s(n² − n + 1) < n for every n ≥ 15, and of the single-step bounds of his Theorem 2 (T-163); not built here.

0 results

RepositorySquares-packing_S-29-_New-Record

By Thomas Schadt

github.com/BalthasarStrauss/Squares-packing_S-29-_New-RecordA record packing of 29 squares.

0 results

WebsiteSQUISH Packing of 153 Squares

By Nate Chaoweeraprasit

#401The supplemental rational certificate submitted with the SQUISH packings.

0 results

WebsiteUnitSquare

By the UnitSquare Project

hmbelvedere.comResults Release 1, reported packings for six counts from