10월 15일, Lean 프로젝트의 설계자 Leonardo de Moura가 글 하나를 공개했습니다. 제목은 "Lean Now Ships with Verified Kernels". Lean v4.35.0부터 증명을 독립적인 커널 여러 개로 다시 검사하는 기능이 들어왔다는 내용입니다.
왜 갑자기 이런 기능이 필요해졌을까요. 글의 첫 문장이 답을 줍니다. "AI 에이전트는 우리 소프트웨어의 취약점을 찾는 데 매우 능하다. 여기에는 Lean 증명 보조기의 커널(증명 검사기)도 포함된다."
즉 AI가 증명을 잘 만들어내는 것과 별개로, AI가 검사기 자체의 버그를 잘 찾아낸다는 것입니다. 그러면 질문이 뒤집힙니다. AI가 만든 증명을, 어떤 검사기로 검사할 것인가.
문제의 배경
Lean에서 커널은 최후의 심판입니다. 커널이 "이 증명은 유효하다"고 승인하면, 그 결론은 수학적으로 참입니다. 그래서 커널에 버그가 있으면, 잘못된 증명이 통과합니다. 무결성(soundness) 문제입니다.
[Lean의 신뢰 구조]
사용자가 쓴 증명
↓
커널(증명 검사기) ← 여기에 버그가 있으면 잘못된 증명도 통과
↓
"정리(theorem)가 참이다"
문제: 커널 자체가 소프트웨어다. 버그가 있을 수 있다.
그리고 그 버그를 잘 찾는 것이 AI 에이전트다.
de Moura는 최근 두 건의 커널 무결성 버그 사후 분석(postmortem, 8월 1일과 8월 24일)을 언급합니다. 그리고 이렇게 대응했습니다.
무엇이 추가됐나
v4.35.0의 핵심은 lake check입니다.
[lake check]
- 프로젝트를 내보내고, leanchecker(군더더기를 걷어낸
공식 Lean 커널)로 다시 검사한다
- 전체 과정이 샌드박스 안에서 실행된다
- lake check --inadvisably-no-sandbox 로 샌드박스를 끌 수 있다
(이름부터 "권하지 않음"이 붙어 있다)
[lake check --paranoid]
- Lean에 함께 배포되는 모든 커널로 다시 검사한다
- 추가로, 메모리 오염을 조용한 오답 대신
'검사된 중단(checked abort)'으로 바꾸는
강화된 메모리 할당자로 빌드한 공식 커널 변형도 돌린다
배포에 포함된 추가 커널은 네 개입니다. nanoda, lean4lean, con-leche, con-ron. 이 중 두 개가 이 글의 흥미로운 부분입니다.
Claude가 구현하고, 수학적으로 증명한 커널
가장 인상적인 항목은 con-leche입니다. 설명을 그대로 옮기면 이렇습니다.
con-leche
- Lean을 위해 Lean으로 작성된 첫 커널
- '일관성(consistency)'이 증명된 커널
- Claude(Fable과 Opus)가 구현하고 일관성을 증명했다
- Lean FRO의 Joachim Breitner가 강하게 감독했다
'일관성'의 의미:
con-leche가 승인하는 모든 환경이
집합론 안에 모델을 가진다
(Mario Carneiro의 Lean 타입 이론 모델을 따름)
성능: 전체 Mathlib 내보내기에서
공식 커널의 0.69배 명령어 수
8스레드로 전체 라이브러리를 약 100초에 검사
이게 왜 중요한가. con-leche는 커널 구현상의 프로그래밍 실수라는, 버그의 한 종류 전체를 제거합니다. 왜냐하면 "이 커널이 승인한 것은 모델이 존재한다"는 사실을 수학적으로 증명했기 때문입니다. 그리고 성능 패널티가 없습니다. 공식 커널보다 오히려 0.69배 명령어로 돕니다.
컴파일러까지 의심하기: con-ron
그런데 con-leche도 완벽하지는 않습니다. con-leche를 빌드한 컴파일러와 런타임에 버그가 있을 수 있습니다. 그래서 다음 단계가 나옵니다.
con-ron
- Joachim이 AI를 이용해 con-leche를 Rust로 번역했다
- Aeneas(Rust 코드를 Lean으로 검증하는 도구)로
"Rust 버전이 con-leche의 검사 알고리즘을 개선(refine)한다"를 증명했다
핵심 논리:
- con-leche에는 형식적 일관성 증명이 있다
→ 남은 무결성 버그는 대부분 Lean 컴파일러·런타임
(bignum 라이브러리 포함)에 있을 것이다
- 같은 버그가 Rust 컴파일러·런타임에도 동시에 있을 확률은 낮다
- 따라서 con-leche와 con-ron으로 함께 검사하면
이 부류의 버그에 대해 높은 수준의 보호를 얻는다
즉 "증명 → 커널"뿐 아니라 "커널 → 그걸 빌드한 도구"까지 신뢰 사슬을 한 단계 늘린 것입니다. lean4lean의 검증도 몇 달 안에 끝날 예정이라, 그러면 배포에 검증된 커널이 세 개가 됩니다.
전: 그래도 남는 위험과 확장 문제
균형을 잡아야 할 지점들입니다.
[완전히 제거되지 않은 위험]
- con-leche도 만능이 아니다. 컴파일러·런타임 버그 가능성은 남는다
(그래서 con-ron을 함께 쓴다)
- 다중 커널 검사가 모든 오류 가능성을 없애지는 않는다
- 'paranoid' 모드는 자원을 더 쓴다
[확장성 문제]
- Anthropic FLT : 1,300만 LoC 초과
- Mathlib : 250만 LoC
- Tau Ceti : 300만 LoC 초과, 빠르게 증가
- General Courtade-Kumar: 5,000만 LoC 초과
- 커뮤니티는 10억 LoC 규모 수학 라이브러리 제안도 논의 중
→ 현재의 외부 커널 방식은 이 규모로 확장되지 않는다
→ 이진 내보내기 형식과 증분 검사가 필요하다
de Moura는 남은 과제도 솔직하게 나열합니다. lake check를 더 쓰기 좋게 만들기, 사용자가 원하는 커널을 훅으로 연결하기(Lean Kernel Arena에 새 커널들이 있다), 컴파일러의 일부를 검증하기, 그리고 위의 확장성 문제입니다.
결론: 독립 검증을 습관으로
브리핑의 액션을 실험으로 옮기면 이렇습니다.
[Lean 프로젝트에서 두 명령을 비교해 보기]
1. 기본 검사
[ ] lake check
→ 공식 커널(leanchecker)로 샌드박스 안에서 재검사
2. 다중 커널 검사
[ ] lake check --paranoid
→ 배포된 모든 커널 + 강화 메모리 할당자 변형으로 재검사
3. 비교할 것
[ ] 검사 시간과 자원 사용량
[ ] 커널 간 결론이 갈리는 증명이 있는가
[ ] 갈리면 Lean FRO에 알린다 ([email protected])
4. 팀 규칙으로 정한다
[ ] 중요한 증명은 PR에 --paranoid 결과를 붙인다
[ ] 일반 증명은 기본 검사로 비용을 낮춘다
핵심 문장은 이렇습니다.
AI가 만든 결과를 그대로 믿는 대신,
서로 다른 독립 경로로 다시 검사한다.
이 원리는 수학 증명에만 국한되지 않습니다. AI가 코드를 쓰고, 문서를 쓰고, 결정을 내리는 모든 곳에서 같은 질문이 남습니다. "이 결과를 무엇으로, 몇 개의 독립된 경로로 검증할 것인가." Lean 4.35는 그 질문에 대해 가장 엄격한 분야의 답을 보여줍니다. AI가 검증 도구의 버그까지 찾아내는 시대에는, 검증 자체도 다중화해야 한다는 것입니다.
함께 읽으면 좋은 글
참고 자료
- Lean Now Ships with Verified Kernels (Leonardo de Moura, Oct 15, 2026)
- Lean v4.35.0 릴리스
- con-leche: Lean으로 작성·증명된 커널
- Lean Kernel Arena
이 주제를 직접 따라가며 배우고 싶다면
"AI의 결과를 독립적으로 검증한다"는 태도는 판단과 결정의 문제입니다. 자동화된 판단 위에 사람이 언제 개입할지, 어떻게 검증할지를 설계하는 감각은 Decision AI와 Human-in-the-Loop를 다뤄 볼 때 구체화됩니다.