Lean 4를 사용하여 3차원 구성 솔리드 기하학(CSG) 연산인 메시 교차에 대한 최초의 형식 검증 구현이 공개되었습니다. 이 구현은 간결한 명세에 따라 검증되었습니다. 이는 수학적 증명을 통해 해당 연산의 정확성을 보장합니다.