Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed • Hacker News Board

Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#1

Post by permute » Thu, Jun 04, 2026, 10:06 PM UTC

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.

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

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#2

Post by CyLith » Thu, Jun 04, 2026, 10:17 PM UTC

Does this use integer coordinates or floating point coordinates?

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#3

Post by [deleted] » Thu, Jun 04, 2026, 10:27 PM UTC

CyLith wrote: post #2

Does this use integer coordinates or floating point coordinates?

[deleted]

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#4

Post by threatripper » Thu, Jun 04, 2026, 10:36 PM UTC

CyLith wrote: post #2

Does this use integer coordinates or floating point coordinates?

It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#5

Post by huflungdung » Thu, Jun 04, 2026, 10:41 PM UTC

[dead]

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#6

Post by olaird25 » Thu, Jun 04, 2026, 10:58 PM UTC

Is the web demo compiled from the lean?

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#7

Post by prewett » Thu, Jun 04, 2026, 11:30 PM UTC

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.

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#8

Post by porcoda » Thu, Jun 04, 2026, 11:35 PM UTC

threatripper wrote: post #4

CyLith wrote: post #2

Does this use integer coordinates or floating point coordinates?

It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...

I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#9

Post by deterministic » Fri, Jun 05, 2026, 3:38 AM UTC

Impressive work. It's nice to see LEAN being used for real-world algorithms.

Re: Show HN: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

#10

Post by permute » Fri, Jun 05, 2026, 8:18 AM UTC

threatripper wrote: post #4

CyLith wrote: post #2

Does this use integer coordinates or floating point coordinates?

It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...

Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.

I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.