Lean4의 증명 인증서를 신뢰해도 되는지 논의할 때는 형식 증명 전반에 관한 철학뿐 아니라 Lean4 자체의 한계도 살펴야 한다. 이 글은 Lean4의 커널 버그, 일관성 증명의 부재, 중첩 귀납 타입의 복잡성, 안전하지 않은 실행 설정을 근거로 신뢰 수준을 공개적으로 논의하자고 주장한다.

글쓴이는 사실 설명 대부분이 맞다고 보지만 최대 두 곳은 틀렸을 수 있다고 밝힌다. 또 현재 GitHub 버전의 Lean4가 “True=False”를 받아들이는 증명을 포함할 가능성을 90%로 추정한다. 다만 이는 커널이나 컴파일러 등의 버그로 인정돼 수정이 필요할 만한 경우라는 조건을 단다. 반면 24개월 안에 정렬되지 않은 AI가 만든 Lean4 인증서에 사회가 막대한 신뢰를 맡기게 될 가능성은 2%라고 평가한다.

일관성 증명과 커널 버그

글은 Lean4가 수학 명제와 증명을 검사하는 데 Zermelo-Fraenkel 집합론과 선택 공리(ZFC)를 쓰는 대신, 컴파일 속도를 고려해 설계한 종속 타입 이론을 기반으로 한다고 설명한다. 하지만 Lean4가 ZFC나 대형 기수 공리로 확장한 체계에 대해 일관적이라는 공개 증명은 없다고 지적한다. 글쓴이는 이를 단순히 증명이 아직 작성되지 않은 기술적 문제로 보지 않는다. 알려진 증명 전략에는 장애물이 있으며, Lean4가 왜 일관적이어야 하는지에 관한 큰 그림도 없다는 것이 그의 해석이다.

Lean의 창시자 Leo de Moura는 커널 건전성 버그 이후 글을 게시했고, Lean FRO는 커널에서 버그를 일곱 건 더 발견했다. de Moura는 “Lean이 거짓 명제를 받아들이는 일은 계속 일어날 것”이며 AI가 커널의 건전성 버그를 잘 악용한다고 말했다. 관련 글은 2026년 4월 글, 버그 #14576 사후 분석, 추가 커널 버그 조사 결과에서 확인할 수 있다. Lean 개발자 포럼에도 버그 관련 토론이 있다.

글은 종속 타입 이론의 역사에서도 설계 오류 가능성을 찾는다. Martin-Löf가 1971년에 제안한 타입 이론은 이듬해 Girard가 모순을 발견했고, Martin-Löf는 수정 논문에서 공리 하나를 포기해야 한다고 썼다. Church의 1932년 람다 계산 기반 수학 기초안도 Kleene과 Rosser가 모순을 보였으며, Quine의 1940년 ZFC 수정안은 Rosser가 모순을 밝혀냈다.

Lean4의 컴파일 속도에 기여하는 기능은 강력한 재귀 능력과도 연결된다. 종속 타입 이론의 일관성을 보이는 데 흔히 쓰이는 정규화 성질은 Lean과 같은 타입 이론에서는 성립하지 않는다는 결과가 2019년에 나왔다(논문). 글쓴이는 이 점이 Lean4의 타입 이론이 복잡하고 다루기 어렵다는 신호라고 본다.

Mario Carneiro는 2019년 Lean3의 원시 개념을 집합론에 대응시켜 일관성을 보이는 방식을 제안했다(제안 자료). 그러나 글에 따르면 2024년에 이 증명 전략의 결함이 드러났고, 올바른 증명에는 새 접근이 필요해졌다(관련 자료). Lean3의 대응을 고치더라도 Lean4의 새 기능을 반영하려면 추가 작업이 필요하다.

또 다른 프로젝트인 con-leche는 Lean4 일부 성질을 포착하는 집합론 모델을 제안한다. 글은 이 프로젝트가 ZFC_omega보다 강한 가정인, 임의로 길게 중첩된 Grothendieck 우주 계열을 사용한다고 설명한다. 글쓴이는 자신이 GPT-6 Astra에 Lean4를 집합론에 대응시키도록 요청했지만 약 25시간과 수천 달러를 들이고도 성공하지 못했다고 전한다. 이는 자신의 경험에 관한 보고이며, 독립적으로 확인된 결과로 제시되지는 않는다.

중첩 귀납 타입과 con-leche의 범위

글이 지목하는 복잡성의 한 원인은 중첩 귀납 타입이다. 이는 타입을 자기 타입의 고차원 성질을 이용해 정의하는 방식으로, 글은 이 분야의 이해가 아직 초기 단계라고 설명한다. 관련 연구로 2026년 논문과 이 논문을 든다. 인용된 연구는 Rocq와 Lean 모두 중첩 귀납 타입에 대한 지원이 충분하지 않아 사용 가능한 제거 원리를 만들지 못하고, 이론적으로 타당한 일부 정의를 거부한다고 지적한다.

글쓴이는 이런 특성이 일관성과 양립하지 않을 만큼 문제가 될 수도 있고, 일관적이더라도 버그를 일으킬 만큼 복잡할 수 있다고 주장한다. Chris Bailey가 ‘바다 괴물’이라고 부른 것도 일관성은 있으나 예측하기 어렵고 오류를 유발하는 이런 요소를 가리킨다는 설명이다. 무엇을 검사해야 하는지에 대한 고수준 명세가 없으므로 체계적인 버그 탐색도 어렵다는 것이 글의 주장이다.

최근 발표된 con-leche는 Lean4로 작성한 형식 검증 커널을 제시한다. 이는 개발 중인 lean4lean에 이은 두 번째 시도다. con-leche 제작자 Joachim Breitner는 lean4lean과 다른 설계 지점을 택해, 주석과 추가 검사, 생성된 귀납 모델을 사용하는 대신 어려운 메타이론적 성질을 증명하지 않고 모델 기반 일관성 증명을 직접 구성한다고 설명했다(lean4lean 저장소).

하지만 글은 con-leche가 공식 Lean4 C++ 커널의 일관성을 주장하는 것은 아니라고 강조한다. con-leche는 별도의 커널을 구성하며, 공식 Lean4와 중첩 귀납 타입을 다르게 처리한다. 공식 커널은 받아들이지만 con-leche는 거부하는 명제도 있다. 따라서 con-leche의 증명은 공식 커널의 문제를 해결하거나 공식 커널의 버그 가능성을 배제하지 않는다. 글은 con-leche의 모델 안에서 con-leche 자체의 일관성을 증명할 때 모델이 주변의 모순된 이론에 의해 오염되지 않았는지 주의해야 한다고 덧붙인다.

Lean4를 사용할 때의 안전 설정

글은 Anthropic의 페르마의 마지막 정리(FLT) 형식화에서 사용한 비교기(comparator)를 사례로 든다. 비교기는 증명 본문의 악성 코드가 명제문을 바꾸지 못하게 하는 보조 도구다. 이는 커널을 신뢰하더라도 고려해야 하는 문제이며, 실행 시간이 길다고 글은 설명한다. 글쓴이는 Lean4만 실행하는 것과 비교기까지 사용하는 것의 비용 차이가 중요 인프라의 형식 검증을 실행 가능한 일과 감당하기 어려운 일로 가를 수 있다고 주장한다.

개발자는 con-leche나 nanoda를 사용하거나, 비교기를 실행하거나, 캐시된 .olean 파일을 샌드박스에서 처리할 수 있다. 글에 따르면 이런 조치는 Lean4의 기본 설정이 아니며, 적절한 선택은 응용 분야와 Lean4 및 에이전트 집단을 얼마나 신뢰하는지에 따라 달라진다.

Anthropic의 FLT 형식화에서는 비교기를 실행하면서 신뢰할 수 없는 증명 코드와 신뢰 대상인 명제문을 분리하는 샌드박스를 비활성화했다. 저장소의 실행 스크립트 주석은 직접 트리를 만들었으므로 신뢰할 수 없는 해답에 대비한 샌드박스가 필요하지 않다는 취지로 설명한다. 글쓴이는 이것이 증명을 작성한 에이전트 집단을 신뢰한 결정으로 보인다며, FLT 인증서를 신뢰의 기준으로 삼으려면 더 높은 안전 기준이 필요하다고 주장한다.

다만 각주에서 글쓴이는 샌드박스를 켠 상태로 비교기를 실행해 FLT 인증서를 확인했고, Kevin Buzzard도 독립적으로 인증서를 검사하고 여러 실사를 했다고 덧붙인다. 그는 실제 커뮤니티의 검증 수준이 Anthropic 저장소의 설정만으로 보이는 것보다 높았다고 설명한다.

글쓴이가 제안하는 다음 단계

글쓴이는 Lean4의 문제들이 해결 가능할 수 있다고 본다. 일관적이라면 그 증명이 존재하고 발견할 수 있으며, 기초에 대한 이해를 바탕으로 커널을 체계적으로 검사할 수 있다는 주장이다. 신뢰할 수 없는 증명이 신뢰 대상인 명제문을 바꾸지 못하도록, 샌드박싱을 기본 설정에 포함하고 이를 보장하는 형식 명세를 마련해야 한다고도 제안한다.

그러나 글쓴이는 Lean4의 안전성 개선이 사이버 보안 작업으로 분류되면서 자신이 사용한 Astra가 관련 질문에 답변을 거부했다고 말한다. Lean4의 일관성을 증명해 달라는 요청에는 응했지만, 일관성이 없을 가능성을 진지하게 검토해 달라는 요청이나 Anthropic의 FLT 인증서 로그를 점검해 달라는 요청은 사이버 보안 관련으로 분류됐다는 설명이다. 이를 바탕으로 그는 프런티어 AI 연구소에 Lean4의 정확성을 진지하게 다뤄 달라고 촉구한다.

글의 결론은 Lean4가 아직 초기 단계이며, 정교한 AI 에이전트의 사이버 공격으로부터 핵심 인프라를 지탱할 것이라고 자신 있게 기대하기까지 중요한 과제가 남아 있다는 것이다. 글쓴이는 AI가 생성한 인증서가 소프트웨어를 신뢰하는 근거를 대신해서는 안 된다고 덧붙인다.

원문과 각주