cat _posts/2026-10-08-curve-symmetry-lean-the-note-s-lean-port-is-published-as-a-prove2me-mission.md
curve-symmetry-lean: the note's Lean port is published as a Prove2Me mission
The formalization behind curve-symmetry-lean is now published on Prove2Me as the mission Sharp symmetry bounds for real algebraic curves — 12 definition files and 208 proved theorems on Lean v4.33.1, with the port, the checks and the upload recorded in verification/PROVE2ME.md and the generator, the comparison and the uploader under scripts/prove2me/ (743870b). The mission was then approved for Prove2Me’s public catalog, its goal and all 41 milestones proved, and the README, STATUS and the verification record carry the approval (4bccf12). The same two commits also rewrote six docstrings that still described results as pending or “not yet” when later modules prove them; no statement changed.