First Formally Verified 3D CSG Mesh Intersection Implemented in Lean 4

Formally Verified 3D CSG Operation

A new implementation of 3D constructive solid geometry (CSG) mesh intersection has been created using Lean 4. This marks the first formally verified implementation of such an operation, ensuring its correctness against a precise specification. The verification process guarantees the resulting mesh's surface and practical well-formedness conditions on the triangulation.

Trusting Specifications Over AI Code

This project serves as an experiment in validating AI-generated code by focusing on a concise, human-readable specification. Human reviewers only need to examine a 93-line formal specification and run the Lean checker to certify the kernel's correctness. The AI autonomously generated over 1,000 lines of implementation code and more than 60,000 lines of Lean proofs, which do not require human inspection. The Lean checker ensures conformance to the specification at compile time, eliminating the need to trust the LLM directly.

Performance Considerations

The current implementation is slower than existing state-of-the-art mesh intersection methods, taking 24 seconds to compute the intersection of two 70,000-triangle Stanford bunnies. The project prioritizes minimizing human review effort for correctness over computational performance. The developers note that this performance gap is not an inherent limitation of formally verified software, which can achieve speeds comparable to conventional software.

Web Demo and Guarantees

A web demo is available, allowing users to intersect example meshes or import and intersect meshes from STL files. The compiled Lean code runs locally in the browser, ensuring no data is sent to a server. While the core kernel is formally verified, the user interface and glue code are not. The output meshes are guaranteed to satisfy specified properties, though the meshing might be suboptimal in terms of criteria not yet formalized, potentially producing finer meshes than necessary.