Packing

This file contains a number of open problems related to the minimal size of a square (or circle) that can contain a given number of unit squares (or circles). In each case, we provide a known upper bound, and ask for the least such size.

References:

• Wikipedia on packing of squares
• Wikipedia on packing of circles in a circle
• Wikipedia on packing of circles in a square
• Friedman, Erich (2009), "Packing unit squares in squares: a survey and new results", Electronic Journal of Combinatorics, 1000, Dynamic Survey 7
• A website with visualizations of packings: link

def SquarePacking.Square (side : ℝ) : Set (EuclideanSpace ℝ (Fin 2))

A square of a particular side length as a subset of the Euclidean plane. Not including border, so that squares that touch at the border are disjoint, but a square internal to another shape is a subset of that shape.

Equations

• SquarePacking.Square side = {p : EuclideanSpace ℝ (Fin 2) | 0 < p 0 ∧ p 0 < side ∧ 0 < p 1 ∧ p 1 < side}

def SquarePacking.UnitSquare : Set (EuclideanSpace ℝ (Fin 2))

The unit square as a subset of the Euclidean plane.

Equations

• SquarePacking.UnitSquare = SquarePacking.Square 1

def SquarePacking.Circle (r : ℝ) : Set (EuclideanSpace ℝ (Fin 2))

A circle of a particular radius as a subset of the Euclidean plane. Not including border, so that circles that touch at the border are disjoint, but a circle internal to another shape is a subset of that shape.

Equations

• SquarePacking.Circle r = {p : EuclideanSpace ℝ (Fin 2) | p 0 ^ 2 + p 1 ^ 2 < r ^ 2}

def SquarePacking.UnitCircle : Set (EuclideanSpace ℝ (Fin 2))

The unit circle as a subset of the Euclidean plane.

Equations

• SquarePacking.UnitCircle = SquarePacking.Circle 1

structure SquarePacking.Packing (n : ℕ) (s S : Set (EuclideanSpace ℝ (Fin 2))) : Type

A structure representing a packing of n isometric embeddings of a set s inside a (presumably larger) set S.

• embeddings : Fin n → EuclideanSpace ℝ (Fin 2) ≃ᵢ EuclideanSpace ℝ (Fin 2)

  The isometric equivalences that represent the transformations of the base shape to their locations in the packing.

• disjoint : Pairwise fun (i j : Fin n) => Disjoint (⇑(self.embeddings i) '' s) (⇑(self.embeddings j) '' s)

  The images of the embeddings are pairwise disjoint

• inside (i : Fin n) : ⇑(self.embeddings i) '' s ⊆ S

  The images of the embeddings are all inside the larger set S

theorem SquarePacking.eleven_square_packing_in_square_bound : Nonempty (Packing 11 UnitSquare (Square 3.877084))

Eleven unit squares can be packed into a square of side length < 3.877084.

Reference: Wikipedia

theorem SquarePacking.least_eleven_square_packing_in_square : IsLeast {x : ℝ | Nonempty (Packing 11 UnitSquare (Square x))} sorry

What is the smallest square that can contain 11 unit squares?

Reference: Wikipedia

theorem SquarePacking.seventeen_square_packing_in_square_bound : Nonempty (Packing 17 UnitSquare (Square 4.6756))

Seventeen unit squares can be packed into a square of side length < 4.6756.

Reference: Wikipedia

theorem SquarePacking.least_seventeen_square_packing_in_square : IsLeast {x : ℝ | Nonempty (Packing 17 UnitSquare (Square x))} sorry

What is the smallest square that can contain 17 unit squares?

Reference: Wikipedia

theorem SquarePacking.three_square_packing_in_circle_bound : Nonempty (Packing 3 UnitSquare (Circle (5 * √17 / 16)))

Three unit squares can be packed into a circle of radius (5 √17) / 16 ≈ 1.288.

Reference: Wikipedia

theorem SquarePacking.least_three_square_packing_in_circle : IsLeast {r : ℝ | Nonempty (Packing 3 UnitSquare (Circle r))} sorry

What is the smallest circle that can contain 3 unit squares?

Reference: Wikipedia

theorem SquarePacking.twenty_one_circle_packing_in_square_bound : Nonempty (Packing 21 UnitCircle (Square 9.359))

Twenty-one unit circles can be packed into a square of side length < 9.359.

Reference: Visualizations

theorem SquarePacking.least_twenty_one_circle_packing_in_square : IsLeast {x : ℝ | Nonempty (Packing 21 UnitCircle (Square x))} sorry

What is the smallest square that can contain 21 unit circles?

theorem SquarePacking.fifteen_circle_packing_in_circle_bound : Nonempty (Packing 15 UnitCircle (Circle (1 + √(6 + 2 / √5 + 4 * √(1 + 2 / √5)))))

Fifteen unit circles can be packed into a circle of radius 1 + √ (6 + 2/√5 + 4 √(1 + 2/√5)) ≈ 4.521.

Reference: Graham RL, Lubachevsky BD, Nurmela KJ, Ostergard PRJ. Dense packings of congruent circles in a circle. Discrete Math 1998;181:139–154.

theorem SquarePacking.least_fifteen_circle_packing_in_circle : IsLeast {r : ℝ | Nonempty (Packing 15 UnitCircle (Circle r))} sorry

What is the smallest circle that can contain 15 unit circles?

Reference: Graham RL, Lubachevsky BD, Nurmela KJ, Ostergard PRJ. Dense packings of congruent circles in a circle. Discrete Math 1998;181:139–154.