AI가 쓴 6만 줄 증명, 사람은 93줄만 읽습니다 — 코드 리뷰가 스펙 리뷰로 바뀌는 순간

핵심 요약 (TL;DR)

AI 에이전트가 구현 코드 1,000줄 이상과 Lean 4 수학 증명 60,000줄 이상을 작성하고, 사람은 93줄짜리 형식 스펙만 검토하는 3D 메시 교차 라이브러리가 Hacker News에 공개됐습니다. 스펙만 올바르면 Lean 증명 검사기가 컴파일 타임에 "구현이 스펙을 지킨다"를 기계적으로 보장하는 구조입니다. AI 코드에 대한 신뢰를 사람의 리뷰가 아니라 수학적 증명에 맡기는 접근인 거죠.

AI에게 코딩을 맡겨본 분이라면 한 번쯤 마주치는 순간이 있습니다. 에이전트가 하루 만에 쏟아낸 수천 줄 앞에서 "이걸 언제 다 읽지"라는 막막함 말입니다. 코드를 생산하는 속도는 수십 배가 됐는데, 검토하는 속도는 여전히 사람의 눈에 묶여 있습니다. 바이브코딩의 진짜 병목은 작성이 아니라 리뷰인 겁니다.

7월 28일 Hacker News에 올라온 한 프로젝트는 이 병목을 정면으로 겨냥했습니다.

AI가 쓴 6만 줄을 93줄만 읽고 믿을 수 있나요?

HN 유저 permute가 공개한 verified-3d-mesh-intersection은 형식 검증된 3D CSG 메시 교차 라이브러리입니다. AI 에이전트(README에 Claude Opus 4.8과 Fable 5 사용이 명시돼 있습니다)가 구현 1,000줄 이상과 Lean 4 증명 60,000줄 이상을 작성했고, 사람이 검토하는 건 93줄짜리 형식 스펙뿐입니다.

원리는 이렇습니다. 93줄 스펙에 "이 함수는 이런 성질을 만족해야 한다"를 수학적으로 적어두면, Lean 4 검사기가 컴파일 타임에 6만 줄의 증명이 그 스펙을 실제로 만족하는지 확인합니다. 증명이 틀리면 컴파일 자체가 실패합니다. 작성자는 이를 "LLM에 대한 신뢰는 0(zero trust placed in any LLM)"이라고 표현합니다. AI를 믿는 게 아니라, AI가 통과해야 하는 검문소를 믿는 거예요. 부동소수점 오차를 피하려 정확한 유리수 연산을 택한 것도 같은 결의 설계입니다. 게시 하루 만에 103포인트, 댓글 44개(7월 28일 게시 기준)를 기록했습니다.

그럼 코드 리뷰는 사라지는 건가요?

사라진 게 아니라 이동했다고 봐야 합니다. "1,000줄의 코드를 읽는 일"이 "93줄의 스펙이 올바른지 따지는 일"로 바뀐 거죠. 건물 완공 검사에서 벽돌을 하나하나 두드리는 대신, 설계 도면과 구조 계산서를 확인하는 방식으로 옮겨간 셈입니다.

다만 부풀려 읽으면 곤란한 지점이 셋 있습니다. 첫째, "자율 작성"에는 조건이 붙습니다. README에는 작성자가 마일스톤 단위로 에이전트를 가이드했다고 적혀 있습니다. 둘째, 형식 검증 범위는 코어 커널에 한정됩니다. 웹 데모의 글루 코드는 검증 대상이 아니었고, 실제로 그 부분에서 오버플로 버그가 발견돼 수정됐습니다. 검증된 커널 바깥은 여전히 평범한 코드라는 뜻이죠. 셋째, HN 댓글에서도 나온 반론처럼 "그 93줄 스펙이 올바르다는 건 누가 보장하나"라는 문제가 남습니다. 신뢰가 사라진 게 아니라, 더 작은 표면으로 압축된 겁니다.

FAQ

Q. 형식 검증은 아무 프로젝트에나 쓸 수 있나요?
기하 연산, 암호, 컴파일러처럼 "올바름"을 수학적으로 정의할 수 있는 영역에 적합합니다. UI나 비즈니스 로직처럼 스펙 자체가 모호한 영역은 아직 어렵습니다.

Q. Lean 4를 몰라도 이 흐름이 저와 관련이 있나요?
직접 증명을 쓸 일은 없어도 "AI 산출물의 검증을 어떻게 자동화할 것인가"라는 질문은 테스트, 타입 시스템, CI 설계에 이미 걸쳐 있는 문제입니다. 스펙(무엇이 맞는가)을 사람이 쥐고, 확인(맞는지 검사)을 기계에 넘기는 방향은 동일합니다.

Q. 이 프로젝트는 믿을 만한 사례인가요?
리포지토리와 스펙·증명 라인 수가 공개돼 있어 직접 확인할 수 있습니다. 다만 스타 65개 수준의 초기 프로젝트라는 점은 감안해야 합니다.

AI 코드가 쌓일수록 질문은 하나로 수렴합니다. 여러분은 지금 무엇을 근거로 AI의 결과물을 믿고 있나요. 사람의 눈, 테스트 커버리지, 수학적 증명 — 여러분의 검문소는 어디에 세워져 있나요?