Optimal packing of 11 squares proved and formalized with AI assistance

The square packing project announced that the classic combinatorial geometry problem of packing 11 unit squares into the smallest possible square has been proven optimal: the machine-checked proof T-060 confirms that Trump's 1979 layout is the optimal solution, with optimal side length s(11)=3.87708359…. The formal verification was carried out in the Lean proof assistant with help from Astra and Claude. This is another practical advance in AI-assisted mathematical research and worth attention.

Confirmed

• The optimal value is s(11)=3.87708359…, corresponding to Trump's 1979 layout, confirmed optimal by the machine-checked proof T-060
• The formal verification was done in Lean using proof assistants Astra and Claude
• ctjlewis handled compiling the Lean proofs and teaching the team to use a GitHub Actions runner; his organization provided a 64-core hosted runner to speed things up, and compiling Lean alone cost $300
• According to ctjlewis, The Squares Project was started by Joshua Levy in August 2026 and showcases progress on square packing under AI-assisted research: new lower bounds were obtained for low values such as n=11 and 17-20, and Kleddamag achieved a certified lower bound of 31/8
• The project produced a series of papers

Why it matters

• The "cursed" n=11 configuration has long been considered an intractable geometric packing problem; proving its optimality alongside formal verification is substantive progress in combinatorial geometry
• The whole workflow demonstrates a viable path for AI (Astra, Claude) and human mathematicians to collaborate on completing and verifying nontrivial mathematical proofs, at controllable cost (compilation was only $300) and with easily reusable infrastructure (GitHub Actions runner)

2026-10-07 ~ 2026-10-07 · 6 related posts

• 11-Square Packing Optimality Proved and Formalized in Lean With Help From Astra and Claude — ctjlewis · 2026-10-07
• Compiling Lean for AI Math Proofs Cost ~$300 on a 64-Core GitHub Runner — ctjlewis · 2026-10-07
• AI-Assisted Square Packing Breakthroughs: Optimality Proof for n=11, New Bounds Up to 53 — ctjlewis · 2026-10-07
• [source] Formal verification proves the cursed n=11 square packing is optimal — ctjlewis · 2026-10-07
• [source] Collaborative AI-assisted proofs settle 11-square packing: Trump's 1979 layout proven optimal — ctjlewis · 2026-10-07
• 11-Square Packing Optimality Formalized in Lean with Help from Claude — ctjlewis · 2026-10-07