As published
= corrects Nagamochi 2005open
Proven
- exact
Citation record n-264
lowerKarakuş 2026, arXiv corrects Nagamochi 2005 (confirmed T-083)
upperOstashev et al., GitHub (confirmed T-186)
Open
- optimality
Bounds
16.77473513…
16.77473513238783285- Found by
- Ostashev 2026
- Improved by
- PingYou Ltd, Polkovskyi
- Construction
- —
- Source
- [Mishapolk KKT refinements 2026-10-14]
- Evidence
E-mishapolk-70a033f-certificate-report
16.77473513…
16.77473513238783285The reported value, verified here.
16.30840309…
16.308403094438- 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 = 16 and interval 6 give a(264) = 16.308403094438469074118669059935..., 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
16.25595125…
16.2559512565- Corrects
- Nagamochi 2005 (T-007)
- Evidence
E-karakus-strip-lower,E-karakus-strip-measure-interval
0.51878387…
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-155 V3 C3 Levy after Daniel · 2026-10-12 · 59 cases
Exact regularized sides at 59 counts,
5.4e-20to9.9e-15below the ceilings they replaceT-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
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.444863 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 60 of its 264 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. Also regularized by the Squares Project with Daniel's regularizer (evand/square-packing, MIT), with none of the project's modifications established; whether its solve climbed a retry rung is not recorded. A regularization of T-101's packing solved to its side, not drawn here; its exact side is registered in T-155, and the same side was first certified by Daniel's certificate (T-101), so it proves no new bound. 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 16.77817459305202 from [Kingbird], the case’s ceiling until 12 October 2026; its certificate and replay remain retained.
- Priority: Earlier house 16.7747351323878329 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)
17 evidence entries
E-regularized-bounds-2026-10-12-exact-decision, 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-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
- [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 tighter certificate, after PingYou Ltd’s, of Ostashev’s composition of his 38-square rectangle with a 93-square piece of Daniel’s exact optimum of de Winter’s n = 126 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 93-square piece of Daniel’s exact optimum of de Winter’s n = 126 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 the catalogue’s packing (T-101, T-155), which stays retained as history (the certificate).
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 , a bound Daniel’s exact certificate of this packing already proves at the same side (T-101). The verified upper bound was that side exactly until 12 October 2026, resting on both certificates (T-101, T-155), and the record printed it as . Until then the verified upper bound was exactly , 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 ,
the verified upper bound from 6 to 12 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 12 October 2026 the verified upper bound here was
, exactly, proved by Daniel’s exact certificate
of this packing (E-evand-exact-ceilings-2026-10-05-exact-replay, T-101) and by the
exact regularized certificate of it (E-regularized-bounds-2026-10-12-exact-decision,
T-155), and the record prints it as . As printed 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 exact side. The catalogue gives the packing’s side exactly, as ,
and the certificate’s side lies 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 Ostashev’s certificate (T-158) 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, which wrote its certificate at the side the solver reached, the
solved point scaled by and the side rounded up.
The result is an exact rational packing of the same 264 squares in a square of side
, below the verified upper bound the record
held before, which was that same side rounded up at the printed precision: it is the
side of Daniel’s certificate of this packing (T-101). Measured against the witness
under the box’s eight symmetries, its squares pair one to one with the witness’s; none
moves by more than , and none turns by more than as a sine.
It draws the same picture as the witness, so the atlas drawing does not change.
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 , the verified upper bound
until 12 October 2026. Daniel’s certificate of this packing already proves the same
bound at the same side (T-101), and its replay here, by two checkers that share no code
with each other or with the source, is independent of the code that made this view.
That side was the exact form of the case’s verified_upper_bound until 12 October 2026,
which cited both certificates (T-101, T-155) and printed it as , 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 264 squares, each a rational centre and a
rational , in a square of side ,
above the side the Kingbird catalogue prints, . Rounded to
binary64, square for square, its pose is the one the atlas pictures for this count.
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 , 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 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) |
Daniil Ostashev’s certificate (T-158)
Ostashev’s composition of his 38-square rectangle with a 93-square piece of Daniel’s exact optimum of de Winter’s n = 126 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 264 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 the catalogue’s packing (T-101, T-155), 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 tighter certificate, after PingYou Ltd’s, of Ostashev’s composition of his 38-square rectangle with a 93-square piece of Daniel’s exact optimum of de Winter’s n = 126 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 264 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 , stay verified and are not selected.