ProofAtlas research outcome
Moser's Convex Worm Mixed-Area Lower Bound
The paper, exact Lean statements, checked evidence, and immutable source release are collected on the canonical formalization page.
Result boundary
Every compact convex cover universal for finite polygonal worms or for all unit worms has area strictly greater than 0.23743658226923856768, both with direct motions and when reflections are allowed.
The exact optimum remains open, and independent acceptance review is not complete.