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

Category: library

Tags: formal-verification, computational-geometry, lean, polygon-intersection, proof-assistant

Score: 7.5/10 (Innovation: 9, Technical: 9, Documentation: 7, Utility: 5)

This project provides the first formally verified implementation of a multipolygon intersection algorithm using the Lean 4 proof assistant. It is notable for leveraging LLM agents to generate the proof while maintaining trust through formal verification, and for including a web demo. The work tackles a notoriously difficult problem in computational geometry where traditional testing is insufficient.

Target audience: backend devs, data engineers, researchers

Repository: https://github.com/schildep/verified-polygon-intersection · Lean · MIT · 1 stars

View on Hacker News