Verified Polygon Intersection

A web-based tool for drawing and intersecting multipolygons with a formally verified core algorithm. The demo lets you create complex shapes with holes and self-intersections, then compute their intersections visually on a canvas. The underlying algorithm is proven correct in Lean, eliminating entire classes of bugs that plague traditional implementations.

This project demonstrates how modern AI agents can assist with formal verification. The creator used Claude to generate both the algorithm implementation and its mathematical proof simultaneously, a capability that previous models couldn't achieve. Trust in correctness comes from the Lean proof checker and human review, not from the AI itself.