Improved area limits for shapes covering all unit-length arcs
Improved bounds for universal convex covers of unit arcs
Computational Geometry
Summary
Imagine trying to find the smallest flat shape that can hold every possible curve of length one. The authors improved the known range for the smallest such convex shape's size, making the estimates much closer. They proved the shape must be at least 0.239 square units in area and found one with 0.24633 square units that works. Their proof involved checking specific simple shapes and using a computer to verify the details.
What this means in practice
- •For computational geometers: Use the improved area bounds to refine algorithms for minimal universal covers of planar shapes.
- •For software verification engineers: Employ the formal proofs in Lean 4 as examples of verified geometric reasoning to enhance correctness in critical software.
Authors
Ethan Keller
Abstract
Moser's worm problem asks for a planar region of least area containing a congruent copy of every unit arc. We show that the infimum area $α$ among convex universal covers satisfies $0.239\leα\le0.24633\ldots$, reducing the gap between the previous refereed bounds by over $75\%$. For the lower bound, we choose four unit polygonal arcs and prove by finite subdivision that, however they are placed, their convex hull has area at least $0.239$. For the upper bound, we construct a quadrilateral of area $0.24633\ldots$ and prove cover universality by showing that its support inequalities force uncovered arcs to have length greater than one. The full proof is formalized in Lean 4 and verified by the Lean kernel. Code and certificates are available at https://github.com/ethan-keller/moser-worm-improved-bounds.