형식적으로 검증된 3D CSG 메쉬 교차: AI 코드가 아닌 93줄의 명세를 신뢰하세요

새로운 프로젝트 verified-3d-mesh-intersection은 Lean 4로 공식 검증된 3D CSG(구성적 고체 기하학) 메시 교차를 구현합니다. 핵심 아이디어: 1000줄이 넘는 AI 작성 구현 코드 대신 93줄의 공식 명세만 신뢰하는 것입니다. AI가 6만 줄이 넘는 Lean 증명을 자동으로 작성했으며, 이는 인간의 검토가 전혀 필요 없습니다. Lean 검사기가 컴파일 타임에 정확성을 보장합니다.

작동 방식

명세는 결과 메시의 정확한 표면을 정의하고 삼각분할의 적정 조건을 보장합니다. 핵등식:

solid (meshIntersect M1 M2) = solid M1 ∩ solid M2

여기서 solid는 메시 내부의 무한한 점 집합을 나타냅니다. Lean은 이러한 무한 집합을 추론하고 등식을 정확히 증명할 수 있습니다.

주요 세부사항

• 언어: Lean 4, emcc-wasm.sh를 통해 WebAssembly로 컴파일됨.
• 성능: 7만 삼각형의 스탠포드 토끼 메시 두 개를 교차하는 데 24초 소요. 느리지만 검증을 속도보다 우선시합니다.
• 웹 데모: 브라우저에서 검증된 커널을 실행합니다: schildep.github.io/verified-3d-mesh-intersection. STL 가져오기 지원. 서버로 데이터 전송 없음.
• 인간 검토: 93줄의 명세만 읽으면 됩니다. 1000줄 이상의 AI 구현과 6만 줄 이상의 AI 증명은 블랙박스로 취급됩니다.
• 적정성: 입력이 적절하지 않은 경우(예: 닫히지 않았거나 자기 교차하는 경우), 알고리즘이 이를 감지하고 올바르게 보고해야 합니다. 이는 명세에 공식화되어 있습니다.

대상 사용자

3D 기하학, CSG 연산 또는 공식 검증을 다루는 개발자, 특히 보장 없이 AI 생성 코드를 신뢰하는 것에 회의적인 분들.

아키텍처

저장소에는 Lean 커널(CSG/), C 래퍼(wrapper.c), 웹 글루 코드(web/)가 포함됩니다. 빌드 명령은 lakefile.lean, emcc-wasm.sh, build_web_demo.sh를 통해 제공됩니다. UI와 글루 코드는 공식 검증되지 않았습니다.