verified-3d-mesh-intersection

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

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.

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

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

> Why we cannot have manifold output meshes in general As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs. I wonder how manifold will break in that condition or would it snap to the nearest manifold. https://github.com/schildep/verified-3d-mesh-intersection#wh...

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 against a concise specification that pins down the surface of the resulting mesh exactly and guarantees practical well-formedness conditions on the triangulation. This project is also an experiment in avoiding having to trust AI-generated code. A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human. The Lean checker guarantees conformance to the specification at compile time, with zero trust placed