The Squares Project

Work on the square packing problem has exploded in the summer of 2026 thanks to AI-powered research efforts.

Contributions include:

• Joshua Levy began the Squares Project in August 2026 with new lower bounds for $n=11,17,18,19,20$n=11,17,18,19,20 and other low values.
• Marc Leonard Overbeck’s certified lower bound of $31/8$31/8 for eleven squares.
• Manasseh Ahmed’s proof of optimality for eleven squares.
• Independently, Evan Daniel has proved the optimality of an infinite family, s(k2−3)=ks(k2−3)=k for every $k\ge 6$k≥6, along with exact values at 21, 32, 45 and 60 squares.
• Marc Leonard Overbeck’s candidate proof for seventeen squares, reported and unverified here (V0/C1).
• Oscar Fitzharding’s Lean proof report for seventeen squares, also unverified here (V0/C1).

Other new results are tabulated on the Results page. See the Contributor Profiles for credited contributors and authors.

This project now independently tabulates all known new results and does AI-assisted verification of the proofs and certificates behind them, to encourage open collaboration on open questions and formalizations of current proofs.

We also have a group chat. Contact ojoshe on X if you wish to join.