HN Showcase
Back to browse
GitHub Repository

Formally verified polygon intersection

42 starsLean

Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

by permute·May 30, 2026·2 points·0 comments
Visit ProjectView on HN

AI Analysis

●●●BangerWizardryBig BrainNiche Gem

First formally verified polygon intersection with Lean 4 proof and web demo.

Strengths
  • •Lean 4 verification guarantees correctness across infinite input configurations, not just test cases.
  • •Handles edge cases like holes, self-intersections, and overlapping edges with mathematical proof.
  • •Web demo makes the verified core accessible without needing Lean expertise.
Weaknesses
  • •Extending or verifying proofs requires Lean 4 expertise, limiting contributor pool.
  • •No performance benchmarks compared to unverified libraries like GEOS or CGAL.
Category
Open Source
Target Audience

Computational geometry developers, GIS tool builders, formal verification enthusiasts

Similar To

CGAL · GEOS · JTS Topology Suite

Post Description

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.

It supports multipolygons including holes, self intersections, and overlapping edges.

Similar Projects