Lean 4 proves CSG correction with 93 lines of specification, ignoring AI code

A project on GitHub called ‘verified-3d-mesh-intersection’ presents the first formally verified implementation of a 3D constructive solid geometry (CSG) operation: mesh intersection. The code is written in Lean 4 and verified against a concise specification that precisely defines the surface of the resulting mesh and guarantees well-formed conditions in the triangulation.

According to the repository