Case record
The best packing known for 227 squares, side 15.56362565…, de Winter 2026. Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT)
As published
The packing as published, de Winter 2026 [Daniel regularized lists 2026-10-20]

n=227

= corrects Nagamochi 2005open

15.06880228…≤s(227)≤15.56362565…

15.0615.564
151617
15.06716.067
nn+1

Proven

15.06880≤s(227)≤15.563626

  • exact

Citation record n-227

lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)

upperde Winter et al., GitHub (confirmed T-225)

Open

  • optimality

Bounds

Best known packing

15.56362565…

15.5636256523251491
Found by
de Winter 2026
Improved by
Couzo, Daniel
Construction
—
Source
[Daniel regularized lists 2026-10-20]
Evidence
E-evand-regularized-1020-certificate-report
Verified upper bound

15.56362565…

15.5636256523251491

The reported value, verified here.

Evidence
E-evand-regularized-1020-exact-feasibility, E-evand-regularized-1020-review-exact-feasibility
Reported lower bound

730113+22+1357113

15.17657384178
Proved by
Green 2000
Kind
monotone
Scope
Source-reported only; no verification promotion.
Note
Friedman's DS7 survey, Theorem 9, k=15, reports this bound at n=226; reference [8] is Green's private communication (2000). The source proof has not been recovered. The unavoidable-set argument DS7's Figure 34 illustrates does not prove it: at k=15 that point pattern leaves a unit square empty (devtools.check_green_ds7). Inherited at n=227 by monotonicity.
Source
[Friedman DS7]
Evidence
E-green-ds7-theorem9-reported-lower
Verified lower bound

15.06880228…

15.0688022843
Corrects
Nagamochi 2005 (T-007)
Evidence
E-karakus-strip-lower, E-karakus-strip-measure-interval
Gap

0.49482336…

Verified upper minus verified lower.

Results in the register

  • T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases

    s(n)≥min(⌈n⌉,n−2⌊n⌋+1+1) for 4≤n≤324

  • T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases

    s(n)≥1/2+n−⌊n⌋+1/4 for every nonsquare 8≤n≤324

  • T-085 V3 C3 Karakuş; Vlasenko · 2026-10-02 · 315 cases

    Nagamochi 2005, Lemma 1 is false for every container with a>3 and b>2

  • T-101 V3 C3 Daniel after Couzo, de Winter, Ellsworth, Levy · 2026-10-06 · 77 cases

    Exact certificates of 77 catalogue packings: s(n) ≤ S', 1.2e-16 to 9.8e-15 above each side

  • T-155 V3 C3 Levy after Daniel · 2026-10-12 · 59 cases

    Exact regularized sides at 59 counts, 5.4e-20 to 9.9e-15 below the ceilings they replace

  • T-180 V0 C1 Hosono · 2026-10-14 · 264 cases

    Closed-form lower bound s(N)≥a(N) for every non-square N≥49, reported

  • T-196 V3 C3 de Winter after Levy · 2026-10-18 · n = 227, 229, 260

    de Winter reports three smaller rational upper bounds at 227, 229 and 260

    Claim and records
    Claim
    Three complete rational source certificates report finite upper-bound improvements at the exact sides they state: s(227)≤194547458795865848854407472552117653131825098066089500568310019841668910818842825068644658133972443495777187230686109286929082683273291187074040913251499/12500000000000000000000000000001272204783003459957077568639425038233180795950995922365041743732086145591922059343477256613382050000000000000000000000000; s(229)≤156501747569482131747919637148801852719869637315233948984618327625011520667543259632677498716011131748832131668750692746335433269145213277034738380207139541/10000000000000000000000000000001737366297119815888250696550926607660931327350731575578989919015034082413286101971092035771621296900000000000000000000000000; s(260)≤16645778804181379786535601/1000000000000000000000000.

    The three certificates and their duplicate-square and outside-container controls were decided here on 20 October 2026 by both maintained exact routes, and the frozen comparison rebuilt; no route here is the source's code, so the replay is independently re-implemented. The 20 October review decided all three again on a third exact route of its own, refused sharp controls 1e-30 past contact on both maintained routes, and found no blocking defect.

    Issue 668 reports the three exact rational certificate sides on 17 October; the retained licensed successor changes only LICENSE and the root README. The ledger preserves this report before Couzo issue 672 and Daniel issue 674 at overlapping counts. No arrangement identity, local minimum or optimum is established.
    Significance
    Two case ceilings move, by 7.27e-03 at 227 and 1.11e-02 at 260, the first improvement at 260 below 11 + 4*sqrt(2), in a construction family that Couzo and Daniel improved further within three days; no lower bound or optimum.
    Novelty
    previously-published Present in an identified source
    Records

    n = 227n = 229n = 260registerevidence 1evidence 2

  • T-225 V3 C3 Daniel after Couzo, de Winter, Polkovskyi, Levy · 2026-10-21 · n = 204, 227, 229, 260

    Daniel's solved, regularized views at 204, 227, 229 and 260, each the smallest side reported there

    Claim and records
    Claim
    Four complete rational source certificates report finite upper-bound improvements at the exact sides they state: s(204)≤14.808642840591493923068442871459, s(227)≤15.563625652325149084792443723702, s(229)≤15.650161513876431064009548865321 and s(260)≤16.645753250519812194746296653316.

    The four certificates and their duplicate-square and outside-container controls were decided here on 21 October 2026 by both maintained exact routes, and the frozen comparison rebuilt; no route here is the source's code, so the replay is independently re-implemented. The 21 October review reproduced it, decided each certificate again on a clean-room checker of its own, and found no blocking defect.

    Each certificate is a display-regularized view, in Daniel's regularized record lists, of a packing already reported, solved to its exact side, and lies below that packing's certificate: by 1.39e-9 at 204 and 2.51e-11 at 260 below Couzo's #678 certificates (T-223), by 1.76e-11 at 227 below Couzo's #672 certificate (T-227), and by 1.91e-11 at 229 below Daniel's #674 update (T-199). Each side lies below the verified upper bound at the next count, so each bound is new.

    Each certificate's JSON reports it VALID under the source's checkers and verified at 80 digits, prints S_cert, the side its certificate's header states, and S_exact, the 50-digit side of the solved packing it rounds up, and classes the view at level 2, same packing traversable without expansion, by a path test that samples angle moves and that the method log says is not a continuous proof. The commit says the six refreshed counts were certified and regularized, and of 229 that the polished side is 2e-11 below the posted one, the exact optimum of the same packing; each JSON says it is not a new bound. The checkers are byte-identical to the copies the n183 packet retains. Those statements are the author's; no source program ran here.

    Credit the packings to their finders (at 227 the source's list names Couzo, whose #672 refines de Winter's packing): Couzo's at 204 (#678, T-223, which his source credits to Polkovskyi's construction) and 260 (#678, T-223, his arrangement from a search seeded with Daniel's exact-form certificate of de Winter's #668 packing); de Winter's at 227 (#668, T-196) as refined in Couzo's #672 report (T-227; who made the refinement the source does not say); and Daniel's own at 229 (#674, T-199, from Couzo's #672 packing, which refines de Winter's).

    Daniel (https://github.com/evand/square-packing) refreshed each packing from his store, solved it to the exact side stated (at 229 after a polish), regularized it for display at that side and wrote the certificate. His credits say the repository's work was produced by Claude (Anthropic) under human direction.
    Significance
    Smaller finite construction sides at 204, 227, 229 and 260, each the solved exact side of a packing already reported (Couzo's #678 at 204 and 260 and his #672 at 227, Daniel's #674 at 229), 1.76e-11 to 1.39e-9 below that packing's certificate and regularized for display: a citable detail of each case that moves no theorem, S2 as T-146 is. At 227 the drop of 1.71e-4 below T-196 is #672's (T-227), not this entry's. No lower bound or optimum. Drafted at intake, confirmed by review A of #716 and by the 21 October stage 4 review.
    Novelty
    previously-published Present in an identified source
    Records

    n = 204n = 227n = 229n = 260registerevidence 1evidence 2evidence 3

  • T-227 V0 C0 Couzo after de Winter, Daniel, Levy · 2026-10-22 · n = 227, 229

    Couzo's refinements of de Winter's 227 and 229, below T-196 at both

    Claim and records
    Claim
    Two complete rational source certificates report finite upper-bound improvements at the exact sides they state: s(227)≤71427829379429597600111901507/4589408083628500000000000000 and s(229)≤231170315041711399213831561/14771101209934000000000000. Complete native feasibility outcomes are retained separately; the entry awaits independent review. At 227 it is below de Winter's T-196, the house best packing when it was reported; Daniel's solved view of this packing (T-225), smaller still, has been the house since 22 October 2026. At 229 Daniel's #674 opening and update (T-198, T-199), reported after it, are smaller.

    The issue states that each bound is strictly smaller than the source's previous published index and a reviewed comparison envelope including deletion and repeated L borders, and the manifest records the author's checker receipts with the source's exact checker verify_bound_certificate.py (Daniel's MIT verifier, modified by Couzo with Codex), pinned here by digest and not run. Those statements are the author's; no source program ran here.

    Credit Couzo (https://github.com/franciscouzo/square-packing) with refinements of de Winter's #668 packings (T-196), as the author's comment of 17 October says: at 227 a CT105 web submission (method fq) seeded from de Winter's #668 certificate by way of Daniel's exact form of it, which the source does not say who made, and at 229 an slp refinement (search job 106640) of de Winter's #668 certificate.
    Significance
    Refinements of de Winter's 227 and 229 packings (T-196), the same arrangement solved lower by 1.71e-4 at 227 and 1.67e-8 at 229: a citable step that moves no theorem, S2 as T-199 (a same-arrangement step of 1.32e-5) and T-225, whose rationale already gives the 1.71e-4 at 227 to this report. No lower bound or optimum.
    Novelty
    previously-published Present in an identified source
    Records

    n = 227n = 229registerevidence 1

Verification

upper: replayed here; lower: external proof (read here), audited here

formal lower differs from report; reported lower: defect recorded

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 48 of the retained witness (witness id 49) translates 0.002631 along (0.830244, -0.5574) with the packing still valid, so the configuration admits a non-trivial feasible motion; 9 of its 227 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.

Regularized drawing

Regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT), with the project's modifications: same-side exact re-solve (devtools.regularize_same_side). A drawing of T-225's packing at the witness's own side: a pure regularization, which proves no new bound, so not a result. Also regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT), with the project's modifications: same-side exact re-solve (devtools.regularize_same_side); whether its solve climbed a retry rung is not recorded. A regularization of T-101's packing at the witness's own side, not drawn here; its exact side is registered as T-155, the upper bound it proves. The house is itself its source's regularization of T-227's packing (Daniel after Couzo, de Winter, Polkovskyi, Levy), registered as T-225 for the upper bound its exact side proves.

Open questions
  • Blocker (source evidence): Green's reported lower-bound proof, cited as private communication by Friedman, has not been recovered or independently replayed. E-green-ds7-theorem9-reported-lower
  • Priority: Earlier house 19463834764831844055010554526310613/1250000000000000000000000000000000 from T-155 (reported as 15.57106781186547 from [Kingbird]), the case’s ceiling until 20 October 2026; its certificate and replay remain retained. (Ellsworth)
  • Priority: Earlier house 15.5637967036692680 from [de Winter upper bounds 2026-10-17], the case’s ceiling from 20 October 2026 until 22 October 2026; its certificate and replay remain retained. (de Winter)

s(227) — open

House adoption, 22 October 2026. Daniel’s display regularization of de Winter’s packing as refined in Couzo’s #672 report (T-225) is now this case’s house: its exact certificate proves s(227)≤15.5636256523251491, the reported and the verified upper bound, rounded outward from its exact side. The exact certificate side improves the previous verified exact side by about 1.71×10−4. The earlier ceiling, displayed outward as 15.5637967036692680 from de Winter’s packing (T-196), applied until this adoption and stays retained as history (the certificate).

House adoption, 20 October 2026. de Winter’s packing (T-196) was this case’s house until 22 October 2026: its exact certificate proves s(227)≤15.5637967036692680, the reported and the verified upper bound, rounded outward from its exact side. The exact certificate side improves the previous verified exact side by about 7.27×10−3. The earlier exact ceiling, 19463834764831844055010554526310613/1250000000000000000000000000000000 from Ellsworth’s packing (T-155), applied until this adoption and stays retained as history; the reported upper bound it replaces, 15.57106781186547 from [Kingbird], lies 7.27×10−3 above the new side (the certificate).

Reported certificate, 2026-10-17. de Winter reported a 227-square certificate at container side 15.563796703670, rounded upward from the retained exact certificate. The exact rational side is registered in the result register. Its V0/C0 registration left both case upper lanes, the house witness and its drawing unchanged until the house adoption of 20 October 2026, and until then the rigidity and arrangement notes below described that retained house. On 20 October 2026 both of this project’s maintained exact routes decided the certificate and refused its two controls, which raised T-196 to V3/C3, independently re-implemented: no route is the source’s code. Couzo’s later #672 reported a smaller side here.

Exact regularized certificate, 2026-10-12. This project’s regularization pass, Daniel’s exact solver and regularizer run here on this register’s witness, produced an exact rational packing of this arrangement, decided here over ℚ by two exact checkers: it proves s(227)≤15.5710678118654752440084436210484904, the verified upper bound until 20 October 2026 (T-155), which the record printed as 15.57106781186548. Until then the verified upper bound was exactly 15.57106781186548, the side of Daniel’s exact certificate of this packing rounded up at the printed precision (T-101).

Exact certificate, 2026-10-06. Daniel’s square-packing published on 5 October 2026 an exact rational certificate of this packing, decided here over ℚ by two exact checkers that share no code with each other or with the source, and by the source’s own two run here: it proves s(227)≤15.57106781186548, the verified upper bound from 6 to 12 October 2026 (T-101). Until then the verified upper bound was the trivial grid bound 16.

Open. Previously, the best known packing gave s(227)≤15.57106782, and the strongest lower bound independently verified here is 15.068802 from Karakuş’s general theorem, leaving a gap of 0.5023. General bound: s(N)≥1/2+N−⌊N⌋+1/4.

The earlier verified ceiling

Until 20 October 2026 the verified upper bound here was 15.5710678118654752440084436210484904, exactly, proved by the exact regularized certificate of this packing (E-regularized-bounds-2026-10-12-exact-decision, T-155), and the record prints it as 15.57106781186548. As printed it was larger than the catalogue’s printed side 15.57106781186547, then the best known, by 1×10−14.

It was not the value of s(227) and not a different packing: it is the certificate’s own exact side. The catalogue gives the packing’s side exactly, as (17/2)+52, and the certificate’s side lies 7.2×10−36 above that, so it bounds the exact side from above and does not reach it. That side is irrational, so no rational certificate reaches it. A mathematics blocker in the frontmatter recorded the difference until de Winter’s certificate (T-196) replaced both lanes.

The regularized exact certificate

This project’s regularization pass of 11 and 12 October 2026 ran Daniel’s exact solver and regularizer (evand/square-packing, MIT, vendored here) on this register’s witness for this count, with the conservative angle policy and coincide placement, and this project’s same-side re-solve then fixed the result’s tight contacts over ℚ at the witness’s own side. The result is an exact rational packing of the same 227 squares in a square of side 15.5710678118654752440084436210484904, 4.8×10−15 below the verified upper bound the record held before, and 1.6×10−19 below the side of Daniel’s certificate of this packing (T-101): it is the witness’s own side. Measured against the witness under the box’s eight symmetries, its squares pair one to one with the witness’s; 1 moves by more than 1×10−3, the largest by 2.9×10−1, and none turns by more than 1×10−6 as a sine. It redraws the packing visibly, and is drawn only once the regularized layer admits it under the regularization policy.

Each pair and each wall is decided over ℚ twice, by sqpack’s exact separating-axis test and by an independent checker that shares no code with it, and both accept it; both refuse it with its tightest pair pushed into overlap and with its box shrunk past its least clearance (certificate). The same two checkers accepted it in the run that made it, so this is a reproduction with the producer’s code. That proves s(227)≤15.5710678118654752440084436210484904, the verified upper bound until 20 October 2026 (T-155), then the exact form of the case’s verified_upper_bound, which printed it as 15.57106781186548, the decimal it printed before and an upper display of it. It says nothing about optimality, and the packing stays its finders’.

The earlier exact certificate

Daniel’s square-packing published on 5 October 2026 exact rational certificates of the packings this register lists as best known, solved from its own witnesses, and offered those that do not lower a printed side as a replay of the existing bounds, asking for nothing to be registered from them. The certificate for this count holds the same 227 squares, each a rational centre and a rational t=tan(θ/2), in a square of side 15.5710678118654752442…, 5.2×10−15 above the side the Kingbird catalogue prints, 15.57106781186547. Square for square, its pose lies within 1.5×10−4 of the binary64 pose the atlas pictures for this count. 3 squares move by more than 1×10−8, all of them squares the source lists as carrying no force; every other square’s centre rounds to the witness’s. Daniel’s solver moves the binary64 pose to a nearby exact KKT point of the problem of minimizing the side under non-overlap, computed at 80 digits, and rounds it outward to rationals.

This repository decides the certificate exactly. Converted without rounding, every pair and every wall is decided over ℚ twice, by sqpack’s exact separating-axis test and by an independent checker that shares no code with it, and the source’s own two checkers, run here as retained, accept it as well (receipts). That proves s(227)≤15.57106781186548, the verified upper bound until 12 October 2026: the certificate’s side rounded up at the fourteen decimals the catalogue prints, as the record writes any certificate of a printed side. It says nothing about optimality. On jlevy/squares#375 its author wrote that the solver, its checkers and the batch “were written with Claude (Anthropic) as a coding and research agent, directed and reviewed by me.”

The packing

Found by Ellsworth in 2025, via an unrecorded method.

The lower bound

The strongest lower bound independently verified in this record is Karakuş’s general bound, which applies to every nonsquare N≥8:

s(N)≥12+N−⌊N⌋+14

Correction, 2 October 2026. Until that date the verified lower bound here was Nagamochi’s general closed form, s(N)≥min(⌈N⌉,N−2⌊N⌋+1+1), which is stronger at this n and is now recorded as a reported bound. Its published proof rests on Nagamochi’s Lemma 1, which Karakuş showed false; nothing is disproved, and no packing beating it is known (review of 2 October 2026). This register had recorded that proof as verified, its own error, logged as defect D-516.

Source-reported bounds are recorded separately from this independently verified theorem.

The reported lower-bound expression for s(227) is 730/113+22+1357/113 (approximately 15.17657384178). Friedman’s DS7 survey, Theorem 9, k=15, reports this bound at n=226; reference [8] is Green’s private communication (2000). The source proof has not been recovered. The unavoidable-set argument DS7’s Figure 34 illustrates does not prove it: at k=15 that point pattern leaves a unit square empty (devtools.check_green_ds7). Inherited at n=227 by monotonicity. This is a source-reported lower bound; it does not replace the verified bound above. The exact specialization and comparison are retained by audit_ds7_lower_bounds.

Verification Code

The programs behind this case’s verified bounds, by their evidence. The code column says how the code that ran stands to the code its producer used. VERIFIERS.md says what each program is and whose it is.

bound evidence run code programs
verified lower E-karakus-strip-lower a published proof no code no verification code
verified lower E-karakus-strip-measure-interval audited here independent V-check-karakus-strip-measure (first-party)
verified upper E-evand-regularized-1020-exact-feasibility replayed here independent V-sqpack-verify, V-check-rational-witness-independent (first-party); V-evand-arrangement-receipts, V-upper-bound-reports, V-evand-exact-certificates (first-party, premises)
verified upper E-evand-regularized-1020-review-exact-feasibility replayed here independent V-evand-regularized-1020-review-check (first-party); V-evand-regularized-1020-review-controls (first-party, premises)

Joost de Winter’s certificate (T-196)

de Winter’s packing, reported on jlevy/squares#668, at an exact rational side, displayed upward as 15.5637967036692680 (T-196). The certificate gives a rational side and, for each of the 227 unit squares, a rational centre and the cosine and sine of its rotation; the retained packet holds it with the complete native jobs that decided it.

Both maintained exact routes decided it here, sqpack’s exact separating-axis verifier and the independent rational corner checker, with its duplicate-square and outside-container controls, and a third exact route, half-extent containment and exact intersection area, decided it again. No route here is the source’s code, so the replay is independently re-implemented. The review of 20 October 2026 accepted the replay for finite feasibility. That proves s(227)≤15.5637967036692680, the verified upper bound until 22 October 2026: confirmed, independently re-implemented. It says nothing about optimality, rigidity or a local minimum.

The issue says the search, numerical optimization, rational certificates, checkers and figures were made with OpenAI Codex agents under de Winter’s direction, and that Claude (Anthropic) replayed the checkers and prepared the repository for publication.

The issue says the search started from this repository’s catalogue, whose credits for the former packings apply, and built asymmetric Young-corner fills around slipped tilted ribbons, then restored the supports and angles; the three counts are one construction family, and the 229-square packing descends from the 260-square one. None of this lineage is measured here (T-196).

The house it replaces, 19463834764831844055010554526310613/1250000000000000000000000000000000 from Ellsworth’s packing (T-155), stays retained with its own replay as history.

Evan Daniel’s certificate (T-225)

Daniel’s display regularization of de Winter’s packing as refined in Couzo’s #672 report, published in his regularized record lists, on no issue, at exact side 7781812826162574542396221861851/500000000000000000000000000000, displayed upward as 15.5636256523251491 (T-225). The certificate gives a rational side and, for each of the 227 unit squares, a rational centre and the tangent of its half-angle; the retained packet holds it with the complete native jobs that decided it.

Both maintained exact routes decided it here, sqpack’s exact separating-axis verifier and the independent rational corner checker, with its duplicate-square and outside-container controls, and the 21 October review’s clean-room checker decided it again on two routes of its own, in integers alone and in rationals with exact intersection area on the pairs whose boxes overlap; its sharp controls at 10−30 found both maintained routes exact at the far wall, the near wall and the least-gap pair. No route here is the source’s code, so the replay is independently re-implemented. The review of 21 October 2026 accepted the replay for finite feasibility. That proves s(227)≤15.5636256523251491, the verified upper bound: confirmed, independently re-implemented. It says nothing about optimality, rigidity or a local minimum.

The certificate regularizes for display the packing T-227 records, at the side the source reports as that packing’s exact optimum, so the packing stays with its finder and Daniel is credited with the regularization and the certificate. That the two are one packing is the source’s claim, measured here and not decided (T-225’s regularizations).

The source’s credits say the repository’s work was produced by Claude (Anthropic) under human direction, and the commit that publishes the certificate names Claude Opus 5.5 as co-author and says Daniel approved it.

The source names Couzo’s #672 packing (T-227), the refinement of de Winter’s #668 packing (T-196) that #672 reports, as the one it regularizes and calls the certificate not a new bound: Daniel solved that packing to its exact side, 1.76×10−11 below #672’s certificate, and regularized it for display at that side. Measured by the import and again by the 21 October review, nearest centres pair the two one to one under a half turn; 194 of the 227 squares lie within 10−6 of T-227’s, 16 move beyond 10−3 and 3 beyond a tenth, at most 0.168, and one square turns by 2.54° (T-225). #672’s packing moves no square beyond a tenth from de Winter’s (T-227).

The house it replaces, 15.5637967036692680 from de Winter’s packing (T-196), stays retained with its own replay as history.