Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
Formal VerificationLean 4Constructive Solid GeometryMesh IntersectionVerified CodeAI-Autonomous ProofsProof AssistantsVerified Implementation.
Author: permute
Date: 7/28/2026
Article Summary:
A project implements a 3D constructive solid geometry (CSG) operation in Lean 4, providing a formally verified mesh intersection kernel with a concise specification and automated proof generation.