permute

We could use floats internally and gain a lot of performance as I described in my response here: https://news.ycombinator.com/item?id=49085136. With this we would still be able to handle special cases correctly.

If you mean, you want float in the interface, I think the picture would be the similar as I described there: You still need to fallback to higher precision for certain computations. But you would also not be able to return the outputs correctly, so we would need to think about how we want to describe this in the specification...

The implementation of a function is in the CSG/Impl folder. A proof is in the CSG/Proof folder. They are both imported and tied together in the human reviewed file in a theorem that makes a mathematical statement about the function. Lean checks mechanically that the theorems are proven via the supplied proofs. Here you have to trust the Lean checker, but neither the proof nor the implementation.

Then you know that the statement in the file you reviewed holds about that function.

Regarding fuzzing. It cannot find the special cases I listed in the readme, because these cases are very rare.

Yet with formal verification we can prove that the implementation actually satisfies the specification for all of infinitely many possible inputs.

Good question!

One complication: For union the spec would look a little bit different than for intersection. I defined the solid associated to a mesh in a way that does not include the surface of the mesh itself. That works for the intersection. For union we would have:

solidWithSurface (meshUnion M₁ M₂) = solidWithSurface M₁ ∪ solidWithSurface M₂

I think it would not be hard to reduce the implementation and the proof of correctness to the intersection: There are some tricks which you can do like flipping the orientation of a mesh and putting a large cube that contains both meshes around it and then intersect these. (And then at the end doing the reverse trick.) Hopefully the implementation would not actually do this, but this construction could be used in the proof.

The implementations uses exact rationals numbers. So there are no issues with numerical errors. We can do all geometrical operations exactly.

Many performant implementations have a separate layer that tries to use floats to decide inequalities and fall back to higher precision when floats are not sufficient. As I understand, this layer can be separated from the geometrical predicates we need (what I mean by predicate is for example deciding which side of a plane a point is), so we could formalize that arithmetic layer separately using axioms on floating point numbers and then plug it in the existing code. I think we could do that and still provide exact outputs and prove the same spec we have right now and the performance should increase a lot, since most of the computations right now is computing all these predicates exactly.

I would not say numerical stability is the one enemy of CSG. See the special cases https://github.com/schildep/verified-3d-mesh-intersection#sp... and bugs in an alternative C++ implementation that also used exact rationals mentioned in https://github.com/schildep/verified-3d-mesh-intersection#co....

Also note that many implementations don’t even try to treat special geometrical cases correctly (for example they „cheat“ by using something called simulation of simplicity which provides some guarantees against some bugs, but at the expense of not treating the cases exactly correctly which can lead to artifacts).

I learned working with the Isabelle proof assistant in a university course. There were weekly exercises and a group project at the end. (Actually proving things by hand, no LLM.) That really helped. Before that course it was also hard for me to get into this.

Other than that you can also read introductory material for set theory. There the meaning of all of the unicode symbols you can see in the spec should be explained.

Both the implementation and the proof are written in Lean. In the files I reference here https://github.com/schildep/verified-3d-mesh-intersection#mi... there are theorems about the function that does the mesh intersection computation. The implementation is in the CSG/Impl folder. The proof is in the CSG/Proof folder. They are imported and tied together in the human reviewed file. Lean checks that these theorems in the human reviewed file are proven via the proofs.

I think this would need to be reimplemented for performance. But maybe the spec can be reused. As agents get better we might reimplement the same spec for performance with minimal human effort. (See notes regarding performance and floats in readme.)

It is possible to prove things involving floats, you just have to addionally trust a small set of axioms on floats. See https://github.com/schildep/verified-3d-mesh-intersection#pe... Don't know if there is something like this in Lean. But there is https://flocq.gitlabpages.inria.fr

Maybe what you mean is that kernels of proof assistants must be small. Here I am referring to a geometry processing kernel (that is formally verified by a proof assistant). The implementation of the algorithm can be very long, the proof that it conforms to the spec can be very long. But lean checks the proof. And so you only have to trust the spec and that the lean proof assistant is correct.

In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.

The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers: https://github.com/schildep/verified-3d-mesh-intersection#pe...

Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.

There are two things here: The proof and how you would represent that in a program that you actually can run.

From the math side, I am confident that the construction and proof can be extended to the real numbers and that can be formalized in lean with minimal changes in the existing proof. (Mathematically speaking, we can replace the rationals with any ordered field and the proof should run through.)

I chose to model the problem with rational numbers because the intersections of polygons with rational coordinates have rational coordinates and rational numbers can easily be represented in the computer.

To have a computable implementation with real numbers, you have to make some choice about which part of the real numbers you want to be able to represent in the computer. For example if sqrt(2) and sqrt(3) is important to you, I think you can have a program that can represent them if they occur in any input coordinates and can represent any resulting coordinates exactly symbolically besides the rational numbers (I think this requires minimal changes in the code, the required lean machinery to work with such numbers can be separated from the geometrical code), but a program can’t be able to represent all real numbers exactly since there are too many of them.

Another interesting direction to take this would be to allow spline segments instead of line segments, since intersections of splines with rational coordinates can have non rational coordinates, but I think can still be represented exactly in the computer. This would require a bigger change and would be interesting geometrically.

Yes, it runs significantly longer.

Opus 4.8 ran autonomously for about 8 hours to provide program and proof of correctness, given the formal specification. And in previous experiments, Opus 4.7 failed and I was only able to do it using that model when I cut the work for the agents in smaller steps.

Much of the work the agent is to provide the proof of correctness. The upside is that less time is needed for human review and we can guarantee the absence of bugs that might be expensive when they come up in production.

Historically formal verification was only worth it for very critical software. In the readme I reference related work from NASA, that implemented and verified a different algorithm concerned with polygons, with the intended application to compute keep out zones for autonomous vehicles. This was 2021 before capable LLMs and in the paper they mention that they manually wrote 700 lemmas to produce such a formal proof manually. I hope that as it gets cheaper now, formal verification is used more widely.

Sure, what the program does is not interesting by itself, neither is that you can use AI to create programs to do polygon intersection.

The main feature, that I hope is interesting in this submission, is that the program is formally verified and how I used formal verification together with AI to create it.

Formal verification means that a mathematical proof is provided that the program satisfies a specification. And that proof is checked automatically by a deterministic system, the lean checker, which we can trust, in constrast to error prone LLMs.

I gave the agent a formal specification m1.interior ∩ m2.interior = result.interior and it produced an implementation together with such a formal proof. With this approach we can treat much of the work of the agent as a black box, which we don't have to review to judge correctness.

I think the project shows that as AI agents get more capable, an approach like this is starting to get practical for certain problems like polygon intersection for which there is a concise way to specify the problem.

Yes

Thanks! Yes, I hope AI and Lean will enable formally verified practical software.

Thanks for the pointer, I will look into it.

I think to do efficient formally verified geometry with floating point we would also need something like Shewchuk robust predicates. (I worked with them in the past to write robust software that is not formally verified. Did not read up, if there is a formally verified library for them.) Shewchuk robust predicates give certain consistency guarantees that are nice to have when implementing computational geometry with floating points and I think can be formalized.

Thanks! I am currently working on a follow up project for 3D polyhedrons for which the case handling really starts to get tedious. It's nice when AI can handle it without humans having to read the code and many unit tests to trust it.

Yes, the webassembly is compiled from lean. The JS UI that calls the webassembly is not built from lean and not formally verified. So a human reviewer that does not trust the code, needs to review the formal spec and the UI code. But the geometry with rare special cases that we want to treat correctly happens in the verified core.

Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.

I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.

I am using Claude Code for formal verification with Lean. In my personal experience both Opus 4.7 and now what I see from first experiments with Opus 4.8 were big improvements. I was able to delegate proofs of larger theorems that their predecessors could not handle.

It’s fun to play around with this! It could be helpful to add support for parentheses and chaining of commands. For example: \add (\area-circle circ0) (\area-circle circ1). Intermediate nodes could be anonymous or automatically named.