HN Explorer

Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed (github.com)

93 points by permute ↗ HN
To my knowledge, this is the first formally verified implementation of an intersection algorithm for polygons.

The experience of working with AI agents on this project changed a lot with recent model releases, as I describe in the readme. Opus 4.8 is able to provide algorithm implementation with formal proof in one shot, whereas previous models required me to provide proof strategies in multiple steps.

Trust in the correctness comes entirely from the Lean checker and human review of a small specification, not from the LLM.

Also check out the web demo built around the verified core linked in the readme: https://schildep.github.io/verified-polygon-intersection/. It supports multipolygons including holes, self intersections, and overlapping edges.

9 comments

[ 3.3 ms ] story [ 30.7 ms ] thread
CyLith
Does this use integer coordinates or floating point coordinates?
olaird25
Is the web demo compiled from the lean?
prewett
This is a great use for AI! Calculating intersections is tedious and there are an surprising number of edge cases that are tedious to track down and fix.
deterministic
Impressive work. It's nice to see LEAN being used for real-world algorithms.
simon84
I'm not sure if the feature is intersection or the use of AI to write it...

Polygon intersection is a well known thing. Video games and geographic information systems (topology) do that for decades.

Tell me more, what should I look at ?

Someone
How hard would it be to extend this proof to real coordinates? Is that ‘just’ a matter of formalizing some known, tedious math, or would it require new work?

For example, if one allows one coordinate of one corner to be non rational, I think the set of potential output coordinates used would be a subset of the reals (depending on the value of that coordinate), and to my (possibly very bad) intuition, formalizing that subset doesn’t feel like a hard problem.

Allowing two of such real points would make things more tedious, potentially way more tedious, but again, doesn’t feel like it would be impossible to handle.