As published
= corrects Nagamochi 2005open
Proven
- exact
Citation record n-232
lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)
upperOstashev et al., GitHub (confirmed T-186)
Open
- optimality
Bounds
15.76417431…
15.76417431748659663- Found by
- Ostashev 2026
- Improved by
- PingYou Ltd, Polkovskyi
- Construction
- —
- Source
- [Mishapolk KKT refinements 2026-10-14]
- Evidence
E-mishapolk-70a033f-certificate-report
15.76417431…
15.76417431748659663The reported value, verified here.
15.29310997…
15.293109978103- Proved by
- Hosono 2026
- Kind
- counting
- Scope
- Unrestricted unit-square packing with independent rotations and disjoint interiors.
- Note
- Hosono's closed form (wand125, 13 October 2026, T-180): >= a(N) for every non-square N >= 49, from a measure of line segments on 34 intervals of the fractional part. At , k = 15 and interval 6 give a(232) = 15.293109978103125446064557336514..., here rounded down at 12 and 30 places. The source replayed its certificate with its own checker; no replay has run here.
- Source
- [wand125 closed form 2026-10-14]
- Evidence
E-wand125-closed-form-report
15.23940297…
15.2394029729- Corrects
- Nagamochi 2005 (T-007)
- Evidence
E-karakus-strip-lower,E-karakus-strip-measure-interval
0.52477134…
Verified upper minus verified lower.
Results in the register
T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
for
T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
for every nonsquare
T-085 V3 C3 Karakuş; Vlasenko · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with and
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-16to9.8e-15above each sideT-136 V3 C3 Chaoweeraprasit after Couzo, Xu, Göbel, Schadt, Ellsworth, Hajba, Levy · 2026-10-10 · 17 cases
Seventeen exact rational packings from SQUISH's third request
T-158 V3 C3 Ostashev after Nakajima, Ellsworth, Schadt, Friedman, de Winter, Daniel, Levy, Xu · 2026-10-12 · n = 175, 232, 264
New packings of 175, 232 and 264 squares built on a new 38-square rectangle, each certified exactly
Claim and records
- Claim
- Three complete rational source certificates by Ostashev, reported on jlevy/squares#528, prove finite upper bounds at the exact sides they state: , and .
Each certificate gives a rational side and, for each unit square, a rational centre and the tangent of its half-angle, in the source's sqcert format: the 60-digit optimum of its packing with the load-bearing squares scaled by 1 + 1e-20, then every centre and the side dilated by 1 + 1e-60. Each side rounds up at 38 places to the side the issue prints and at 15 to the README's.
The author reports that each packing passes his own C++ checker in GMP rational arithmetic, on the shipped certificates with no dilation and no tolerance and on certificates rebuilt from the 60-digit decimal packings, and an 80-digit mpmath cross-check written separately, all three written with AI assistance; he also states that each side is the exact first-order optimum of its packing's contact topology, with nonnegative KKT multipliers at a 60-digit solution. Those statements are the author's; no source program ran here.
All nine retained jobs, the three positives with their duplicate-square and outside-container controls, were decided again here on 12 October 2026 by both maintained exact routes and equal their retained rows. A third exact route, half-extent containment and exact intersection area, decided the three with six controls each and held each retained file to its upstream bytes fetched at the pin. No route here is the source's code, and the source ran none of them, so the replay is independently re-implemented. The 12 October review found no blocking defect.
Each side was below the ceiling its case held, by 2.95e-03 at 175 (Couzo's refinement of Xu's packing, T-140), 3.25e-03 at 232 (SQUISH's third request, T-136) and 3.44e-03 at 264 (the catalogue's 9 + 11 sqrt(2)/2, Goebel's pattern, verified by Daniel's exact ceiling, T-101, and at its exact side by T-155's regularized certificate of the same packing); at 175 it is also 2.94e-03 below Couzo's certificate of 11 October, which the issue names as the previous best and which the record holds in the issue-506 packet and registers as T-185, and 4.72e-03 below Xu's T-125. At all three counts it is the smallest exact side the record holds.
On 12 October 2026 the case records adopted this entry as the house at all three counts, each case's reported and verified upper bounds moving together and each earlier house kept as history, with T-140, T-130, T-138 and T-125 verified and not selected at 175; private-worker custody was closed in the same change (packing/devtools/house-custody-2026-10-11.json).
Credit Ostashev (https://github.com/dostashev/square-packing) with the three packings and their certificates. The issue says each is a composition: two library rectangles in opposite corners of the box with aligned squares around them, each using his new packing of 38 unit squares in an (h + 2) x h rectangle, h = 5.7641743..., found by a GPU soft-to-rigid search after Nakajima's idea; at 175 in place of the pieces of Ellsworth's template, cut from Schadt's ; at 232 beside a 76-square piece of Friedman's ; at 264 beside a 93-square piece of Daniel's exact optimum of de Winter's ; each then taken to the exact optimum of its contact topology. He asks that the pieces' sources be acknowledged as the record sees fit.
Measured pose by pose, none of the three is a placement of the packing its case holds or of any report pending at its count: no symmetry of the box pairs the 175 square for square with T-140, with Couzo's certificate of 11 October or with T-125, the 232 with T-136, or the 264 with T-101's certificate. Where the record retains a named piece exactly, it reappears: 66 of the 171 squares of Daniel's certificate of Ellsworth's (T-101) land on squares of the 175 to the ninth decimal under a half turn, none turned, and 88 of the 126 of his exact optimum of de Winter's (T-098) on squares of the 264. Friedman's and the 38-square block are the author's statement, not measured.
The issue states AI assistance: the author set up an AI-assisted research loop and drove it with his own ideas, the rectangle library and composition being his; AI agents wrote and ran the search, composition and verification code. - Significance
- Three new packings, measured as no placement of the packings their cases hold or have pending, smaller finite construction sides at , 232 and 264, 2.95e-03 to 3.44e-03 below the case ceilings and the smallest known at all three; no lower bound or optimum.
- Novelty
- previously-published Present in an identified source
- Records
T-174 V3 C3 PingYou Ltd after Friedman, Ellsworth, Daniel, Xu, Barnett, Couzo, Ostashev, Chaoweeraprasit, Gupta, Fang, Polkovskyi, Levy · 2026-10-14 · 68 cases
Tighter certificates at 68 counts from PingYou Ltd, of others' packings and its own
T-180 V0 C1 Hosono · 2026-10-14 · 264 cases
Closed-form lower bound for every non-square , reported
T-186 V3 C3 Polkovskyi after Ostashev, Couzo, PingYou Ltd, Levy · 2026-10-15 · 12 cases
Exact certificates at twelve counts from Polkovskyi, tightening the smallest reported there
T-193 V3 C3 Daniel after Xu, Chaoweeraprasit, Ostashev, Couzo, PingYou Ltd, Gupta, Polkovskyi, Levy · 2026-10-16 · 16 cases
Exact algebraic sides at sixteen counts from Daniel, of packings the record credits
upper: replayed here; lower: external proof (read here), audited here
formal lower differs from report
not rigid, numerically checked, numerical multiprecision
Evidence: E-translation-escape-not-rigid
Scope
Square 1 of the retained witness (witness id 2) translates 0.008488 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 120 of its 232 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 by the Squares Project with Daniel's regularizer (evand/square-packing, MIT), with the project's modifications: port of his coincidence placement (regularize_grid_slack/1) rather than his code, same-side exact re-solve (devtools.regularize_same_side). A drawing of T-186's packing at the witness's own side: a pure regularization, which proves no new bound, so not a result. The house is itself its source's regularization of T-174's packing (Polkovskyi after Ostashev, Couzo, PingYou Ltd, Levy), registered as T-186 for the upper bound its exact side proves.
- Priority: Earlier house 15.77817459305202 from [Kingbird], the case’s ceiling until 11 October 2026; its certificate and replay remain retained.
- Priority: Earlier house 15.7674283499418417 from [SQUISH third request 2026-10-09], the case’s ceiling from 11 October 2026 until 12 October 2026; its certificate and replay remain retained. (Chaoweeraprasit (itsnaka))
- Priority: Earlier house 15.7641743174865967 from [Ostashev records 2026-10-12], the case’s ceiling from 12 October 2026 until 16 October 2026; its certificate and replay remain retained. (Ostashev)
18 evidence entries
E-evand-exact-ceilings-2026-10-05-report, E-evand-exact-ceilings-2026-10-05-exact-replay, E-evand-exact-ceilings-2026-10-05-source-replay, E-kingbird-upper-register, E-nagamochi-lower, E-basic-grid-upper, E-karakus-strip-lower, E-karakus-strip-measure-interval, E-nagamochi-lemma1-counterexample, E-squish-481-certificate-report, E-squish-481-exact-feasibility, E-pingyou-574-certificate-report, E-pingyou-574-exact-feasibility, E-ostashev-528-certificate-report, E-ostashev-528-exact-feasibility, E-wand125-closed-form-report, E-mishapolk-70a033f-certificate-report, E-mishapolk-70a033f-exact-feasibility
- [evand exact optima 2026-10-05] formal certificate
- [Kingbird] record catalogue
- [Nagamochi 2005] lower bound proof
- [Friedman DS7] survey
- [Karakuş 2026] lower bound proof
- [SQUISH third request 2026-10-09] upper bound report
- [Ostashev records 2026-10-12] upper bound report
- [wand125 closed form 2026-10-14] lower bound proof
- [Mishapolk KKT refinements 2026-10-14] upper bound report
— open
Hosono’s closed form, 14 October 2026. Hosono’s closed form (wand125, 13 October 2026, T-180) states for every non-square , from a measure of line segments on 34 intervals of the fractional part. At , and interval 6 give , so the reported lower bound here is now , rounded down, above Nagamochi’s closed form, . The source replayed its certificate with its own checker; no record of it has been replayed here, so the verified lower bound is unchanged. The source states that its search, certificates, checkers and text were produced with AI assistance (Claude and Codex), under the direction of and reviewed by Hosono.
House adoption, 16 October 2026. Polkovskyi’s refinement, after PingYou Ltd’s, of Ostashev’s composition of his 38-square rectangle with a 76-square piece of Friedman’s n = 85 packing (T-186) is now this case’s house: its exact certificate proves , 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 . The earlier ceiling, displayed outward as from Ostashev’s packing (T-158), applied until this adoption and stays retained as history (the certificate).
House adoption, 12 October 2026. Ostashev’s composition of his 38-square rectangle with a 76-square piece of Friedman’s n = 85 packing (T-158) was this case’s house until 16 October 2026: its exact certificate proves , the reported and the verified upper bound, below the ceiling the case held until then, from Chaoweeraprasit’s packing (T-136), which stays retained as history (the certificate).
House adoption, 11 October 2026. Chaoweeraprasit’s SQUISH packing (T-136) was this case’s house until 12 October 2026: its exact certificate proves , the reported and the verified upper bound, below the ceiling the case held until then, from the catalogue’s packing (T-101), which stays retained as history (the certificate).
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 proved ,
the verified upper bound until 11 October 2026 (T-101). Until then the verified upper
bound was the trivial grid bound .
Open. Previously, the best known packing gave , and the strongest lower bound independently verified here is from Karakuş’s general theorem, leaving a gap of . General bound: .
The earlier verified ceiling
Until 11 October 2026 the verified upper bound here was , proved by
Daniel’s exact rational certificate of this packing
(E-evand-exact-ceilings-2026-10-05-exact-replay, T-101). It was larger than the
catalogue’s printed side , then the best known, by .
It was not the value of and not a different packing: it is the certificate’s
own side, , rounded up at the fourteen decimals the
catalogue prints.
The catalogue gives the packing’s side exactly, as ,
and the certificate’s side lies above that: its squares are rational and each
is kept clear of its neighbours and the walls, 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 Chaoweeraprasit’s certificate (T-136) replaced both lanes.
The 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 232 squares, each a rational centre and a
rational , in a square of side ,
above the side the Kingbird catalogue prints, . Square for
square, its pose lies within of the binary64 pose the atlas pictures for this
count. 4 squares move by more than , all of them squares the source lists as
carrying no force; every other square moves by at most . 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 proved , the verified upper bound until 11 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 an unrecorded author, via a hand construction.
The lower bound
The strongest lower bound independently verified in this record is Karakuş’s general bound, which applies to every nonsquare :
Correction, 2 October 2026. Until that date the verified lower bound here was Nagamochi’s general closed form, , which is stronger at this 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.
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-mishapolk-70a033f-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) |
Nate Chaoweeraprasit’s certificate (T-136)
Chaoweeraprasit’s SQUISH packing, reported on jlevy/squares#481, at an exact rational side, displayed upward as (T-136). The certificate gives a rational side and, for each of the 232 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 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 10 October 2026
and the
final review of 11 October 2026
accepted the replay for finite feasibility.
That proves , the verified upper bound until 12 October
2026: confirmed, independently re-implemented.
It says nothing about optimality, rigidity or a local minimum.
The source states that SQUISH’s solver, its verification and the issue were written with Claude Opus 5.5 under the author’s direction.
The house it replaces, from the catalogue’s packing (T-101), stays retained with its own replay as history.
Daniil Ostashev’s certificate (T-158)
Ostashev’s composition of his 38-square rectangle with a 76-square piece of Friedman’s n = 85 packing, reported on jlevy/squares#528, at an exact rational side, displayed upward as (T-158). The certificate gives a rational side and, for each of the 232 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 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 12 October 2026
accepted the replay for finite feasibility.
That proves , the verified upper bound until 16 October
2026: confirmed, independently re-implemented.
It says nothing about optimality, rigidity or a local minimum.
The issue says the author set up an AI-assisted research loop and drove it with his own ideas, the rectangle library and the composition being his, and that AI agents wrote and ran the search, composition and verification code.
The house it replaces, from Chaoweeraprasit’s packing (T-136), stays retained with its own replay as history. T-174 at , below this house, is confirmed here and accepted by the review of 14 October 2026. From 15 October 2026 until the owner’s house rule of 16 October 2026 lifted the hold, PR #574’s houses were held for the owner, since their witnesses would add about 18.5 MB to a checkout and their custody inputs about 5.8 MB to every worker’s snapshot.
Mykhailo Polkovskyi’s certificate (T-186)
Polkovskyi’s refinement, after PingYou Ltd’s, of Ostashev’s composition of his 38-square rectangle with a 76-square piece of Friedman’s n = 85 packing, reported in his repository on 14 October 2026, with no issue, at an exact rational side, displayed upward as (T-186). The certificate gives a rational side and, for each of the 232 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 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 16 October 2026
accepted the replay for finite feasibility.
That proves , the verified upper bound: confirmed,
independently re-implemented.
It says nothing about optimality, rigidity or a local minimum.
The certificate is Polkovskyi’s tightening of the packing T-174 records, measured here pose by pose as that packing (T-186’s regularizations), so the packing keeps its finder’s credit and Polkovskyi is credited with the certificate.
The commit makes no statement about AI assistance; the author’s issue 593 discloses Gemini assistance with solver scripting, precision checks and formatting.
The house it replaces, from Ostashev’s packing (T-158), stays retained with its own replay as history. The other certificates confirmed here at this count, T-174 at and T-136 at , stay verified and are not selected. T-193’s exact algebraic side at this count, a root of a degree-7 integer polynomial below this house, is confirmed here and accepted by the review of 16 October 2026. The owner’s house rule of 16 October 2026 adopts it: the case keeps this house until its adoption, staged under think-ot5c, moves it to T-193’s side, once the writer takes an algebraic side.