verified-3d-mesh-intersection

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