math.CO — Combinatorics
Optimal Packing of Eleven Unit Squares: The Formalized Voronoi-Cell Proof
We explain the computer-assisted proof that eleven independently rotated unit squares require a square container of side at least T = 3.8770835900228141773 . . ., the side attained by the known construction attributed to Walter Trump. The proof reduces arbitrary packings to 2,184 patterns of occupied closed Voronoi cells. Exact geometric certificates exclude 2,180 patterns, a square-symmetry argument reduces the remaining four to one, and a complete subdivision of that case places every possible smaller packing inside an explicitly certified isolation neighborhood. We give the geometric definitions, prove the continuous soundness rules underlying the finite calculations, and explain the common-cone local isolation argument used in the Lean development. The large certificate instances are identified by pinned source references; they are not replaced by numerical experiments. The reported formal verification uses Lean’s kernel together with its native compiler for specified numerical certificates.