1. FormalConjectures
  2. Wikipedia
  3. MoserWorm
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Moser's Worm

Reference: Wikipedia

open EuclideanGeometry MeasureTheory namespace MoserWorm

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 ℝ².

def Worms : Set (Set ℝ²) := {s | ∃ f : (Set.Icc (0 : ℝ) (1 : ℝ)) → ℝ², LipschitzWith 1 f ∧ Set.range f = s}

The set of covers is the set of (measurable) sets that cover every worm by translation and rotation.

def WormCovers : Set (Set ℝ²) := {X | MeasurableSet X ∧ ∀ w ∈ Worms, ∃ (e : ℝ² ≃ₗᵢ[ℝ] ℝ²) (v : ℝ²), e.toLinearEquiv.det = 1 ∧ w ⊆ (fun x => e x + v) '' X}

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.

@[category textbook, AMS 52] theorem disc_mem_worm_covers : Metric.closedBall 0 0.5 ∈ WormCovers := ⊢ Metric.closedBall 0 0.5 ∈ WormCovers ⊢ ∀ w ∈ Worms, ∃ e v, LinearEquiv.det e.toLinearEquiv = 1 ∧ w ⊆ (fun x => e x + v) '' Metric.closedBall 0 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 f⊢ ∃ e v, LinearEquiv.det e.toLinearEquiv = 1 ∧ Set.range f ⊆ (fun x => e x + v) '' Metric.closedBall 0 0.5 refine ⟨LinearIsometryEquiv.refl ℝ _, f ⟨1/2, f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 f⊢ 1 / 2 ∈ Set.Icc 0 1 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 f⊢ 0 ≤ 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 f⊢ 1 / 2 ≤ 1 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 f⊢ 0 ≤ 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 f⊢ 1 / 2 ≤ 1 All goals completed! 🐙⟩, LinearEquiv.det_refl .., ?_⟩ f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ f t ∈ (fun x => (LinearIsometryEquiv.refl ℝ ℝ²) x + f ⟨1 / 2, ⋯⟩) '' Metric.closedBall 0 0.5 refine ⟨f t - f ⟨1/2, f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 1 / 2 ∈ Set.Icc 0 1 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 0 ≤ 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 1 / 2 ≤ 1 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 0 ≤ 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 1 / 2 ≤ 1 All goals completed! 🐙⟩, ?_, f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ (fun x => (LinearIsometryEquiv.refl ℝ ℝ²) x + f ⟨1 / 2, ⋯⟩) (f t - f ⟨1 / 2, ⋯⟩) = f t All goals completed! 🐙⟩ f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ ‖f t - f ⟨1 / 2, ⋯⟩‖ ≤ 0.5 have h := hf.dist_le_mul t ⟨1/2, f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 1 / 2 ∈ Set.Icc 0 1 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 0 ≤ 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 1 / 2 ≤ 1 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 0 ≤ 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)⊢ 1 / 2 ≤ 1 All goals completed! 🐙⟩ f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)h:dist (f t) (f ⟨1 / 2, ⋯⟩) ≤ dist t ⟨1 / 2, ⋯⟩⊢ ‖f t - f ⟨1 / 2, ⋯⟩‖ ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)h:‖f t - f ⟨1 / 2, ⋯⟩‖ ≤ dist t ⟨1 / 2, ⋯⟩⊢ ‖f t - f ⟨1 / 2, ⋯⟩‖ ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:↑(Set.Icc 0 1)h:‖f t - f ⟨1 / 2, ⋯⟩‖ ≤ dist t ⟨1 / 2, ⋯⟩⊢ dist t ⟨1 / 2, ⋯⟩ ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩ ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ |t - 1 / 2| ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ -0.5 ≤ t - 1 / 2 ∧ t - 1 / 2 ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ -0.5 ≤ t - 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ t - 1 / 2 ≤ 0.5 f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ -0.5 ≤ t - 1 / 2f:↑(Set.Icc 0 1) → ℝ²hf:LipschitzWith 1 ft:ℝht1:0 ≤ tht2:t ≤ 1h:‖f ⟨t, ⋯⟩ - f ⟨1 / 2, ⋯⟩‖ ≤ dist ⟨t, ⋯⟩ ⟨1 / 2, ⋯⟩⊢ t - 1 / 2 ≤ 0.5 All goals completed! 🐙

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?

@[category research open, AMS 52] theorem declaration uses 'sorry'mosers_worm_problem : IsGLB {v | ∃ X ∈ WormCovers, volume X = v} answer(sorry) := ⊢ IsGLB {v | ∃ X ∈ WormCovers, volume X = v} sorry All goals completed! 🐙

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.

@[category research solved, AMS 52] theorem declaration uses 'sorry'mosers_worm_problem_upper_bound : ∃ X ∈ WormCovers, volume X = 0.260437 := ⊢ ∃ X ∈ WormCovers, volume X = 0.260437 All goals completed! 🐙

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?

@[category research open, AMS 52] theorem declaration uses 'sorry'convex_mosers_worm_problem : IsGLB {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} answer(sorry) := ⊢ IsGLB {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} sorry All goals completed! 🐙

The minimal area of a convex shape that can cover every unit-length curve is attained. This follows from the Blaschke selection theorem.

@[category research solved, AMS 52] theorem declaration uses 'sorry'convex_mosers_worm_problem_bound_attained : ∃ bound, IsLeast {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} bound := ⊢ ∃ bound, IsLeast {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} bound All goals completed! 🐙

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.

@[category research solved, AMS 52] theorem declaration uses 'sorry'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 := ⊢ ∃ X, MeasurableSet X ∧ Convex ℝ X ∧ volume X = 0.270911861 ∧ ∀ w ∈ Worms, ∃ e v, LinearEquiv.det e.toLinearEquiv = 1 ∧ w ⊆ (fun x => e x + v) '' X All goals completed! 🐙

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.

@[category research solved, AMS 52] theorem declaration uses 'sorry'convex_mosers_worm_problem_lower_bound : 0.232239 ∈ lowerBounds {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} := ⊢ 0.232239 ∈ lowerBounds {v | ∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = v} All goals completed! 🐙 end MoserWorm