형식적으로 검증된 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와 글루 코드는 공식 검증되지 않았습니다.
📖 전체 소스 보기: HN LLM Tools
👀 See Also
2,181개 원격 MCP 서버 엔드포인트 분석 결과 신뢰성 문제 발견
2,181개의 원격 MCP 서버 엔드포인트에 대한 자동화된 헬스 체크 결과, 9%만이 정상 작동하는 것으로 확인되었으며, 52%는 완전히 작동하지 않고 37%는 인증이 필요한 것으로 나타났습니다. 이 데이터에는 카테고리별 분석, 지연 시간 측정, 가동 시간 통계가 포함되어 있습니다.
RTX 5000 PRO 48GB, Qwen3.6-27B용 4400 tok/s 정밀 캐싱 제공
첫 PC 조립 사용자가 단일 RTX 5000 Pro 48GB에서 vLLM과 Claude Code를 사용하여 Qwen3.6-27B-FP8 전체 정밀도 KV 캐시로 프롬프트 처리 4400 tok/s, 생성 80 tok/s를 기록했습니다.
간편한 배포: Open Claw를 위한 새로운 원클릭 AWS 설정 출시
Open Claw 애호가들이 이제 기뻐할 이유가 생겼습니다. 새로운 원클릭 AWS 배포 도구가 Open Claw의 설정 과정을 단순화하여 개발자와 취미 개발자 모두에게 더욱 접근하기 쉬워졌습니다.
미국 법 집행 기관, AI 반발 속 '안티테크 극단주의'를 새로운 위협 범주로 지정
국토안보부, FBI 및 퓨전 센터가 '반기술 폭력 극단주의'라는 새로운 범주를 감시하고 있습니다. 이는 트럼프 행정부 지시에 따라 인공지능 관련 시위, 데이터 센터 위협 및 반대 의견을 표적으로 삼습니다.