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)=k$s(k^2-3)=k$ for every $k\ge 6$$k\ge 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.

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.