Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean

Every version keeps its own PDF, citation, and review record — endorsements are bound to the version they examined and never carry forward silently.