Lean4 인증서를 믿기 전에 구현과 실행 환경을 살펴야 한다

앤스로픽은 페르마의 마지막 정리(FLT) 증명 인증서를 검사할 때, 신뢰하지 않는 증명 코드와 신뢰하는 정리문을 격리하는 샌드박스를 끄고 비교 도구를 실행했다. 이 글은 Lean4의 논리적 일관성을 뒷받침하는 공개 증명이 아직 없고, 공식 커널의 버그와 안전하지 않은 실행 설정도 우려할 만하다고 주장한다.

Lean4를 어디까지 믿을 수 있나

Lean4는 수학적 명제와 증명을 작성하고, 정해진 공리와 규칙에 따라 증명이 유효한지 검사하는 형식 증명 도구다. 증명서 검사를 수학 문제의 풀이를 확인하는 채점기에 빗대면 쉽다. 다만 채점기 자체의 규칙과 구현에 결함이 있으면 틀린 풀이를 통과시킬 수 있다.

이 글의 주장은 Lean4 인증서에 대한 철학적 신뢰 논의만으로는 충분하지 않다는 것이다. Lean4가 아직 초기 단계인 소프트웨어이고, 실제로 버그가 있으며, 공식 커널의 일관성도 증명되지 않았으므로 무엇을 믿을지 구체적으로 따져야 한다고 주장한다. Lean4 인증서를 쓰거나 검토하는 수학·소프트웨어 팀이라면 증명 결과뿐 아니라 검사기와 실행 환경도 확인할 필요가 있다는 취지다.

글쓴이는 사실관계 설명 대부분이 맞다고 보지만, 그중 최대 두 가지는 틀렸을 가능성이 있다고 자신의 인식 상태를 제시한다. 현재 GitHub의 Lean4 버전에는 True=False라는 명제를 받아들이게 만드는 증명이 있을 가능성이 90%라고 본다. 그런 증명이 발견되면 Lean 커뮤니티가 패치가 필요한 버그로 여길 유형이라고 설명한다. 반면 앞으로 정렬되지 않은 AI가 만든 Lean4 인증서에 사회가 막대한 신뢰를 둘 것이고, 향후 24개월 동안 커뮤니티가 Lean4를 고치는 일이 Less Wrong이 말하는 중대한 결정적 행동에 해당할 가능성은 2%라고 적었다.

일관성 증명은 왜 중요한가

수학의 표준적 공리 체계로는 선택 공리를 포함한 체르멜로-프렝켈 집합론(ZFC)이 있다. 글은 이 공리들이 많은 수학자에게 검토됐고 일관성이 있다고 상당히 확신할 수 있다고 설명한다. 그러나 Lean4는 ZFC를 기반으로 하지 않는다. 컴파일 속도를 높이는 설계 원칙 아래 여러 현대 유형 이론의 요소를 조합한 자체 의존 유형 이론을 사용한다.

이 글에 따르면, ZFC나 대형 기수 공리 같은 표준 체계가 일관적이면 Lean4도 일관적이라는 설득력 있는 증명을 만드는 것이 바람직하다. 하지만 현재 Lean4가 ZFC와 어떤 대형 기수 공리를 더한 체계에 대해 일관적이라는 공개 증명은 없다. 글쓴이는 이를 단순히 증명 작성을 미뤄 둔 기술적 문제로 보지 않는다. Lean4가 왜 일관적이어야 하는지에 대한 이해 자체가 부족하고, 알려진 증명 전략에도 실질적인 장애물이 있다고 평가한다.

새로운 수학 기초 체계에서 모순이 발견된 전례도 있다. 의존 유형 이론의 선구자인 마르틴뢰프(Martin-Löf)가 1971년 제안한 유형 이론은 이듬해 지라르(Girard)가 모순을 찾아냈다. 마르틴뢰프는 수정 논문에서 공리 하나를 버려야 한다고 결론 내렸으며, 그 수정이 이론의 표현력을 크게 낮췄다고 설명했다. 람다 계산으로 수학 기초를 세우려던 처치(Church)의 1932년 제안도 클리니(Kleene)와 로서(Rosser)가 모순을 보였고, 1940년 콰인(Quine)이 제안한 ZFC의 재구성 역시 로서가 모순을 찾아냈다.

Lean4의 빠른 컴파일을 가능하게 하는 설계 요소는 강한 재귀 능력과도 맞닿아 있다. 의존 유형 이론의 일관성을 ZFC와 대형 기수 공리에 비춰 보이는 대표적 방법 중 하나는 정규화 성질을 이용하는 것이다. 하지만 아벨(Abel)과 코캉(Coqand)은 2019년 Lean과 비슷한 유형 이론에서는 이 성질이 성립하지 않는다고 증명했다. 글쓴이는 이를 Lean4 유형 이론의 동작이 복잡하고 예측하기 어렵다는 징후로 본다.

마리오 카르네이루(Mario Carneiro)는 2019년 Lean3의 일관성 증명을 제안했다. Lean3의 기본 개념을 집합론의 집합과 함수로 옮기고, Lean3의 공리가 집합에 관한 참인 명제에 대응함을 보이는 방식이었다. 그러나 2024년에 그 증명 전략에 결함이 있다는 점이 드러났고, 올바른 증명에는 새로운 접근이 필요하다는 결과가 나왔다. Lean3의 집합론적 표현을 고치더라도 Lean4에는 상당한 확장이 필요한 새 기능이 추가됐다는 것이 글의 지적이다.

또 다른 접근인 con-leche 프로젝트는 Lean4의 일부 성질을 포착하는 집합론적 표현을 제안한다. Lean3 증명에서 사용한 비교적 온건한 대형 기수 공리 ZFC_omega와 달리, con-leche는 임의로 길게 중첩되는 그로텐디크 우주를 사용한다. 글쓴이는 이를 강한 가정이라고 평가한다. 글쓴이는 GPT-6 Astra에 Lean4를 집합론으로 표현해 달라고 요청했고, 모델은 약 25시간과 수천 달러를 썼지만 성공하지 못했다고 한다. 여러 표현 방법을 시도했지만 Lean4의 강한 재귀 능력 때문에 반례가 계속 나왔다는 설명이다. 이는 집합론적 표현을 찾는 일이 쉽지 않고, Lean4의 일관성을 뒷받침하는 큰 그림도 아직 없다는 글쓴이의 판단 근거다.

재귀 기능과 커널 버그는 무엇이 문제인가

중첩 귀납 유형은 자기 유형에 관한 고차 성질을 이용해 유형을 정의하는 방식이다. 글은 이것이 Lean4의 논리적 복잡성을 높이는 주요 요소이며, 연구와 이해가 아직 초기 단계라고 설명한다. 2026년에 나온 연구 두 편에서 일부 진전이 있었지만, 인용된 논문은 Rocq와 Lean 모두 중첩 귀납 유형을 충분히 지원하지 못한다고 지적한다. 두 시스템은 사용 가능한 소거 원리를 만들지 못하고, 서로 다른 종류의 중첩 귀납 유형을 받아들이는데 어느 쪽도 만족스럽지 않다는 내용이다. 논문은 Lean의 구현에서 내부 표현이 새어 나오는 문제와, 이론상 유효하고 고급 명세에 필요한 정의를 거부하는 문제도 언급한다.

글쓴이는 문헌을 바탕으로, Lean4의 유형 이론이 큰 틀에서는 일관적이더라도 중첩 귀납 유형의 재귀 동작이 예상보다 복잡할 수 있다고 본다. 그 복잡성은 모순을 일으키거나, 모순까지는 아니더라도 버그를 만들 정도로 예측하기 어려울 수 있다는 주장이다. 크리스 베일리(Chris Bailey)가 이를 앞서 말한 ‘바다 괴물’이라고 표현했다는 설명도 덧붙인다. 무엇을 찾아야 하는지에 대한 상위 수준의 설명이나 명세가 없어 체계적으로 버그를 찾기 어렵다는 것이 글쓴이의 우려다.

Lean의 제작자 레오 데 모우라(Leo de Moura)는 2026년 4월 글에 이어 3개월 뒤 커널의 건전성 버그 14576번을 다룬 사후 분석을 게시했다. 이후 Lean FRO는 커널에서 버그를 7개 더 찾았다. 데 모우라는 거짓 명제가 Lean에 받아들여지는 일이 계속 일어날 것이며, AI는 커널의 건전성 버그를 악용하는 데 능하다고 말했다. 해당 버그에 대한 Lean 개발자 포럼의 토론도 소개됐다. 글은 이 사례들을 Lean4 커널에 버그가 없다고 가정해서는 안 되는 이유로 든다.

con-leche는 공식 커널의 문제를 해결하나

con-leche는 Lean4로 작성한 형식 검증 커널을 제안한 프로젝트다. 앞선 시도인 lean4lean도 있으며, 글이 쓰인 시점에는 개발 중이었다. con-leche 제작자 요아힘 브라이트너(Joachim Breitner)는 con-leche가 lean4lean과 다른 설계 지점을 택했다고 설명한다. 주석, 추가 검사, 생성된 귀납 모델 등을 도입해 검사기 구현에 제약을 두는 대신, 어려운 메타이론적 성질을 증명하지 않고도 모델을 통해 일관성을 직접 증명하려는 방식이다.

글쓴이는 con-leche가 공식 Lean4 C++ 커널의 일관성을 주장하는 것은 아니라고 지적한다. con-leche는 자체 커널을 구성하고, 그 커널이 일관적이라고 주장한다. 두 커널은 중첩 귀납 유형을 다르게 처리하며 공식 Lean4 커널이 받아들이고 con-leche가 거부하는 명제도 있다. 글쓴이가 Astra를 이용해 con-leche의 증명을 공식 C++ 커널의 일관성 증명으로 옮기려 했지만, 증명 변환이 실제로 실패했다고 한다. 글쓴이의 설명에 따르면 con-leche의 변경은 ‘바다 괴물’을 피하기 위한 것이므로, con-leche에서 집합론적 표현이 작동한다고 해서 공식 Lean4의 관련 문제가 해결되지는 않는다.

또한 con-leche의 일관성을 con-leche 자체로 증명하면 순환 논증이 된다. 이를 피하려면 con-leche 안에 표현된 집합론 모델만 사용해야 하지만, 그 모델이 주변의 모순 가능성이 있는 이론에 의해 오염되지 않았는지도 주의해야 한다. 글쓴이는 con-leche가 커널을 하나 더 제공한다는 점은 긍정적으로 보면서도, 이 프로젝트가 ‘바다 괴물’ 문제를 해결하거나 공식 커널의 버그 가능성을 배제하지는 않는다고 결론 내린다.

인증서를 실행할 때는 무엇을 확인해야 하나

앤스로픽의 페르마의 마지막 정리 인증서를 실행하는 데 드는 계산 비용을 글은 비교 대상으로 언급한다. 여기서 비교 도구는 증명 본문의 악성 코드가 정리문의 내용을 정교화·컴파일 과정에서 바꾸지 못하게 점검하는 별도 도구다. 커널을 전적으로 신뢰하더라도 이런 위험은 남으며, 비교 도구 실행에는 오랜 시간이 걸린다고 설명한다. 형식 검증을 중요 소프트웨어 인프라 전반에 적용하는 일이 큰 비용이 드는 프로젝트라면, 기본 Lean4 실행과 비교 도구를 함께 실행하는 선택의 비용 차이가 도입 가능성을 좌우할 수 있다는 것이 글쓴이의 주장이다.

글은 개발자가 선택할 수 있는 안전 조치로 con-leche와 nanoda에서 코드를 실행하는 방법, 비교 도구 사용, 캐시된 .olean 파일을 샌드박스에 두는 방법을 든다. 이런 방식은 Lean4의 기본 동작이 아니므로 개발자가 따로 선택해야 한다. 적절한 선택은 사용하는 분야와 Lean4 및 에이전트 집단을 얼마나 신뢰하는지에 따라 달라진다고 설명한다.

앤스로픽의 저장소에는 비교 도구를 실행하면서 샌드박스를 끈 이유가 주석으로 적혀 있다.

“Comparator의 자체 scripts/fake-landrun.sh를 사용한다 = 샌드박스 없음. 기록된 실행도 이 방식으로 했다. 직접 트리를 만들었으므로 신뢰하지 않는 풀이를 막는 샌드박스는 불필요하다.”

글쓴이는 이를 앤스로픽이 페르마의 마지막 정리 증명을 작성한 에이전트 집단을 신뢰해 악성 코드 방어를 불필요하다고 판단한 사례로 본다. 다른 사람이 해당 인증서를 근거로 자기 인증서도 같은 엄격함을 거쳤다고 주장할 수 있으므로, 더 높은 검증 기준이 필요하다는 주장이다. 각주에는 글쓴이가 같은 인증서에 샌드박스를 켜고 비교 도구를 실행했을 때 검사가 통과했다고 적혀 있다. 케빈 버자드(Kevin Buzzard)도 인증서를 독립적으로 확인하고 여러 실사를 했으며, 글쓴이는 커뮤니티의 실제 검증 수준이 앤스로픽 저장소의 실행보다 높았다고 덧붙인다.

앞으로 확인할 것은 무엇인가

글쓴이는 문제들이 일시적이거나 고칠 수 있다고 본다. Lean4가 일관적이라는 전제 아래 기초를 이해하고 증명할 수 있어야 하며, 그 이해를 바탕으로 커널을 체계적으로 검사할 수 있다는 전망이다. 또 신뢰하지 않는 증명이 신뢰하는 정리문을 바꾸지 못한다는 형식 검증된 명세를 마련하고, 기본 설정부터 강한 샌드박싱을 적용해야 한다고 주장한다.

다만 글쓴이는 보안 문제를 고치는 과정에 누구나 참여할 수 있는 것은 아니라고 말한다. 자신의 경험으로는 Astra가 Lean4의 안전성을 다루는 질문에 사이버 보안 문제라는 이유로 응답을 거부했다. Lean4의 일관성을 증명해 달라는 요청에는 응했지만, Lean4가 일관적이지 않을 가능성을 진지하게 검토해 달라고 하자 대화가 중단됐다고 한다. 앤스로픽 인증서의 로그를 살펴 이상 여부를 확인해 달라는 요청도 같은 이유로 분류됐다고 적었다. 이는 글쓴이의 경험에 관한 설명이며, AI 서비스 전반의 동작을 독립적으로 확인한 결과로 제시되지는 않는다.

글쓴이는 Lean4의 정확성을 진지하게 다뤄야 한다고 AI 연구소에 요청하며, 현재 상태와 핵심 인프라에 신뢰를 둘 수준 사이에는 상당한 과제가 남아 있다고 주장한다. 인증서만으로 소프트웨어를 이해하는 일을 대신할 수 없다는 각주도 덧붙인다. Lean4의 일관성 증명 공개 여부, 커널 버그의 추가 발견과 수정, 기본 샌드박싱 설정, 인증서 검증 비용은 계속 확인할 사안이다. 글은 앤스로픽 인증서 실행 비용의 구체적인 수치와 비교 도구를 실행하는 데 걸린 시간을 제시하지 않으며, Lean4가 일관적이지 않다는 사실을 입증하지도 않는다.