수학계의 벤더 락인 논쟁 — 우리는 증명 도구 Lean에 갇힌 걸까

수학자들이 모이는 Q&A 사이트 MathOverflow에 흥미로운 질문이 하나 올라왔어요. 제목이 '우리는 Lean에 갇힌 걸까?(Are We Stuck with Lean?)'인데요. 요즘 수학계에서는 증명을 컴퓨터로 검증하는 '형식화' 작업이 빠르게 퍼지고 있는데, 그 도구가 사실상 Lean 하나로 쏠리고 있는 상황을 두고 나온 질문이에요. 개발자라면 어디서 많이 본 그림이죠? 특정 기술에 생태계가 쏠리고, 나중에 갈아타고 싶어도 못 갈아타는 상황이요. 그 '벤더 락인' 논쟁이 수학계에서 그대로 벌어지고 있는 거예요.

정리 증명기, 이게 뭐냐면요

정리 증명기(proof assistant)는 수학 증명을 코드처럼 작성하면 컴퓨터가 논리적 빈틈이 없는지 한 줄 한 줄 검증해주는 프로그램이에요. 컴파일러가 타입 에러를 잡아주듯이, 증명의 비약이나 오류를 기계가 잡아주는 거죠. 사람이 논문을 리뷰하다 놓치는 미묘한 오류도 기계는 안 놓쳐요. 이 분야에는 오래된 도구들이 여럿 있어요. Coq(최근 Rocq로 이름을 바꿨어요), Isabelle, Agda 같은 것들이요. Lean은 이 중에서 비교적 후발주자인데, 지난 몇 년 사이 수학 형식화 분야를 사실상 평정했어요.

Lean은 어쩌다 대세가 됐나

핵심은 mathlib이라는 라이브러리예요. 전 세계 수학자와 개발자들이 학부 수학부터 최신 연구 수준까지의 정리 수십만 개를 Lean 코드로 쌓아 올린 거대한 공유 라이브러리인데요. 새로운 정리를 형식화하려면 그 밑에 깔리는 기초 정리들이 미리 다 준비돼 있어야 하거든요. mathlib이 있으면 바로 시작할 수 있지만, 다른 시스템에서는 바닥부터 쌓아야 해요. npm에 패키지가 쌓일수록 Node.js를 떠나기 어려워지는 것과 정확히 같은 네트워크 효과예요. 여기에 유명 수학자 케빈 버자드가 페르마의 마지막 정리를 Lean으로 형식화하는 대형 프로젝트를 이끌고 있고, AI 연구 진영도 가세했어요. 구글 딥마인드의 AlphaProof가 국제수학올림피아드 문제를 풀 때 쓴 언어가 바로 Lean이거든요. LLM이 만들어낸 증명이 맞는지 기계적으로 채점해줄 도구가 필요한데, Lean이 그 표준 자리를 차지한 거예요.

'갇혔다'는 걱정의 정체

그런데 이 쏠림이 마냥 좋기만 한 건 아니라는 게 질문의 요지예요. 우선 Lean은 언어 표준과 구현체가 사실상 하나예요. C++처럼 표준 문서가 있고 컴파일러가 여러 개인 구조가 아니라, 특정 구현이 곧 언어인 거죠. 더 근본적인 문제는 기반 이론이에요. Lean은 '의존 타입 이론'이라는 논리 체계 위에 서 있는데, Isabelle 같은 도구는 다른 체계를 써요. 이게 뭐냐면, 단순히 문법이 다른 게 아니라 증명이라는 건물의 기초 공사 방식 자체가 달라서, 한 시스템의 증명을 다른 시스템으로 자동 변환하는 게 굉장히 어렵다는 뜻이에요. 프로그래밍 언어를 갈아타는 건 로직을 다시 쓰면 되지만, 이건 수십만 개의 정리를 사람 손으로 다시 증명해야 할 수도 있는 수준의 이전 비용이거든요. 수학은 백 년 뒤에도 유효해야 하는 학문인데, 특정 소프트웨어에 이렇게 깊이 의존해도 되느냐는 거죠.

개발자 세계와 똑 닮은 구조

사실 이 고민은 소프트웨어 업계가 늘 하던 고민이에요. 형식 검증은 이미 실무에서도 쓰이고 있어요. 운영체제 커널 seL4는 Isabelle로, C 컴파일러 CompCert는 Coq로 검증됐고, AWS도 핵심 인프라 설계에 형식 기법을 써요. 그리고 AI가 코드를 쏟아내는 시대일수록 이런 도구의 가치는 올라가요. 사람이 다 리뷰할 수 없는 양의 산출물을 기계가 수학적으로 검증하는 구조가 유일한 출구일 수 있거든요. 그 미래의 기반 기술이 지금 어느 생태계에 쌓이느냐가 결정되고 있는 셈이에요.

배워둘 가치가 있을까

Lean 4는 순수한 증명 도구를 넘어 그 자체로 꽤 잘 만든 함수형 프로그래밍 언어이기도 해요. 실무에 바로 쓸 일은 없더라도, 타입 시스템이 얼마나 강력해질 수 있는지 감각을 키우는 데는 이만한 교재가 없어요. 주말에 Lean 입문용 웹 게임인 'Natural Number Game'을 한번 해보시면, 증명이 곧 프로그래밍이라는 말이 무슨 뜻인지 몸으로 느껴질 거예요.

정리하면, 수학계는 지금 Lean이라는 단일 생태계에 미래 자산을 쌓을지 말지를 두고 개발자들이 늘 하던 락인 고민을 하고 있어요. 여러분은 기술을 고를 때 '나중에 갈아탈 수 있는가'를 얼마나 따지시나요? 락인을 감수하고라도 생태계가 큰 쪽에 올라타는 게 맞을까요?