AI-Assisted Proof of the Optimal Packing Problem for 11 Squares

A Geometric Puzzle That Has Long Stumped Mathematicians

Square packing is a classic problem in combinatorial geometry: how do you fit n unit squares into the smallest possible larger square without overlap? The question sounds straightforward, yet hides remarkable complexity. When n is not a perfect square (such as 4, 9, or 16), the optimal arrangement is often not a neat grid but instead involves counterintuitive layouts with tilted and offset squares.

The difficulty lies in the continuity of the solution space — squares can be rotated at any angle and placed at any position, making exhaustive search and traditional geometric proofs extremely challenging. For small values of n, mathematicians have spent decades gradually confirming optimal solutions. For a moderate case like n=11, a rigorous proof of the optimal packing arrangement has remained an open problem.

For n=11, the currently known optimal solution compresses the side length of the enclosing square to approximately 3.8772…, with some of the smaller squares needing to be rotated by roughly arctan(1/3) ≈ 18.43° to achieve the most compact fit. This non-obvious angle is no accident — it arises because a rotated square can more effectively exploit corner space along the diagonal. Meir and Moser systematically posed this class of packing problems in 1968, and researchers including Erdős later studied them, but rigorous optimality proofs advanced slowly, with optimal solutions for many small values of n only being confirmed through the 1990s and into the 2000s.

A New Attempt at AI-Assisted Mathematical Proof

The work that recently sparked discussion on Hacker News is about using AI assistance to prove the optimal packing arrangement for 11 squares. The core value of an "AI-assisted proof" is not having AI conjure answers from thin air, but rather leveraging computational and search capabilities to help human mathematicians handle the kind of exhaustive case analysis that is impractical to do by hand.

In packing problems, proving that an arrangement is optimal is far harder than finding a good arrangement. Finding a good arrangement only requires construction; proving optimality means ruling out every possible arrangement that could be better. This typically involves an enormous number of geometric constraints and boundary cases. AI and automated tools contribute by systematically searching the configuration space, verifying constraints, and helping narrow things down to a finite set of cases that can then be rigorously argued.

Why This Work Deserves Attention

This work illustrates a new role for AI in mathematical research — not replacing proofs, but acting as a "proof assistant" that handles the heavy lifting of verification and enumeration. This aligns with a broader trend in the application of formal proof tools (such as Lean) and SAT/SMT solvers to mathematics.

What makes square packing particularly interesting is its continuity and geometric intuitiveness. Many optimal solutions look "unnatural" — requiring certain squares to be rotated by specific non-standard angles. Human intuition tends to fail on such problems, and computational assistance is precisely what compensates for this weakness. For the n=11 optimality proof, researchers need to establish a strict lower bound over a continuous parameter space — a quintessential scenario where pure computational search falls short and human-machine collaboration becomes essential.

Formal proof tools (such as Lean, Coq, and Isabelle) are software systems that allow mathematicians to write proofs in a machine-verifiable language, with every inference step checked by a computational kernel for logical correctness. SAT/SMT solvers are specialized tools for determining the satisfiability of Boolean or arithmetic constraints, capable of efficiently finding counterexamples or proving unsatisfiability across vast discrete or semi-continuous search spaces. In packing problems, researchers typically discretize or interval-bound the continuous geometric constraints before passing them to such solvers, transforming the geometric question "does a better arrangement exist?" into an automatically decidable constraint-satisfaction task.

The Significance and Limitations of Human-Machine Collaborative Proofs

From a broader perspective, AI-assisted mathematical proof is becoming an active research direction. It raises some thought-provoking questions: when critical steps in a proof rely on computer enumeration, is such a proof sufficiently "trustworthy"? The four-color theorem once sparked controversy precisely because it relied on computer verification. Today, with formalizable and reproducible toolchains, such concerns are gradually being addressed.

That said, a clear-eyed view is warranted: results of this kind still belong to a relatively niche, specialized domain. While the packing of 11 squares is representative, there is a long road between this and AI independently resolving major mathematical conjectures. AI largely plays the role of an amplifier of human capability; the genuine mathematical insight and proof strategy still come from the researchers themselves.

The four-color theorem (1976) is the most famous precedent for computer-assisted proof: Appel and Haken reduced the map-coloring problem to checking approximately 1,936 configurations, each verified by computer. This approach triggered years of controversy in the mathematical community, centered on the question: "If humans cannot directly inspect every step of the proof, can it truly be considered rigorous?" That debate has largely been settled, thanks to Gonthier's complete formal verification of the four-color theorem using Coq in 2005 — formal language provides a path for the community to independently reproduce and audit the proof, narrowing the scope of "trust in a computer program" to a small, widely audited proof kernel.

Conclusion

The optimality proof for packing 11 squares is yet another example of AI and computational tools making inroads into pure mathematical research. It demonstrates a pragmatic model of collaboration: let machines handle the tedious search and verification, while humans focus on structural insight. As formal proof systems and AI reasoning capabilities continue to advance, we may see more and more mathematical results once considered "impossible to complete by hand" being rigorously established.

(Note: This article is based on limited discussion from Hacker News. For specific proof details, readers are encouraged to consult the original research paper.)