HN Debrief

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

  • AI
  • Programming
  • Developer Tools

The project is a formally verified polygon intersection library written in Lean, with a WebAssembly demo around the verified core. It works on exact rational coordinates, not floating point, and the proof target is simple to state but strong in effect: the interior of the result equals the intersection of the interiors of the input polygons. The submitter framed the interesting part as the workflow, not the geometry itself. Polygon clipping is old news. What changed is that a newer model could generate both implementation and proof from the formal specification in one long run, while earlier models only worked when the task was broken into smaller guided steps.

If you are evaluating AI for nontrivial engineering work, the useful pattern here is "LLM generates, proof checker decides" for domains that have compact formal specs. That does not remove integration work, but it can sharply reduce review burden on the most failure-prone logic.

Discussion mood

Strongly positive and impressed. The excitement came less from polygon intersection itself and more from seeing Lean used on a practical algorithm, with AI producing proof-carrying code and exact arithmetic avoiding the usual computational geometry disasters.

Key insights

  1. 01

    Proof generation took hours, not prompts

    Getting from a formal spec to a verified implementation was an autonomous run that took about eight hours on Opus 4.8. That cost is the trade. You spend far more model time producing proof artifacts, but you buy down human review on the logic that usually hides the worst bugs. The submitter anchors this with older formal methods work that needed hundreds of manually written lemmas for related polygon problems.

    Treat this as a batch pipeline, not an interactive coding assistant workflow. The main budget line is now compute and proof search time, so use it where post hoc review and bug fallout are more expensive than long agent runs.

      Attribution:
    • permute #1 #2
  2. 02

    Real-number proofs are easier than real-number programs

    The hard boundary is representation, not the mathematics. The submitter says the existing proof should extend with minimal changes from rationals to any ordered field, but executable software still needs a concrete exact representation. That makes symbolic support for selected irrational values plausible, while "all real numbers" is impossible to represent exactly. The same framing points toward spline geometry as a more interesting extension because exact intersections quickly leave the rationals.

    Separate mathematical generality from deployable implementation when you scope verified systems. A proof that lifts cleanly to richer number systems does not mean your runtime can support those values without a new representation layer.

      Attribution:
    • permute #1
  3. 03

    The verified boundary stops at the UI

    The browser demo is not a toy wrapper around screenshots. The WebAssembly geometry engine is compiled from Lean, and the JavaScript layer passes exact rationals into it. That narrows the review surface to the formal spec and the UI glue instead of the clipping logic itself, which is where rare degeneracies usually live.

    When you pitch or adopt formally verified components, define the proof envelope precisely. You can get real value even if only the core kernel is verified, as long as the unverified edges are small and easy to audit.

      Attribution:
    • permute #1 #2
  4. 04

    Verified floating-point geometry still lacks key tooling

    Several comments land on the same practical gap. Lean can verify geometry over rationals or abstract reals, but there is not yet an obvious Lean equivalent of Rocq plus Flocq for production-grade IEEE floating-point reasoning. On top of that, robust computational geometry often depends on techniques like Shewchuk predicates to keep orientation and intersection tests consistent under floating point. Without formalized versions of those tools, verified geometry will keep gravitating toward exact arithmetic even when it is slower.

    If your roadmap needs verified numeric code that must interoperate with standard floats, watch the library ecosystem as closely as the models. The blocker may be missing formal infrastructure, not missing AI capability.

      Attribution:
    • porcoda #1
    • permute #1
    • threatripper #1

Against the grain

  1. 01

    The geometry itself is not novel

    Polygon intersection has been standard in graphics and GIS for decades, so the submission can look like old wine in a new bottle if you focus on the algorithm alone. That skepticism is useful because it forces the right reading of the project. The novelty is the proof-carrying implementation and the AI-assisted workflow, not a new clipping method.

    Judge efforts like this by where they move the reliability or development-cost frontier, not by whether the base algorithm is already well known. If you cannot state the proof boundary and workflow gain clearly, the project will sound less interesting than it is.

      Attribution:
    • simon84 #1

In plain english

Flocq ↩
A formal library for reasoning about floating-point arithmetic in Rocq.
formally verified ↩
Shown correct with a mathematical proof that is checked by software rather than only tested with examples.
GIS ↩
Geographic information systems, software used to store, analyze, and manipulate spatial and map data.
IEEE floating point ↩
The standard computer representation for approximate real numbers such as 32-bit and 64-bit floats.
Lean ↩
A proof assistant programming language and software system used to write mathematical statements and have proofs checked by a computer.
ordered field ↩
A number system with addition, subtraction, multiplication, and division where values can also be compared with less-than and greater-than in a way that behaves normally.
Rocq ↩
The new name for the Coq proof assistant, a system for writing and checking formal proofs.
Shewchuk predicates ↩
A family of robust computational geometry tests, such as orientation and incircle checks, designed to stay reliable despite floating-point error.
WebAssembly ↩
A compact binary format that lets code run at near-native speed inside a web browser.

Reference links

Project links