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

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

Lower bound: $\sqrt{73}$ (≈8.544004) Verified (not in the literature)
Upper bound: $9$ Verified

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.

Updates from the literature