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

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

Lower bound: $\sqrt{69}$ (≈8.306624) Verified (not in the literature)
Upper bound: ${\approx}8.8272$

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