SquarePacking.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

16 declarations, 10 contain sorry, 0 declared as axioms

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
Pirl, U. (1969), "Der Mindestabstand von $n$ in der Einheitskreisscheibe gelegenen Punkten", Mathematische Nachrichten, 40: 111–124
A website with visualizations of packings: link
Erich Friedman, Squares in Circles
The-Anh Vu-Le, Lean 4 proof of Squares in Circles
Kenta Kitamura, Lean proof of the exact three-square minimum for Formal Conjectures

Imports (1)

FormalConjecturesUtil

def SquarePacking.Square A square of a particular side length as a subset of the Euclidean plane line 58 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Set, EuclideanSpace, Fin, OfNat.ofNat, Nat
Proof uses: Set.ofPred, And, LT.lt, WithLp.ofLp, ENNReal
12 instances, coercions and auxiliary constants left out.
```
def Square (side : ℝ) : Set ℝ² :=
…
```
def SquarePacking.UnitSquare The unit square as a subset of the Euclidean plane line 64 source
Source documentation
The unit square as a subset of the Euclidean plane.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: SquarePacking.Square
3 instances, coercions and auxiliary constants left out.
```
def UnitSquare : Set ℝ² := Square 1
```
Mentions: SquarePacking.Square
def SquarePacking.Circle A circle of a particular radius as a subset of the Euclidean plane line 72 source
Source documentation
A circle of a particular radius as a subset of the Euclidean plane. The radius is a nonnegative real, so that Circle r is always the disc of radius $r$. 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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Set.ofPred, LT.lt, HAdd.hAdd, HPow.hPow, WithLp.ofLp, ENNReal
17 instances, coercions and auxiliary constants left out.
```
def Circle (r : ℝ≥0) : Set ℝ² :=
…
```
def SquarePacking.UnitCircle The unit circle as a subset of the Euclidean plane line 78 source
Source documentation
The unit circle as a subset of the Euclidean plane.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: SquarePacking.Circle, NNReal
3 instances, coercions and auxiliary constants left out.
```
def UnitCircle : Set ℝ² := Circle 1
```
Mentions: SquarePacking.Circle
structure SquarePacking.Packing A structure representing a packing of n isometric embeddings of a set s inside a (presumably larger) set S line 84 source
Source documentation
A structure representing a packing of n isometric embeddings of a set s inside a (presumably larger) set S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, EuclideanSpace, Real, Fin, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
structure Packing (n : ℕ) (s : Set ℝ²) (S : Set ℝ²) where
…
```
theorem SquarePacking.circle_zero The degenerate circle is empty line 97 source
Source documentation
The degenerate circle is empty.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, SquarePacking.Circle, NNReal, EmptyCollection.emptyCollection
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, LE.le, HAdd.hAdd, HPow.hPow, WithLp.ofLp, ENNReal, id, Eq.trans, Not, LT.lt, False, congr, congrArg, congrFun', Set.ofPred, funext, zero_pow and 8 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem circle_zero : Circle 0 = ∅ := by
…
```
Mentions: SquarePacking.Circle
theorem SquarePacking.eleven_square_packing_in_square_bound Eleven unit squares can be packed into a square of side length < 3.877084 sorry line 109 source
Source documentation
Eleven unit squares can be packed into a square of side length < 3.877084.
Reference: Wikipedia

L4DEL explanation
Eleven unit squares can be packed into a square of side length < 3.877084. Reference: Wikipedia
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitSquare, SquarePacking.Square, OfScientific.ofScientific, Real, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem eleven_square_packing_in_square_bound :
    Nonempty (Packing 11 UnitSquare (Square 3.877084)) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitSquare, SquarePacking.Square
theorem SquarePacking.least_eleven_square_packing_in_square What is the smallest square that can contain 11 unit squares? sorry line 119 source
Source documentation
What is the smallest square that can contain 11 unit squares?
Reference: Wikipedia

L4DEL explanation
What is the smallest square that can contain 11 unit squares? Reference: Wikipedia
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: IsLeast, Real, Set.ofPred, Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitSquare, SquarePacking.Square, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem least_eleven_square_packing_in_square :
    IsLeast {x : ℝ | Nonempty (Packing 11 UnitSquare (Square x))} answer(sorry) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitSquare, SquarePacking.Square
theorem SquarePacking.seventeen_square_packing_in_square_bound Seventeen unit squares can be packed into a square of side length < 4.6756 sorry line 129 source
Source documentation
Seventeen unit squares can be packed into a square of side length < 4.6756.
Reference: Wikipedia

L4DEL explanation
Seventeen unit squares can be packed into a square of side length < 4.6756. Reference: Wikipedia
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitSquare, SquarePacking.Square, OfScientific.ofScientific, Real, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem seventeen_square_packing_in_square_bound :
    Nonempty (Packing 17 UnitSquare (Square 4.6756)) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitSquare, SquarePacking.Square
theorem SquarePacking.least_seventeen_square_packing_in_square What is the smallest square that can contain 17 unit squares? sorry line 139 source
Source documentation
What is the smallest square that can contain 17 unit squares?
Reference: Wikipedia

L4DEL explanation
What is the smallest square that can contain 17 unit squares? Reference: Wikipedia
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: IsLeast, Real, Set.ofPred, Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitSquare, SquarePacking.Square, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem least_seventeen_square_packing_in_square :
    IsLeast {x : ℝ | Nonempty (Packing 17 UnitSquare (Square x))} answer(sorry) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitSquare, SquarePacking.Square
theorem SquarePacking.three_square_packing_in_circle_bound Three unit squares can be packed into a circle of radius $(5 \sqrt{17}) / 16 \approx 1.288$ sorry line 149 source
Source documentation
Three unit squares can be packed into a circle of radius $(5 \sqrt{17}) / 16 \approx 1.288$.
Reference: Wikipedia

L4DEL explanation
Three unit squares can be packed into a circle of radius $(5 \sqrt{17}) / 16 \approx 1.288$. Reference: Wikipedia
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitSquare, SquarePacking.Circle, HDiv.hDiv, NNReal, HMul.hMul, OrderIso, NNReal.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem three_square_packing_in_circle_bound :
    Nonempty (Packing 3 UnitSquare (Circle ((5 * NNReal.sqrt 17) / 16))) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitSquare, SquarePacking.Circle
theorem SquarePacking.least_three_square_packing_in_circle sorry line 168 source
depends on sorry what this means
Statement uses: IsLeast, NNReal, Set.ofPred, Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitSquare, SquarePacking.Circle, HDiv.hDiv, HMul.hMul, OrderIso, NNReal.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem SquarePacking.twenty_one_circle_packing_in_square_bound Twenty-one unit circles can be packed into a square of side length < 9.359 sorry line 179 source
Source documentation
Twenty-one unit circles can be packed into a square of side length < 9.359.
Reference: Visualizations

L4DEL explanation
Twenty-one unit circles can be packed into a square of side length < 9.359. Reference: Visualizations
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitCircle, SquarePacking.Square, OfScientific.ofScientific, Real, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem twenty_one_circle_packing_in_square_bound :
    Nonempty (Packing 21 UnitCircle (Square 9.359)) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitCircle, SquarePacking.Square
theorem SquarePacking.least_twenty_one_circle_packing_in_square What is the smallest square that can contain 21 unit circles? sorry line 187 source
Source documentation
What is the smallest square that can contain 21 unit circles?

depends on sorry what this means
Statement uses: IsLeast, Real, Set.ofPred, Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitCircle, SquarePacking.Square, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem least_twenty_one_circle_packing_in_square :
    IsLeast {x : ℝ | Nonempty (Packing 21 UnitCircle (Square x))} answer(sorry) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitCircle, SquarePacking.Square
theorem SquarePacking.fifteen_circle_packing_in_circle_bound Fifteen unit circles can be packed into a circle of radius $1 + \sqrt{6 + 2/\sqrt{5} + 4 \sqrt{1 + 2/\sqrt{5}}} \approx 4.521$ sorry line 200 source
Source documentation
Fifteen unit circles can be packed into a circle of radius $1 + \sqrt{6 + 2/\sqrt{5} + 4 \sqrt{1 + 2/\sqrt{5}}} \approx 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.

depends on sorry what this means
Statement uses: Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitCircle, SquarePacking.Circle, HAdd.hAdd, NNReal, OrderIso, NNReal.sqrt, HDiv.hDiv, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem fifteen_circle_packing_in_circle_bound :
    Nonempty (Packing 15 UnitCircle
      (Circle (1 + NNReal.sqrt (6 + 2 / NNReal.sqrt 5 +
        4 * NNReal.sqrt (1 + 2 / NNReal.sqrt 5))))) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitCircle, SquarePacking.Circle
theorem SquarePacking.least_fifteen_circle_packing_in_circle What is the smallest circle that can contain 15 unit circles? sorry line 215 source
Source documentation
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. Pirl (1969) conjectured this configuration to be optimal.

L4DEL explanation
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. Pirl (1969) conjectured this configuration to be optimal.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: IsLeast, NNReal, Set.ofPred, Nonempty, SquarePacking.Packing, OfNat.ofNat, Nat, SquarePacking.UnitCircle, SquarePacking.Circle, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem least_fifteen_circle_packing_in_circle :
    IsLeast {r : ℝ≥0 | Nonempty (Packing 15 UnitCircle (Circle r))} answer(sorry) := by
…
```
Mentions: SquarePacking.Packing, SquarePacking.UnitCircle, SquarePacking.Circle