\(s (51)\)$s(51)$ — open

Exact certificate, 2026-10-06. Evan Daniel’s square-packing published on 5 October 2026 an exact rational certificate of this packing, decided here over \(\mathbb{Q}\)$\mathbb{Q}$ 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(51) \le 7.70079923541702\)$s(51)\le 7.70079923541702$, the verified upper bound (T-101). Until then the verified upper bound was the trivial grid bound \(8\)$8$.

Verified lower bound, 2026-10-06. sqverify-fast, this repository’s clean-room measure verifier, decided wand125’s mixed_n51_L747 (T-090) here at all 201 net directions of the retained candidate, with two mutants scaled below coverage one refused (E-n051-wand125-mixed-747-sqverify-fast-replay, V3/C3), so \(s(51) \ge 747/100 = 7.47\)$s(51)\ge 747/100=7.47$ is the verified lower bound, above by \(0.0275\)$0.0275$ the \(2977/400\)$2977/400$ that T-070’s replay of rect_n51_L74425 had made it earlier that day, which had replaced the \(37/5\)$37/5$ carried from \(n = 50\)$n=50$. It shares no code with the source’s checker, so it decides coverage a second way with the same method; the source’s own checker was not run here.

External intake, 2026-10-02. wand125’s rectangle-density source reports the rectangle certificate rect_n51_L74425 at side \(2977/400 = 7.4425\)$2977/400=7.4425$, since superseded (T-082, T-090), with total mass \(5099/100 = 50.99 < 51\)$5099/100=50.99<51$, accepted by Tokoharu’s unchanged interval checker. The complete 201-direction coverage replay here accepted it again on 3 October, after this repository’s exact audit checked that the regenerated checker input is the published one and checked the mass and net premises, so it was the verified lower bound from its entry on 6 October (T-070) until T-090’s certificate was decided here later that day. wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-10-05. wand125’s mixed-certificate source reports \(s(51) \ge 747/100 = 7.47\)$s(51)\ge 747/100=7.47$ (T-090), from a density of 489 rectangles of total mass \(5099999/100000 < 51\)$5099999/100000<51$, accepted there at every net angle by its research copy of Tokoharu’s checker at threshold one. It is above the \(373/50\)$373/50$ this case reported, by \(0.01\)$0.01$. It supersedes the source’s mixed_n51_L746. sqverify-fast, this repository’s clean-room verifier, decided it here on 6 October 2026 at all 201 net directions, so it is also the verified lower bound: confirmed, independently re-implemented. wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-10-03. wand125’s mixed-certificate source reports the mixed certificate mixed_n51_L746 at side \(373/50 = 7.46\)$373/50=7.46$ (T-082), since superseded (T-090), from a density of 446 rectangles of total mass \(5099999/100000 < 51\)$5099999/100000<51$, accepted there at every net angle by its research copy of Tokoharu’s checker at threshold one. It is above the \(2977/400\)$2977/400$ this case reported, by \(0.0175\)$0.0175$. sqverify-fast, this repository’s clean-room verifier, decided it here on 6 October 2026 at all 201 net directions: confirmed, independently re-implemented. The verified lower bound is unchanged, the certificate above being higher. wand125’s README says parts of the work were produced with AI assistance under human direction.

Verified lower bound, 2026-10-02. wand125’s mixed rectangle-density certificate for 50 squares (T-048), of mass \(4999999/100000 < 51\)$4999999/100000<51$, carries \(s (51) \ge 37 / 5 = 7.4\)$s(51)\ge 37/5=7.4$ here by monotonicity: its complete replay passed here on 29 September, so it was the verified lower bound until 6 October, above Nagamochi’s closed form, which has been a reported bound since Karakuş’s finding (see below). The reported bound below was higher and had not then been replayed; on 6 October rect_n51_L74425’s \(2977/400 = 7.4425\)$2977/400=7.4425$ (T-070), whose complete replay with Tokoharu’s checker ran on 3 October, replaced it, and T-090’s \(747/100\)$747/100$ (above) replaced that later the same day. wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-09-28. wand125’s rectangle-density source reports the rectangle certificate rect_n51_L74425 at side \(2977/400 = 7.4425\)$2977/400=7.4425$, since superseded (T-082), with total mass \(5099/100 = 50.99 < 51\)$5099/100=50.99<51$, accepted by Tokoharu’s unchanged interval checker. This repository’s exact audit checks that the regenerated checker input is the published one, and checks the mass and net premises; the complete coverage replay had not yet run here, so the verified lower bound was unchanged until that replay was entered on 6 October (T-070, above). wand125’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-09-27. wand125’s rectangle-density source reports a direct \(743/100 = 7.43\)$743/100=7.43$ certificate for this case, whose reported bound the 2026-09-28 intake above raises, with total mass \(5099/100 = 50.99 < 51\)$5099/100=50.99<51$, accepted by Tokoharu’s unchanged interval checker. This repository’s exact audit checks that the regenerated checker input is the published one, and checks the mass and net premises; the complete coverage replay has not yet run here, so the verified lower bound is unchanged.

\(s(51) \le 7.70079923541701\ldots\)$s(51)\le 7.70079923541701\dots$, found by Thomas Schadt in January 2026 by simulated annealing, refound and refined by David Ellsworth, and analytically optimized to a degree-12 algebraic number in February 2026.

The exact certificate

Evan 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 51 squares, each a rational centre and a rational \(t = \tan(\theta/2)\)$t=\tan (\theta /2)$, in a square of side \(7.7007992354170117236\ldots\)$7.7007992354170117236\dots$, \(1.7 \times 10^{-15}\)$1.7\times {10}^{-15}$ above the side the Kingbird catalogue prints, \(7.70079923541701\)$7.70079923541701$. Rounded to binary64, square for square, its pose is the one the atlas pictures for this count. Evan 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 \(\mathbb{Q}\)$\mathbb{Q}$ 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(51) \le 7.70079923541702\)$s(51)\le 7.70079923541702$, the verified upper bound: 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 verified upper bound and the printed side now agree to one unit of the printed side’s last place, the precision at which the record compares them. The printed side itself is not certified here: the certificate’s side lies above it.

The best published data on how hard these searches are

This case matters out of proportion to its size because Ellsworth published run statistics for it, and they are the most informative artifact in the entire subject. Across nine sessions on an NVIDIA RTX 3080 Ti with the annealer configured for 65,536 threads, the search found 3,004 distinct basins, of which only 4 refine to the record — about 23.6 seconds per basin, and an expected 4.9 hours of GPU time to hit the record basin once. Ellsworth’s own description: “an exceedingly rare find.”

That quantifies the shape of the objective landscape better than any prose can. The optimum is a needle among thousands of basins that look almost as good, which is why general-purpose global optimization loses ground past \(n \approx 16\)$n\approx 16$ and why the records are held by a purpose-built stochastic searcher rather than a solver.

It is also why an open annealer with reproducible, counter-based randomness would be worth building: statistics like these exist for exactly two values of \(n\)$n$, and only because one person chose to publish them.

Reported Lower Bound

The earlier external report, [Friedman DS7], gives the lower-bound expression \(3 \sqrt{14} / 25 + 2 \sqrt{2} + 101 / 25\)$3\sqrt{14}/25+2\sqrt{2}+101/25$ for \(s(51)\)$s(51)$ (approximately \(7.317426011159\)$7.317426011159$). Friedman’s DS7 survey, Theorem 9, k=7, reports this bound at n=50; 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 = 7\)$k=7$ that point pattern leaves a unit square empty (review). Inherited at n=51 by monotonicity. wand125’s rectangle-density certificate above has since replaced it in the reported field, and the replayed \(s(50)\)$s(50)$ certificate the verified one, itself replaced on 6 October by the replayed rectangle certificate for this count, and that later the same day by this count’s own mixed certificate, decided here (above). Before that certificate the verified lower bound was \(7.16441400297\)$7.16441400297$, Nagamochi’s closed form (corrected 2 October 2026: a reported bound since that date, Karakuş’s general bound giving \(7.152067\)$7.152067$ here, since Nagamochi’s Lemma 1, on which the earlier value rested, is false; review). This register had recorded that proof as verified, its own error, logged as defect D-516. The source audit compares the exact theorem expressions separately from opaque table decimals.

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.