Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed
37 points by permute
by deterministic
0 subcomment
Impressive work. It's nice to see LEAN being used for real-world algorithms.
by CyLith
2 subcomments
Does this use integer coordinates or floating point coordinates?
by prewett
0 subcomment
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.
Hacker News