Formally verified polygon intersection – Opus 4.8 oneshots, prev failed

Name: Formally verified polygon intersection – Opus 4.8 oneshots, prev failed
Availability: InStock
Author: permute

by permute·Jun 4, 2026·31 points·5 comments

Visit Project View on HN

AI Analysis

●●●BangerWizardryBig Brain

First formally verified polygon intersection—Lean 4 proofs guarantee correctness for all inputs.

Strengths

•Formal verification with Lean 4 guarantees correctness across infinite input configurations.
•Handles complex cases including holes, self-intersections, and overlapping edges correctly.
•Web demo makes the verified core accessible and testable without Lean expertise.

Weaknesses

•Lean 4 expertise required to verify or modify the proofs yourself.
•Niche audience limits broader adoption beyond computational geometry specialists.

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: https://schildep.github.io/verified-polygon-intersection/. It supports multipolygons including holes, self intersections, and overlapping edges.