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

9 declarations, 6 contain sorry, 0 declared as axioms

Moser's Worm

Reference: Wikipedia

Imports (1)

FormalConjecturesUtil

def MoserWorm.Worms The set of worms is the set of curves of length (at most) 1 line 36 source
Source documentation
The set of worms is the set of curves of length (at most) 1. We formalize this as the set of ranges of 1-Lipschitz functions from [0,1] to ℝ².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Set.ofPred, Exists, Set.Icc, And, LipschitzWith, Membership.mem, ENNReal, NNReal, Eq, Set.range
22 instances, coercions and auxiliary constants left out.
```
def Worms : Set (Set ℝ²) :=
…
```
def MoserWorm.WormCovers The set of covers is the set of (measurable) sets that cover every worm by translation and rotation line 43 source
Source documentation
The set of covers is the set of (measurable) sets that cover every worm by translation and rotation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Set.ofPred, And, MeasurableSet, ENNReal, Membership.mem, MoserWorm.Worms, Exists, LinearIsometryEquiv, RingHom.id, Eq, Units, MonoidHom, LinearEquiv, LinearEquiv.det, LinearIsometryEquiv.toLinearEquiv, LE.le, Set.image, HAdd.hAdd
56 instances, coercions and auxiliary constants left out.
```
def WormCovers : Set (Set ℝ²) :=
…
```
theorem MoserWorm.disc_mem_worm_covers A disc of radius 1 / 2 is a worm cover line 53 source
Source documentation
A disc of radius 1 / 2 is a worm cover.
This follows by translating the center of the disc to the midpoint of the worm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, MoserWorm.WormCovers, Metric.closedBall, ENNReal, OfScientific.ofScientific, Bool.true
Proof uses: And.intro, MeasurableSet, MoserWorm.Worms, Exists, LinearIsometryEquiv, RingHom.id, And, Eq, Units, MonoidHom, LinearEquiv, LinearEquiv.det, LinearIsometryEquiv.toLinearEquiv, LE.le, Set.image, HAdd.hAdd, measurableSet_closedBall, Set.Icc, LipschitzWith, NNReal and 124 more
198 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem disc_mem_worm_covers : Metric.closedBall 0 0.5 ∈ WormCovers := by
…
```
Mentions: MoserWorm.WormCovers
theorem MoserWorm.mosers_worm_problem Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a shape that can cover every unit-length curve? sorry line 76 source
Source documentation
Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a shape that can cover every unit-length curve?

depends on sorry what this means
Statement uses: IsGLB, ENNReal, Set.ofPred, Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Membership.mem, MoserWorm.WormCovers, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
98 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem mosers_worm_problem :
    IsGLB {v | ∃ X ∈ WormCovers, volume X = v} answer(sorry) := by
…
```
Mentions: MoserWorm.WormCovers
theorem MoserWorm.mosers_worm_problem_upper_bound There is a set of area 0.260437 that covers all worms sorry line 88 source
Source documentation
There is a set of area 0.260437 that covers all worms.
Reference: Norwood, Rick; Poole, George (2003), "An improved upper bound for Leo Moser's worm problem", Discrete and Computational Geometry, 29 (3): 409–417, doi:10.1007/s00454-002-0774-3, MR 1961007.

depends on sorry what this means
Statement uses: Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Membership.mem, MoserWorm.WormCovers, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
100 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem mosers_worm_problem_upper_bound :
    ∃ X ∈ WormCovers, volume X = 0.260437 := by
…
```
Mentions: MoserWorm.WormCovers
theorem MoserWorm.convex_mosers_worm_problem Convex Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a convex shape that can cover every unit-length curve? sorry line 98 source
Source documentation
Convex Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a convex shape that can cover every unit-length curve?

depends on sorry what this means
Statement uses: IsGLB, ENNReal, Set.ofPred, Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Membership.mem, MoserWorm.WormCovers, Convex, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
114 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem convex_mosers_worm_problem :
    IsGLB {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} answer(sorry) := by
…
```
Mentions: MoserWorm.WormCovers
theorem MoserWorm.convex_mosers_worm_problem_bound_attained The minimal area of a convex shape that can cover every unit-length curve is attained sorry line 107 source
Source documentation
The minimal area of a convex shape that can cover every unit-length curve is attained. This follows from the Blaschke selection theorem.

depends on sorry what this means
Statement uses: Exists, ENNReal, IsLeast, Set.ofPred, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Membership.mem, MoserWorm.WormCovers, Convex, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
114 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem convex_mosers_worm_problem_bound_attained :
    ∃ bound, IsLeast {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} bound := by
…
```
Mentions: MoserWorm.WormCovers
theorem MoserWorm.convex_mosers_worm_problem_upper_bound There is a convex set of area 0.270911861 that covers all worms sorry line 119 source
Source documentation
There is a convex set of area 0.270911861 that covers all worms.
Reference: Wang, Wei (2006), "An improved upper bound for the worm problem", Acta Mathematica Sinica, 49 (4): 835–846, MR 2264090.

depends on sorry what this means
Statement uses: Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, MeasurableSet, ENNReal, Convex, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfScientific.ofScientific, Bool.true, Membership.mem, MoserWorm.Worms, LinearIsometryEquiv, RingHom.id and 8 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
186 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem convex_mosers_worm_problem_upper_bound :
    ∃ X : Set ℝ², MeasurableSet X ∧ Convex ℝ X ∧ volume X = 0.270911861 ∧
      ∀ w ∈ Worms, ∃ (e : ℝ² ≃ₗᵢ[ℝ] ℝ²) (v : ℝ²), e.toLinearEquiv.det = 1 ∧ w ⊆ (fun x => e x + v) '' X := by
…
```
Mentions: MoserWorm.Worms
theorem MoserWorm.convex_mosers_worm_problem_lower_bound 0.232239 is a lower bound on the area of a convex set that covers all worms sorry line 134 source
Source documentation
0.232239 is a lower bound on the area of a convex set that covers all worms.
Reference: Khandhawit, Tirasan; Pagonakis, Dimitrios; Sriswasdi, Sira (2013), "Lower Bound for Convex Hull Area and Universal Cover Problems", International Journal of Computational Geometry & Applications, 23 (3): 197–212, arXiv:1101.5638, doi:10.1142/S0218195913500076, MR 3158583, S2CID 207132316.

depends on sorry what this means
Statement uses: Membership.mem, ENNReal, Set, lowerBounds, Set.ofPred, Exists, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, MoserWorm.WormCovers, Convex, Eq, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
118 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem convex_mosers_worm_problem_lower_bound :
    0.232239 ∈ lowerBounds {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} := by
…
```
Mentions: MoserWorm.WormCovers