Show HN: Formally verified polygon intersection, Opus 4.8 one-shot

This Show HN points to a GitHub project called verified-polygon-intersection, on the theme of using Lean 4 to formally verify a multi-polygon intersection algorithm. Polygon intersection is a basic function common in vector graphics, CAD, geographic information systems, and graphics editors, but computational geometry often has a large number of boundary conditions—such as overlapping line segments, holes, multiple closed boundary components, and special intersection configurations—that traditional testing struggles to exhaust across all input cases. The author's approach is to write the requirement that "the intersection of the interior sets of two input multi-polygons must equal the interior set of the output multi-polygon" as a formal specification, and to have Lean 4 check the proof, so that correctness does not depend on test cases or on what the LLM says, but on the proof checker.