\(s (33)\)$s(33)$ — solved

\(s(33) = 6\)$s(33)=6$. Established by an unavoidable point set, Wolfram Bentz (2016).

The packing

Found by Wolfram Bentz in 2018, via a hand construction.

The lower bound

Proved by exhibiting an unavoidable set: a set of points in the container that every unit square placed inside must contain. With \(n - 1\)$n-1$ such points, \(n\)$n$ disjoint squares are impossible by pigeonhole. Nobody here has worked through Bentz’s argument.

A second proof, replayed here

\(s(33) = 6\)$s(33)=6$ is also the case \(k = 6\)$k=6$ of Evan Daniel’s \(s(k^2 - 3) = k\)$s(k^2-3)=k$ for every integer \(k \ge 6\)$k\ge 6$ (T-064). Its lower half rests on one finite statement, Valid7, and on a Lean reduction from it to every \(k \ge 6\)$k\ge 6$. 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 the reduction 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 6 October 2026; until then it cited the proof 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.