Viewing profile — 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…

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 tha…

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 act…

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 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…

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.) T…

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 th…

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 …

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…

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 imp…

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 h…

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) …

To my knowledge, this is the first formally verified implementation of a 3D constructive solid geometry (CSG) operation: mesh intersection, implemented in Lean 4 and verified again…

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…

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 experime…

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…

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…

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 ha…

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,…

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 repro…

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 lo…

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 w…