n = 8 · Case Records · The Squares Project

n = 8 proved ★ corrects Nagamochi 2005O=

$s (8) = 3$

The best packing known for 8 squares, side

3

234

2.8283.828

\sqrt{n}

\sqrt{n} + 1

Proven

$s (8) = 3$

new result
optimal
exact

Citation record n-008

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

Bounds

Best known packing

$3$

Construction: grid
Tilt angles: $0^{\circ}$
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$3$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Proved by: Said El Moumni 1999
Kind: counting
Note: El Moumni derives this case from Proposition 3's parallel-line intersection-length bound (printed pp. 288–289). Friedman's distinct DS7 Theorem 3 uses seven unavoidable points.
Source: [El Moumni 1999]
Evidence: E-migrated-lower-report

Verified lower bound

$3$

The reported value, verified here.

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

Gap

Solved: the verified bounds meet.

Results in the register

T-007 V0 C1 Nagamochi · 2026-08-31 · 321 cases
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
T-083 V3 C3 Karakuş · 2026-10-02 · 301 cases
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
T-084 V3 C3 Karakuş · 2026-10-02 · 16 cases
$s (k^{2} - 1) = k$ for every integer $k \geq 3$ ; $k = 3 \dots 18$ are the cases held here

Verification

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

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

Square 5 of the retained witness (witness id 6) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 2 of its 8 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.

Open questions

Priority: s(8) determined (Bajmoczy (via Schrijver, via Gobel))

Evidence and sources

6 evidence entries

E-kingbird-upper-register, E-migrated-lower-report, E-basic-grid-upper, E-karakus-strip-lower, E-karakus-strip-measure-interval, E-nagamochi-lower

[Kingbird] record catalogue
[El Moumni 1999] lower bound proof
[Friedman DS7] survey
[Karakuş 2026] lower bound proof

In the frontier survey On GitHub

$s (8)$ — solved

$s (8) = 3$ . El Moumni (1999) obtains the bound from parallel-line intersection lengths.

The packing

The record catalogue does not picture $n = 8$ : no arrangement has ever been found that beats the trivial $⌈ \sqrt{8} ⌉ = 3$ grid, so the grid is still the best known packing. That is a statement about what has been searched, not a proof.

The lower bound

El Moumni’s Proposition 3, printed pp. 288–289 (volume PDF pp. 294–295), counts the lengths of intersections between the packed squares and parallel line segments. Proposition 2 gives a minimum contribution from each square; the total available segment length bounds their sum. The last sentence of printed p. 289 applies this argument to $n = 8$ .

Friedman’s DS7, Theorem 3 gives a distinct proof using seven unavoidable points (Figure 25).

The verified lower-bound evidence recorded here is Karakuş’s rectangle bound, E-karakus-strip-lower, which gives exactly $s (k^{2} - 1) = k$ (T-084). Correction, 2 October 2026: until that date it was the Nagamochi result, E-nagamochi-lower, whose published proof rests on Nagamochi’s Lemma 1, which Karakuş showed false; its value here is the same, and it is now a reported bound (review of 2 October 2026). This register had recorded that proof as verified, its own error, logged as defect D-516.

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-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)