First Formally Verified Polygon Intersection
A developer named schildep has published what they claim is the first formally verified implementation of a multipolygon intersection algorithm. The project uses the Lean 4 proof assistant to guarantee that the intersection of two multipolygons is computed correctly for all possible inputs.
The Verification Stack
The core specification lives in three files totaling just 87 lines of Lean code: DataStructures.lean, Defs.lean, and MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean. A human reviewer only needs to read these files and run the Lean checker to verify correctness. The actual algorithm implementation and its proof are in separate ...Proofs.lean and ...Impl.lean files, which were written entirely by AI agents and never human-reviewed.
To check the proofs, run:
printf 'import Polygons.MultipolygonIntersectionAlgorithmWithPreconditionCheck\n#print axioms multipolygonIntersectionAlgorithmWithPreconditionCheck_interior_eq\n#print axioms multipolygonIntersectionAlgorithmWithPreconditionCheck_complete\n' | lake env lean --stdin
This outputs the axioms used. Currently, only propext, Classical.choice, and Quot.sound are relied upon — no unwanted axioms were introduced.
Why Formal Verification Matters Here
Multipolygon intersection is notoriously hard to test exhaustively. There are infinitely many input configurations, and the interior set of a polygon is infinite. Classical testing can't cover all edge cases. For example, intersecting a cross with a square containing a hole can yield multiple valid boundary decompositions (four squares vs. a cross with a square hole). A tiny shift in the hole makes the result unique. The algorithm must handle these degenerate cases correctly.
Formal verification in Lean proves the intersection equality for every possible configuration, not just a test suite. The proof that the definition of "inside" (parity of ray intersections) is independent of ray direction took thousands of lines of Lean.
AI Agent Evolution: Opus 4.8 Delivers
The developer's experience with AI agents evolved dramatically across Claude Opus versions:
- Opus 4.5/4.6: Could translate perfectly rigorous human-written proofs into Lean, but couldn't design proof strategies independently.
- Opus 4.7: Could take larger steps, proving existence of intersections for any two polygons, but still needed human hints for Eulerian circuits and special cases.
- Opus 4.8: In ultracode mode, it reproved the main polygon intersection theorem from scratch with no hints, and independently extended the algorithm to handle overlapping segments — a case where Opus 4.7 had failed. Both tasks succeeded after a few hours of autonomous work.
A key observation: Opus 4.8 handled risky intermediate theorems better. When previous models got stuck on an incorrect helper theorem, Opus 4.8 became suspicious, pivoted to a different strategy, or ran parallel subagents to try multiple approaches.
Practical Considerations and Next Steps
The developer notes a drawback: forcing AI agents to produce formally verified code tends to yield slower, less optimized implementations. The specification doesn't capture performance requirements, so the AI optimizes for proof simplicity over speed. The current code is unoptimized and will grow significantly when optimizations are added.
Next steps include:
- Measure and improve performance
- Simplify proofs that take unnecessary detours (the developer notes many detours exist that could be avoided, based on a parallel experiment)
- Add SVG import/export
- Build a WebAssembly bundle for the web demo (requires emscripten, zstd, wasm-opt)
Related Work
Di Vito and Hocking (NASA Formal Methods 2021) verified a polygon merge algorithm in PVS, but that only combined two overlapping simple polygons into a single outer boundary without holes. This new work handles general multipolygons with holes and computes the actual intersection set.
How to Try It
A web demo is available (linked from the GitHub repo) where you can draw and intersect multipolygons. The verified core runs in WebAssembly.
Why It Matters
Formal verification is gaining traction in critical software, but the cost of writing proofs remains high. This project demonstrates that AI agents can now autonomously produce complex formal proofs, potentially lowering the barrier. For developers working on geometry algorithms, rendering engines, or any domain where correctness is paramount, this approach could become a practical tool.
Editor's Take
I've been following formal verification for years, and the biggest hurdle has always been the human effort to write proofs. Seeing Opus 4.8 autonomously handle Eulerian circuits and degenerate polygon cases is genuinely impressive. That said, I'm skeptical about the generalizability — polygon intersection is a well-defined, self-contained problem. Real-world codebases have messy dependencies and changing requirements. Still, this is a concrete milestone: an AI wrote a non-trivial verified algorithm that a human can trust by reading 87 lines of spec. That's a workflow I'd like to see replicated for other algorithms.
