$n=46$$n=46$

$s(46)$$s(46)$ — solved

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

The m2−3$m^2-3$ family

46=72−3$46=7^2-3$. Until September 2026 the family s(m2−3)=m$s(m^2-3)=m$ was known exactly only at $m=3,4,5,6,7$$m=3,4,5,6,7$: $s(6)=3$$s(6)=3$, $s(13)=4$$s(13)=4$, $s(22)=5$$s(22)=5$, $s(33)=6$$s(33)=6$, and this case, which was then the largest $n$$n$ known exactly other than through the two general families (perfect squares, and Nagamochi’s m2−1$m^2-1$, m2−2$m^2-2$). Corrected 2 October 2026: Nagamochi’s proof of both families is incomplete, his Lemma 1 being false; m2−1$m^2-1$ is proved again by Karakuş (T-084) and m2−2$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.

The family is no longer a conjecture. Daniel proved s(k2−3)=k$s(k^2-3)=k$ for every integer $k\ge 6$$k\ge 6$ (T-064), which with the five cases above gives s(m2−3)=m$s(m^2-3)=m$ for every $m\ge 3$$m\ge 3$.

A second proof, replayed here

$s(46)=7$$s(46)=7$ is the case $k=7$$k=7$ of Daniel’s theorem, and its finite statement, Valid7, is a statement about this case’s own container: every closed unit square in [0,7]2$[0,7{]}^2$ has mass at least one under a measure of total mass below $46$$46$. Daniel’s exact checker of Valid7 was replayed here in full on the retained cover on 2 and 3 October 2026, every root’s leaves equal to the published run’s (E-k2m3-evand-valid7-qx2-replay), and his Lean reduction from it to every $k\ge 6$$k\ge 6$ was built here with the pinned toolchain and depends only on the standard axioms (E-k2m3-evand-bentz-lean-build). The verified lower bound cites both beside Bentz’s proof since 11 October 2026; until then it cited the proof and this repository’s audit of its Theorem 8 alone. The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.

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.