n = 46 · Case Records · The Squares Project

n = 46 provedO=

$s (46) = 7$

The best packing known for 46 squares, side

7

, Wolfram Bentz 2009

678

6.7827.782

\sqrt{n}

\sqrt{n} + 1

Proven

$s (46) = 7$

optimal
exact

Citation record n-046

lowerBentz 2010, Electron. J. Combin. 17 (confirmed T-004, T-008)

Bounds

Best known packing

$7$

Found by: Wolfram Bentz 2009
Construction: hand
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$7$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Proved by: Wolfram Bentz 2010
Kind: unavoidable points
Source: [Bentz 2010]
Evidence: E-bentz-2010-proof

Verified lower bound

$7$

The reported value, verified here.

Evidence: E-bentz-2010-proof, E-bentz46-theorem8-audit

Gap

Solved: the verified bounds meet.

Results in the register

T-004 V3 C3 Bentz · 2026-08-31 · n = 46
Bentz 2010, Theorem 8 ( $s (46) \geq 7$ ) is correct as printed, machine-audited in full
Claim and records
Claim
Bentz 2010, Theorem 8: the printed 45-point unavoidable-set argument for $s (46) \geq 7$ is correct as printed, machine-audited in full.
Next rung
V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A second independent mechanism, such as the pose-space interval audit generalized to Q(sqrt 2, sqrt 3) sides, would be shown beside the rung as a second machine method. Rung 5 needs a proof-assistant formalization reviewed by human experts.
Significance
As far as the archived corpus shows, the first machine verification of a published unavoidable-set proof in this literature; the theorem is Bentz's, the audit is the contribution.
Novelty
previously-published Present in an identified source
Records
n = 46 register evidence 1 evidence 2 source
n = 46 register evidence 1 evidence 2 source
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-008 V3 C3 Bentz · 2026-08-31 · n = 46
$s (46) = 7$
Claim and records
Claim
$s (46) = 7$ : the lower half by T-004's audited unavoidable set, the upper half by the exact $7 \times 7$ grid packing of 46 squares.
Composition
Compound: lower = T-004 (exact-algebraic audit), upper = the grid bound replayed exactly by the basic-bounds checker. Under epistemics.md's rule for an equality whose upper half is an exactly replayed packing, the lower half sets the rung: it is machine-replayed here, so the equality is C3.
Next rung
Rises with T-004: V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. A method-independent second confirmation of the lower half would be shown beside the rung.
Significance
The first equality from the literature whose both halves are machine-confirmed here end-to-end.
Novelty
previously-published Present in an identified source
Records
n = 46 register evidence 1 evidence 2 evidence 3 source
n = 46 register evidence 1 evidence 2 evidence 3 source
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-064 V3 C3 Daniel after Burns, Massaccesi · 2026-10-01 · 13 cases
$s (k^{2} - 3) = k$ for every integer $k$ from 6 up; $k = 6 \dots 18$ are the cases held here
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-085 V3 C3 Karakuş; chelokot · 2026-10-02 · 315 cases
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$

Verification

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

—

Rigidity

not rigid, numerically checked, numerical multiprecision

Evidence: E-translation-escape-not-rigid

Scope

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

Evidence and sources

5 evidence entries

E-kingbird-upper-register, E-basic-grid-upper, E-nagamochi-lower, E-bentz-2010-proof, E-bentz46-theorem8-audit

[Kingbird] record catalogue
[Bentz 2010] lower bound proof
[Friedman DS7] survey

In the frontier survey On GitHub

$s (46)$ — solved

$s (46) = 7$ , proved by Wolfram Bentz (2010) in the same paper as $s (13) = 4$ .

The largest non-trivial proved case

At $n = 46$ this is the largest $n$ for which $s (n)$ is known exactly other than through the two general families (perfect squares, and Nagamochi’s $m^{2} - 1$ , $m^{2} - 2$ ). It belongs to the $m^{2} - 3$ family — $49 - 3 = 46$ — for which exact values are known only at $m = 3, 4, 5, 6, 7$ : that is $s (6) = 3$ , $s (13) = 4$ , $s (22) = 5$ , $s (33) = 6$ , and this case. Corrected 2 October 2026: Nagamochi’s proof of both families is incomplete, his Lemma 1 being false; $m^{2} - 1$ is proved again by Karakuş (T-084) and $m^{2} - 2$ by chelokot’s Lean proof, replayed here (T-086; review). This register had recorded that proof as verified, its own error, logged as defect D-516.

Whether $s (m^{2} - 3) = m$ holds for all $m \geq 3$ is an open conjecture. The evidence is five consecutive confirmations and no proof of the general statement — which, given that the analogous conjecture $s (n^{2} - n) = n$ survives small cases and then fails at $n = 17$ , is weaker evidence than it looks.

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-bentz-2010-proof`	a published proof	no code	no verification code
verified lower	`E-bentz46-theorem8-audit`	audited here	independent	`V-sqpack-cover` (first-party)
verified upper	`E-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)

Bounds

Results in the register

\(s (46)\)s(46) — solved

The largest non-trivial proved case

Verification Code

$s (46)$ — solved