\(s (13)\)$s(13)$ — solved

\(s(13) = 4\)$s(13)=4$, proved by Wolfram Bentz (2010), in the same paper as \(s(46) = 7\)$s(46)=7$. The first new exact value proved after Stromquist’s 2003 \(s(10)\)$s(10)$.

The technique, and why it is the template worth studying

Bentz’s contribution is a genuine strengthening of the unavoidable-point method rather than a new idea: he replaces fixed point sets with continuously varying families of them, and introduces resources that are not points at all. His Corollary 7 requires a box whose centre lies in a certain rectangle to intersect two specified segments with total intersection length at least \(2\sqrt{2} - 2 \approx 0.828\)$2\sqrt{2}-2\approx 0.828$ — a measure-valued condition, not a hitting condition.

Read in the framework Bentz himself names in the 2016 sequel — resource starvation — this is the field drifting from integral transversals toward fractional ones: points worth 1, then sliding points, then segments measured by length, then continuously varying families. That drift is the most promising direction in the lower-bound literature, and \(n = 13\)$n=13$ is where it starts to pay.

A case-free proof, kernel-checked here

Evan Daniel’s evand/square-packing reports a second proof of the lower bound with no case analysis at all: one weighted closed cover of \([0,4]^2\)$[0,4{]}^2$, 3,621 rational points of total weight \(2591194431/200000000 = 12.955972155 < 13\)$2591194431/200000000=12.955972155<13$, such that every closed unit square in the container captures weight at least \(1\)$1$. The margin is zero at side 4, so an angle net cannot decide it; two exact checkers that share no code subdivide pose space instead, one over the symmetry-reduced domain and one over the full domain, and both reach no uncertified box. The theorem is Bentz’s; the source claims only the proof. The review of 27 September found it sound and re-ran the second checker on a few cells. The source’s CREDITS.md says the work was produced by Claude (Anthropic) in a single session under human direction.

On 28 September the source’s third checker, zmx2, certified the cover here over all 1,600 roots of its symmetry-reduced domain, with no uncertified box (E-n013-evand-casefree-cover-zmx2-replay). On 30 September the source’s Lean 4 proof was built here, from the retained project and Mathlib’s official cache. SquarePacking.s13_eq_4 : minSide 13 = 4 is checked by the Lean kernel from the definitions: closed unit squares with independent rotations, disjoint open interiors, inside the closed square \([0, s]^2\)$[0,s{]}^2$. That includes every one of the cover’s 209 data chunks, and the proof depends only on the standard axioms propext, Classical.choice and Quot.sound (E-n013-evand-casefree-cover-lean-kernel; receipts). So \(s(13) = 4\)$s(13)=4$ is the first exact value on this record checked by a proof assistant with no hypothesis. An independent review confirms that the Lean statement is \(s(13) = 4\)$s(13)=4$ in this record’s convention. That review was written by an AI lane, and V5 also needs a human expert’s review of the formalization, so T-006 stands at V3. It is not the first kernel-checked \(s(13) = 4\)$s(13)=4$ anywhere: the source’s literature note reports chelokot’s formalisation of Bentz’s argument. The same machinery gives the source’s \(s(32) = 6\)$s(32)=6$; see n-032.md.

The source’s literature note also reports, from chelokot’s Lean archive, that two of Bentz’s printed auxiliary point sets are avoidable and were repaired in that formalisation, with the theorem standing. The archive is not retained here and that report is unchecked; it is a different defect from the transposed Lemma 10 point this record already carries.

Its relationship to the open case at 12

\(s(13) = 4\)$s(13)=4$ is proved and \(s(12) = 4\)$s(12)=4$ is not, even though 12 is the smaller case. See n-012.md: excluding twelve squares from a side-4 container is strictly stronger than excluding thirteen, so the difficulty runs backwards here.

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.