Formally verified 3D mesh intersection in Lean, trusted by 93‑line spec
This repo implements a 3D CSG mesh intersection in Lean 4, with a 93‑line formal specification that’s fully verified, while the underlying 1,000+ lines of AI‑generated code are never inspected. It shows correctness can be guaranteed without human code review, though it runs slower—24 seconds for two 70k‑triangle Stanford bunnies.