$n=78$$n=78$

$s(78)$$s(78)$ — solved

$s(78)=9$$s(78)=9$, by monotonicity from $s(77)=9$$s(77)=9$ (T-067): removing a square from a packing leaves a packing, so $s(78)$$s(78)$ is at least $s(77)$$s(77)$, and the $9\times 9$$9\times 9$ grid holds 78. The premise is Hosono’s mixed cover, whose interval check was replayed here in full; its total is below 78 too, so the same certificate decides this case. Hosono’s README says parts of the work were produced with AI assistance under human direction. The value is also the case $k=9$$k=9$ of Daniel’s family s(k2−3)=k$s(k^2-3)=k$ (T-064), whose certificate was replayed here on 2 and 3 October 2026: its finite statement Valid7 in full, and its Lean reduction built with the pinned toolchain. The verified lower bound cites Hosono’s cover, which closed the case first.

External intake, 2026-10-01. Hosono’s rectangle-density source reports a direct $1793/200=8.965$$1793/200=8.965$ certificate for this case, with total mass $7799/100=77.99<78$$7799/100=77.99<78$, accepted by Tokoharu’s unchanged interval checker. Its complete coverage replay has not run here; the verified lower bound was $1791/200=8.955$$1791/200=8.955$ until 2 October 2026, from the source’s certificate for this count in the 2026-09-27 intake, whose complete 201-direction replay passed here. Hosono’s README says parts of the work were produced with AI assistance under human direction.

External intake, 2026-10-01. Daniel’s source reports $s(78)=9$$s(78)=9$ as the case $k=9$$k=9$ of s(k2−3)=k$s(k^2-3)=k$ for every integer $k\ge 6$$k\ge 6$ (T-064). By the source’s report, its Lean development derives the family from one finite covering statement, Valid7, which a single exact Python checker at the source decides. Neither had been run here when this was written; the case was closed on 2 October 2026 by the replay of Hosono’s $s(77)$$s(77)$ cover, which the lower bound below describes, and both were rebuilt here on 2 and 3 October. The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.

External intake, 2026-09-27. Hosono’s rectangle-density source reports a direct $1791/200=8.955$$1791/200=8.955$ certificate for this case, whose reported bound the 2026-10-01 intake above raises, with total mass $7799/100=77.99<78$$7799/100=77.99<78$, 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. Hosono’s README says parts of the work were produced with AI assistance under human direction.

The packing

The upper bound is trivial: the $9\times 9$$9\times 9$ grid holds 81 unit squares, so it holds 78 with three cells empty, and $s(78)\le 9$$s(78)\le 9$. The record catalogue does not picture $n=78$$n=78$, and no arrangement below side 9 has ever been found. What is new is that none exists.

The lower bound

The verified field rests on the complete replay here of zmx2 on Hosono’s $s(77)$$s(77)$ cover (E-n077-wand125-mixed-cover-zmx2-replay, V3/C3): all 8,100 D4 roots and all 64,800 unreduced roots certified on 2 October with no uncertified box, the box totals equal to the source’s. The cover’s total, 43347137744028965/249=76.99998460$43347137744028965/2^{49}=76.99998460$, is below 78, so a packing of 78 at a side below 9, scaled to side 9, would capture at least 78 from it. The case record for 77 squares describes the certificate and the review that found no defect in it, the corollary included.

Earlier lower bounds

Hosono’s rectangle-density certificate of 27 September, replayed here, gave $s(78)\ge 1791/200=8.955$$s(78)\ge 1791/200=8.955$, which was the verified lower bound until 2 October 2026. Before 2026 it was Nagamochi’s general closed form, now a reported bound (see the correction below). Karakuş’s general bound, independently verified here and below the exact value proved here, applies to every nonsquare $N\ge 8$$N\ge 8$:

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)$s(N)\ge min(\lceil \sqrt{N}\rceil ,\sqrt{N-2\lfloor \sqrt{N}\rfloor +1}+1)$, which is stronger at this $n$$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.

See the Frontier corpus summary for the current aggregate count; source-reported bounds are recorded separately.

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.