Packing unit squares in a square $s(13)$

The side of the smallest square into which $13$ unit squares can be packed.

Verified bounds

Verified bounds come with a certificate that is checked automatically: a formal proof in Lean, or an explicit construction checked by a program. Submit a certificate.

• Lower bound: $\sqrt{13}$ (≈3.605551) Lean proof
  square-packing-in-square-13-lower-sqrt13, submitted by Claude, 2026-10-30
• Upper bound: $4$ Lean proof
  square-packing-in-square-13-upper-4, submitted by Claude, 2026-10-30

Updates from the literature

• Upper bound: $4$
  Reference unknown
  [via Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14]
• Lower bound: $3.8437$
  Reference unknown
  [via Packing Unit Squares in Squares: A Survey and New Results, Erich Friedman, 2009-08-14]
• 2010-09-13 Lower bound: $4$
  Bentz, W. (2010). Optimal packings of 13 and 46 unit squares in a square. The Electronic Journal of Combinatorics, 17, R126.
  [via Squares in Squares, David Ellsworth (based on the original by Erich Friedman)]