Formally verified 3D mesh intersection - trust 93 lines of spec, not 1000+ lines AI-written code
Summary
The project presents the first formally verified implementation of a 3D mesh intersection (CSG) in Lean 4, verified against a concise 93-line specification. It argues that correctness can be achieved with minimal human review by relying on formal proofs generated by AI and checked by Lean, treating the implementation as a black box. A web demo runs locally in the browser, with performance noted as slower than state-of-the-art but emphasizing correctness over speed, and the article discusses well-formedness, special cases, and tradeoffs between formal verification and AI-driven code.