Moser's worm problem asks for the minimum area of a planar region containing a congruent copy of every unit arc. The infimum area among convex universal covers is unknown, so work focuses on bounding it.

For the lower bound, four polygonal unit arcs are chosen and finite subdivision proves their joint convex hull always has area at least 0.239. For the upper bound, a rational quadrilateral is constructed and support inequalities are combined via a finite certificate to force any uncovered arc to have length greater than one. Search programs produce rational certificates exported to Lean declarations, with finite numerical checks proved by decide plus the kernel. Formal soundness theorems establish that certificate acceptance implies the geometric bounds.

The infimum area alpha satisfies 0.239 <= alpha <= 0.24633..., reducing the gap between previous refereed bounds by over 75%. Both bounds are verified by the Lean kernel without native_decide.