"그냥 Lean 쓰면 안 돼요?"라는 질문에 Isabelle 진영이 내놓은 진지한 대답

정리 증명기 세계의 작은 논쟁

수학을 컴퓨터로 증명하는 정리 증명기(theorem prover)라는 분야가 있어요. 종이와 연필로 쓰던 수학 증명을 형식 언어로 옮겨 적으면, 컴퓨터가 한 줄 한 줄 검증해서 "이 증명에 빈틈이 없다"는 걸 보장해주는 도구거든요. 이 분야에서 최근 몇 년 사이 Lean이라는 시스템이 폭발적으로 인기를 끌고 있어요. Terence Tao 같은 필즈상 수상자도 Lean으로 증명을 작성해 화제가 됐죠. 그런데 Isabelle이라는 더 오래된 시스템의 핵심 개발자 중 한 명인 Lawrence Paulson이 "왜 그냥 Lean을 쓰지 않냐"는 흔한 질문에 대해 정면으로 답한 글을 써서 흥미로운 논의가 이어지고 있어요.

정리 증명기 생태계의 지형

먼저 배경부터 정리하면, 정리 증명기는 크게 두 계열로 나뉘어요. 한 쪽은 Coq, Lean, Agda처럼 의존 타입 이론(Dependent Type Theory)에 기반한 시스템이고, 다른 한 쪽은 Isabelle/HOL이나 HOL Light처럼 고차 논리(Higher-Order Logic)에 기반한 시스템이에요.

이게 뭐냐면, 의존 타입 시스템은 "타입이 값에 의존할 수 있다"는 강력한 표현력을 가져요. 예를 들어 "길이가 n인 리스트"라는 타입을 만들 수 있어서, 컴파일러가 인덱스 범위 오류를 미리 잡아낼 수 있죠. 반면 고차 논리는 표현력이 조금 더 제한적이지만, 자동화가 더 강력하고 학습 곡선이 비교적 완만하다는 장점이 있어요.

Paulson이 말하는 Lean의 한계

Paulson 글의 요지는 "Lean이 멋진 시스템인 건 맞지만, Isabelle이 Lean으로 단순히 대체되기 어려운 이유들이 있다"는 거예요.

첫째, 자동화의 깊이예요. Isabelle은 sledgehammer라는 도구로 외부 SAT/SMT 솔버, 일급 정리 증명기를 호출해서 보조 정리(lemma)를 자동으로 찾아주는 기능이 매우 성숙해 있어요. Lean에도 비슷한 도구가 있지만 아직 Isabelle만큼의 성숙도는 아니라는 거죠. 수학자가 매일 쓰는 도구에서는 이 자동화 차이가 굉장히 큰 생산성 차이로 이어집니다.

둘째, 라이브러리의 성격이에요. mathlib(Lean의 수학 라이브러리)이 빠르게 성장하고 있긴 하지만, Isabelle의 Archive of Formal Proofs는 수십 년에 걸쳐 축적된 검증 자산이거든요. 분야가 다르고, 깊이가 달라요. 특히 컴퓨터 과학의 형식 검증 분야(컴파일러, OS 커널, 분산 알고리즘 등)는 Isabelle 진영의 자산이 압도적입니다.

셋째, 논리 토대의 단순함이에요. 의존 타입 이론은 표현력이 강한 만큼 메타이론(meta-theory)이 복잡해요. 시스템 자체의 정합성을 신뢰하기 위해서는 그 토대가 단단해야 하는데, HOL은 상대적으로 단순한 공리 위에 서있어서 검증이 쉽다는 주장이에요.

업계 맥락과 흐름

객관적으로 보면 흐름은 Lean 쪽으로 기울고 있어요. 수학자 커뮤니티의 채택률, GitHub 활동성, AI와의 결합(LLM이 Lean 코드를 생성하는 연구가 활발해요) 모두 Lean이 앞서고 있습니다. DeepMind의 AlphaProof, OpenAI의 정리 증명 연구도 주로 Lean을 타깃하고 있고요.

하지만 Paulson이 짚는 포인트는 "유행과 별개로 도구의 가치는 사용 목적에 따라 다르다"는 거예요. 새로운 분야의 수학을 형식화하고 싶다면 Lean의 활기찬 커뮤니티가 매력적이지만, 안전이 중요한 시스템의 형식 검증을 한다면 Isabelle이 여전히 더 견고한 선택일 수 있다는 거죠.

한국 개발자에게 주는 시사점

정리 증명기는 당장 한국 개발 현장에서 흔히 보이는 기술은 아니에요. 하지만 두 가지 맥락에서 알아둘 가치가 있어요. 첫째, AI와 형식 추론의 결합이 본격화되는 시점이라는 점이에요. LLM이 Lean 코드를 생성하고 검증기가 검증하는 식의 워크플로우는 "환각 없는 AI"의 한 방향이라 향후 5~10년의 큰 흐름이 될 가능성이 높거든요.

둘째, 도구 선택에 대한 일반론으로도 의미 있어요. "유행하는 도구 = 최선의 도구"가 아니라는 것, 그리고 도구를 평가할 때는 자동화 수준, 라이브러리 성숙도, 토대의 견고함 같은 다층적 기준을 봐야 한다는 것. 이건 정리 증명기뿐 아니라 프로그래밍 언어, 프레임워크 선택에도 그대로 적용됩니다.