34145.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

18 declarations, 4 contain sorry, 0 declared as axioms

Mathoverflow 34145

Can the unit square be covered by $1/k$-by-$1/(k+1)$ rectangles (across $1 \le k$ natural)?

I am deliberately not requiring that the rotations can only be $0^\circ, 90^\circ, 180^\circ, \text{ or } 270^\circ$.

Because of indexing, since n : ℕ starts at 0, we change the side lengths to $1 / (n + 1)$ and $1 / (n + 2)$, so that the first rectangle is $1/1$ by $1/2$, the second is $1/2$ by $1/3$, etc.

Reference: mathoverflow/34145 asked by user Kaveh

Imports (1)

FormalConjecturesUtil

structure Mathoverflow34145.Rectangle A rectangle is specified by its width, height, starting point, and rotation line 42 source
Source documentation
A rectangle is specified by its width, height, starting point, and rotation. The rectangle is assumed to start in the lower left corner. For example, the unit square $\{ (x, y) \mid 0 \le x \le 1, 0 \le y \le 1 \}$ is specified as ⟨1, 1, (0, 0), 0⟩

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure Rectangle : Type where
…
```
def Mathoverflow34145.rigidMotion A combination of a rotation and a translation to map the standard rectangle to the desired rectangle line 51 source
Source documentation
A combination of a rotation and a translation to map the standard rectangle to the desired rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real, Real.Angle
Proof uses: Prod.mk, HSub.hSub, HAdd.hAdd, Prod.fst, HMul.hMul, Real.Angle.cos, Prod.snd, Real.Angle.sin
6 instances, coercions and auxiliary constants left out.
```
noncomputable def rigidMotion (start : ℝ × ℝ) (θ : Angle) (p : ℝ × ℝ) : (ℝ × ℝ) :=
…
```
lemma Mathoverflow34145.rigidMotion_test line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Prod, Real, Mathoverflow34145.rigidMotion, Prod.mk, Real.sqrt, OfNat.ofNat, Nat, HDiv.hDiv, HMul.hMul, Real.pi, HSub.hSub, HAdd.hAdd, Neg.neg
Proof uses: Eq.mpr, And, Inv.inv, HPow.hPow, id, Eq.trans, congr, congrArg, Prod.fst, Real.Angle.cos, Prod.snd, Real.Angle.sin, Real.Angle, mul_div_assoc, Real.cos, Real.cos_two_mul, congrFun', Real.cos_pi_div_three, one_div, inv_pow and 94 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Mathoverflow34145.scale A scaling to map the unit square to a standard rectangle line 62 source
Source documentation
A scaling to map the unit square to a standard rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Prod
Proof uses: Prod.mk, HMul.hMul, Prod.fst, Prod.snd
2 instances, coercions and auxiliary constants left out.
```
noncomputable def scale (x y : ℝ) (p : ℝ × ℝ) : (ℝ × ℝ) :=
…
```
def Mathoverflow34145.unitSquare The unit square line 66 source
Source documentation
The unit square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Prod, Real
Proof uses: Set.ofPred, And, LE.le, OfNat.ofNat, Prod.fst, Prod.snd
5 instances, coercions and auxiliary constants left out.
```
def unitSquare : Set (ℝ × ℝ) :=
…
```
def Mathoverflow34145.Rectangle.toSet Converts a rectangle to a set in ℝ × ℝ line 70 source
Source documentation
Converts a rectangle to a set in ℝ × ℝ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mathoverflow34145.Rectangle, Set, Prod, Real
Proof uses: Set.image, Mathoverflow34145.rigidMotion, Mathoverflow34145.Rectangle.start, Mathoverflow34145.Rectangle.rotation, Mathoverflow34145.scale, Mathoverflow34145.Rectangle.width, Mathoverflow34145.Rectangle.height, Mathoverflow34145.unitSquare
```
def Rectangle.toSet (r : Rectangle) : Set (ℝ × ℝ) :=
…
```
Mentions: Mathoverflow34145.Rectangle
abbrev Mathoverflow34145.lbMeasure The standard Lebesgue measure on ℝ² line 74 source
Source documentation
The standard Lebesgue measure on ℝ².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.Measure, Prod, Real
Proof uses: Module.Basis.addHaar, Fin, OfNat.ofNat, Nat, Module.Basis.finTwoProd
16 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev lbMeasure : Measure (ℝ × ℝ) :=
…
```
lemma Mathoverflow34145.lbMeasure_rigidMotion lbMeasure is invariant under rigidMotion start θ line 79 source
Source documentation
lbMeasure is invariant under rigidMotion start θ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real, Real.Angle, Set, Eq, ENNReal, MeasureTheory.Measure, Mathoverflow34145.lbMeasure, Set.image, Mathoverflow34145.rigidMotion
Proof uses: Prod.mk, HSub.hSub, HMul.hMul, Prod.fst, Real.Angle.cos, Prod.snd, Real.Angle.sin, HAdd.hAdd, Trans.simple, Module.Basis.addHaar, Fin, OfNat.ofNat, Nat, Module.Basis.finTwoProd, Eq.trans, Set.preimage, Eq.symm, MeasureTheory.measure_preimage_add_right, congr_arg, Set.ext and 71 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma lbMeasure_rigidMotion (start : ℝ × ℝ) (θ : Angle) (s : Set (ℝ × ℝ)) :
    lbMeasure (rigidMotion start θ '' s) = lbMeasure s := by
…
```
Mentions: Mathoverflow34145.lbMeasure, Mathoverflow34145.rigidMotion
lemma Mathoverflow34145.lbMeasure_scale lbMeasure is scaled by scale line 93 source
Source documentation
lbMeasure is scaled by scale.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Set, Prod, Eq, ENNReal, MeasureTheory.Measure, Mathoverflow34145.lbMeasure, Set.image, Mathoverflow34145.scale, HMul.hMul, ENNReal.ofReal, abs
Proof uses: LinearMap, RingHom.id, LinearMap.mk, AddHom.mk, Prod.mk, Prod.fst, Prod.snd, of_eq_true, HAdd.hAdd, Eq.trans, True, congrFun', congrArg, congr, mul_add, eq_self, HSMul.hSMul, RingHom, Real.ringHom_apply, mul_left_comm and 62 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma lbMeasure_scale (x y : ℝ) (s : Set (ℝ × ℝ)) :
    lbMeasure (scale x y '' s) = .ofReal |x * y| * lbMeasure s := by
…
```
Mentions: Mathoverflow34145.lbMeasure, Mathoverflow34145.scale
lemma Mathoverflow34145.lbMeasure_unitSquare The Lebesgue measure of the unit square is 1 line 106 source
Source documentation
The Lebesgue measure of the unit square is 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENNReal, MeasureTheory.Measure, Prod, Real, Set, Mathoverflow34145.lbMeasure, Mathoverflow34145.unitSquare, OfNat.ofNat
Proof uses: Eq.mpr, Module.Basis.addHaar, Fin, Nat, Module.Basis.finTwoProd, TopologicalSpace.PositiveCompacts, Module.Basis.parallelepiped, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, Set.ext, Iff, Membership.mem, And, LE.le, Prod.fst and 46 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma lbMeasure_unitSquare : lbMeasure unitSquare = 1 := by
…
```
Mentions: Mathoverflow34145.lbMeasure, Mathoverflow34145.unitSquare
lemma Mathoverflow34145.lbMeasure_rectangle_toSet The Lebesgue measure of the a rectangle r is r.width * r.height line 117 source
Source documentation
The Lebesgue measure of the a rectangle r is r.width * r.height

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mathoverflow34145.Rectangle, Eq, ENNReal, MeasureTheory.Measure, Prod, Real, Set, Mathoverflow34145.lbMeasure, Mathoverflow34145.Rectangle.toSet, ENNReal.ofReal, abs, HMul.hMul, Mathoverflow34145.Rectangle.width, Mathoverflow34145.Rectangle.height
Proof uses: Eq.mpr, Set.image, Mathoverflow34145.rigidMotion, Mathoverflow34145.Rectangle.start, Mathoverflow34145.Rectangle.rotation, Mathoverflow34145.scale, Mathoverflow34145.unitSquare, id, congrArg, Mathoverflow34145.Rectangle.toSet.eq_1, Mathoverflow34145.lbMeasure_rigidMotion, Mathoverflow34145.lbMeasure_scale, OfNat.ofNat, Mathoverflow34145.lbMeasure_unitSquare, mul_one, Eq.refl
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma lbMeasure_rectangle_toSet (r : Rectangle) :
    lbMeasure r.toSet = .ofReal |r.width * r.height| := by
…
```
Mentions: Mathoverflow34145.Rectangle, Mathoverflow34145.lbMeasure
lemma Mathoverflow34145.tsum_area_eq_one The areas of the required rectangles sum to 1 line 123 source
Source documentation
The areas of the required rectangles sum to 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, tsum, Nat, HMul.hMul, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, SummationFilter.unconditional
Proof uses: Finset.sum, Finset.range, HSub.hSub, Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, Inv.inv, EmptyCollection.emptyCollection, Finset, funext, one_div, congrFun', CharP.cast_eq_zero, zero_add, div_self, Not, False and 125 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma tsum_area_eq_one : ∑' (n : ℕ), ((1 / (n + 1)) * (1 / (n + 2)) : ℝ) = 1 := by
…
```
structure Mathoverflow34145.Configuration A configuration of rectangles of sides 1 / (n + 1) and 1 / (n + 2) line 135 source
Source documentation
A configuration of rectangles of sides 1 / (n + 1) and 1 / (n + 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure Configuration : Type where
…
```
def Mathoverflow34145.Configuration.IsPacking A "packing" means that the interiors of any two rectangles are disjoint line 141 source
Source documentation
A "packing" means that the interiors of any two rectangles are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Mathoverflow34145.Configuration
Proof uses: Pairwise, Nat, Eq, Set, Prod, Real, Inter.inter, interior, Mathoverflow34145.Rectangle.toSet, Mathoverflow34145.Configuration.rect, EmptyCollection.emptyCollection
6 instances, coercions and auxiliary constants left out.
```
def Configuration.IsPacking (c : Configuration) : Prop :=
…
```
Mentions: c, Mathoverflow34145.Configuration
theorem Mathoverflow34145.rectangles_cover_unit_square Can a unit square be covered by rectangles of width 1 / (n + 1) and height 1 / (n + 2)? sorry line 146 source
Source documentation
Can a unit square be covered by rectangles of width 1 / (n + 1) and height 1 / (n + 2)?

depends on sorry what this means
Statement uses: Iff, True, Exists, Mathoverflow34145.Configuration, Prod, Real, Membership.mem, Set, Mathoverflow34145.unitSquare, Nat, Mathoverflow34145.Rectangle.toSet, Mathoverflow34145.Configuration.rect
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rectangles_cover_unit_square :
    answer(sorry) ↔ ∃ c : Configuration, ∀ p ∈ unitSquare, ∃ n, p ∈ (c.rect n).toSet := by
…
```
Mentions: c, Mathoverflow34145.Configuration, Mathoverflow34145.unitSquare
theorem Mathoverflow34145.rectangles_pack_unit_square Equivalently, can a unit square be packed with rectangles of width 1 / (n + 1) and height 1 / (n + 2)? sorry line 153 source
Source documentation
Equivalently, can a unit square be packed with rectangles of width 1 / (n + 1) and height 1 / (n + 2)?

depends on sorry what this means
Statement uses: Iff, True, Exists, Mathoverflow34145.Configuration, And, Nat, LE.le, Set, Prod, Real, Mathoverflow34145.Rectangle.toSet, Mathoverflow34145.Configuration.rect, Mathoverflow34145.unitSquare, Mathoverflow34145.Configuration.IsPacking
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rectangles_pack_unit_square :
    answer(sorry) ↔ ∃ c : Configuration, (∀ n, (c.rect n).toSet ⊆ unitSquare) ∧ c.IsPacking := by
…
```
Mentions: c, Mathoverflow34145.Configuration, Mathoverflow34145.unitSquare
theorem Mathoverflow34145.rectangles_pack_square_133_div_132 It is known that packing the rectangles into a square of side length 133/132 is possible sorry line 162 source
Source documentation
It is known that packing the rectangles into a square of side length 133/132 is possible.
Reference: https://www.sciencedirect.com/science/article/pii/0097316594901163

depends on sorry what this means
Statement uses: Exists, Mathoverflow34145.Configuration, And, Nat, LE.le, Set, Prod, Real, Mathoverflow34145.Rectangle.toSet, Mathoverflow34145.Configuration.rect, Mathoverflow34145.Rectangle.mk, HDiv.hDiv, OfNat.ofNat, Prod.mk, Real.Angle, Mathoverflow34145.Configuration.IsPacking
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rectangles_pack_square_133_div_132 :
    (∃ c : Configuration,
      (∀ n, (c.rect n).toSet ⊆ Rectangle.toSet ⟨133/132, 133/132, (0, 0), 0⟩) ∧
      c.IsPacking) := by
…
```
Mentions: c, Mathoverflow34145.Configuration, Mathoverflow34145.Rectangle.toSet
theorem Mathoverflow34145.rectangles_pack_square_501_div_500 It is known that packing the rectangles into a square of side length 501/500 is possible sorry line 173 source
Source documentation
It is known that packing the rectangles into a square of side length 501/500 is possible.
Reference: https://www.sciencedirect.com/science/article/pii/S0167506008706009

depends on sorry what this means
Statement uses: Exists, Mathoverflow34145.Configuration, And, Nat, LE.le, Set, Prod, Real, Mathoverflow34145.Rectangle.toSet, Mathoverflow34145.Configuration.rect, Mathoverflow34145.Rectangle.mk, HDiv.hDiv, OfNat.ofNat, Prod.mk, Real.Angle, Mathoverflow34145.Configuration.IsPacking
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rectangles_pack_square_501_div_500 :
    (∃ c : Configuration,
      (∀ n, (c.rect n).toSet ⊆ Rectangle.toSet ⟨501/500, 501/500, (0, 0), 0⟩) ∧
      c.IsPacking) := by
…
```
Mentions: c, Mathoverflow34145.Configuration, Mathoverflow34145.Rectangle.toSet