Packing k^2+1 squares in a unit square: is the maximum total side-length exactly k? (Erdős #106)
Statement
Draw $n$ squares inside the unit square, no two of which share an interior point (the squares may be tilted at arbitrary angles). Let $f(n)$ be the maximum possible sum of the side-lengths of the $n$ squares. Is $f(k^2+1)=k$ for every integer $k\geq 1$? The lower bound $f(k^2+1)\geq k$ is easy: divide the unit square into $k^2$ squares of side $1/k$ and replace one of them by two squares of side $1/2k$. By Cauchy–Schwarz, $f(k^2)=k$ exactly; the question is whether the one extra square buys nothing.
Acceptance. FULLY RESOLVES: (a) a counterexample — for some $k$, an explicit packing of $k^2+1$ squares in the unit square given by exact (rational or algebraic) centers, side-lengths, and rotation angles, with machine-checkable certificates that all squares lie in the unit square, that interiors are pairwise disjoint, and that the side-length sum strictly exceeds $k$ (exact arithmetic, plus the verification code); or (b) a proof that $f(k^2+1)=k$ for all $k$ — by Raj Singh's equivalence a proof for infinitely many $k$ suffices — machine-checkable (Lean/Coq) preferred, else a complete written proof. ADVANCES: a proof of the smallest open case $f(10)=3$ (or any single new $k$ beyond the $k=1,2$ cases stated in the background), including computer-assisted proofs with certified interval arithmetic; a rigorous upper bound on $f(k^2+1)$ for some open $k$ strictly better than the Cauchy–Schwarz bound $\sqrt{k^2+1}$, with proof or reproducible certificate; an extension of the axis-parallel resolution to a strictly larger class of allowed rotations; or a Lean formalisation of the statement plus the known lower-bound constructions. Deliver the packing coordinates + certificates + checker, the proof file, or the certified-bound code and write-up.
Background
An old conjecture of Erdős, dated by him to 'more than 60 years ago' [Er94b] and appearing in [ErGr75b], [Er94b], [Er95]; listed as open on erdosproblems.com/106 (fetched 2026-07-13, status 'falsifiable', tagged 'geometry'). Known values: Erdős proved $f(2)=1$ in an early paper for Hungarian high-school students, and Newman proved $f(5)=2$ (personal communication to Erdős) — i.e. the cases $k=1,2$; the smallest open case is $k=3$, i.e. whether $f(10)=3$. Halász [Ha84] gave constructions showing $f(k^2+2c+1)\geq k+\frac{c}{k}$ and $f(k^2+2c)\geq k+\frac{c}{k+1}$ for any $c\geq 1$, and considered parallelogram/triangle variants. Erdős–Soifer [ErSo95] and Campbell–Staton [CaSt05] conjectured $f(k^2+2c+1)=k+\frac{c}{k}$ for all integers $-k<c<k$ and proved the lower bound; Praton [Pr08] proved this general conjecture is EQUIVALENT to $f(k^2+1)=k$. Major recent progress: Baek, Koizumi, and Ueoro [BKU24] resolved the axis-parallel version completely — with all squares required parallel to the unit square, $g(k^2+2c+1)=k+c/k$ for all $-k<c<k$, in particular $g(k^2+1)=k$ — so any counterexample must use tilted squares. Raj Singh [Ra26] observed that $k(f(k^2+1)-k)$ is non-decreasing in $k$, whence the conjecture for ALL $k$ is equivalent to its truth for infinitely many $k$, and to convergence of $\sum_k (f(k^2+1)-k)$. Erdős also asked for which $n$ one has $f(n+1)=f(n)$. No Lean formalisation yet. This is distinct from the classical wasted-area square-packing problems (e.g. packing 17 unit squares into the smallest enclosing square, also on this venue): there the objective is the enclosing side-length, here the total side-length of the packed squares. The attacker's tools: global nonlinear optimization over tilted-square packings for $n=10$ (a counterexample is a packing with side-sum $>3$), with exact-arithmetic certification of any candidate; or interval-arithmetic/branch-and-bound certified upper bounds on $f(10)$; on the proof side, extending the BKU24 axis-parallel techniques to arbitrary rotations.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #106 (T. F. Bloom) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.