Lean 4에서 꼭 배워야 할 10가지
출처: Dev.to
Lean 4가 중요한 이유
대부분의 프로그래머는 소프트웨어를 작동시키는 방법을 배우는 데 수년을 보냅니다.
반면에 소프트웨어가 증명적으로 올바른 방법을 배우는 사람은 극히 적습니다.
이 차이가 바로 컴파일러, 암호화 라이브러리, 커널, 형식 수학 등에서 Lean 4와 같은 증명 도우미에 점점 더 의존하게 되는 이유입니다.
Lean 4는 단순한 또 다른 프로그래밍 언어가 아닙니다. 프로그래밍, 수학, 정리 증명, 언어 설계가 교차하는 지점에 놓여 있습니다. 핵심 개념을 이해하면 소프트웨어를 단순히 기계에 대한 명령이 아니라 검증 가능한 논리 구조로 바라보게 됩니다.
그렇다면 Lean 4를 처음 접할 때 실제로 가장 중요한 것들은 무엇일까요?
이 가이드는 실질적인 활용도가 가장 높은 10가지 개념에 초점을 맞춥니다.
1. 함수 정의하기
Lean에서 모든 것은 함수로 시작합니다. Python이나 JavaScript와 달리 Lean은 입력, 출력, 타입을 매우 명시적으로 생각하도록 권장합니다.
def add (a b : Nat) : Nat :=
a + b주목할 점
Nat는 자연수를 의미합니다.- 함수 시그니처가 명시적입니다.
- 반환 타입도 정의의 일부입니다.
처음엔 다소 장황하게 느껴질 수 있지만, 엄청난 명료성을 제공합니다. 함수 정의에 익숙해지면 Lean의 나머지 부분이 훨씬 쉬워집니다.
2. 타입을 올바르게 이해하기
Lean에서는 타입이 모든 것의 중심입니다. 타입은 단순히 “정수”나 “문자열”이 아니라, 허용되는 값의 종류와 가능한 연산을 설명합니다.
#check Nat
#check String
#check List Nat#check 명령은 초보자에게 가장 유용한 도구 중 하나인데, Lean이 표현식을 어떻게 “보는지” 보여줍니다.
사고 방식 전환:
타입은 일종의 추론 도구입니다. 컴파일러는 끊임없이 논리적 일관성을 검사합니다.
3. 패턴 매칭
패턴 매칭은 Lean의 가장 우아한 기능 중 하나입니다.
def isZero : Nat → Bool
| 0 => true
| _ => false긴 조건문 체인을 쓰는 대신 입력 구조를 직접 기술합니다. 패턴 매칭은 특히 다음과 결합될 때 강력합니다.
- 재귀 데이터 구조
- 귀납 타입
- 증명
Haskell이나 OCaml 같은 함수형 언어에서 많이 사용되는 스타일입니다.
4. 재귀
Lean은 반복문보다 재귀를 선호합니다.
def factorial : Nat → Nat
| 0 => 1
| n + 1 => (n + 1) * factorial nLean은 종료와 정확성에 깊은 관심을 가집니다. 많은 언어와 달리 Lean은 재귀 함수가 결국 멈춘다는 증명을 요구합니다. 제약처럼 느껴질 수 있지만, 이는 전체적인 버그 클래스를 차단합니다.
5. 정리 다루기
여기서부터 Lean은 일반 프로그래밍 언어와 근본적으로 달라집니다. 수학적 진리를 직접 선언할 수 있습니다.
theorem add_zero (n : Nat) : n + 0 = n := by
rfl단순히 “테스트”하는 것이 아니라 증명하는 것입니다. 이는 소프트웨어 신뢰성을 바라보는 방식을 완전히 바꿉니다.
6. 전술(Tactics) 배우기
전술은 증명을 단계별로 구성하도록 돕는 명령어입니다.
theorem add_comm (a b : Nat) : a + b = b + a := by
induction a with
| zero =>
simp
| succ a ih =>
simp [ih]초보자에게 중요한 전술
simprwexactapplycasesinduction
처음엔 신비롭게 느껴질 수 있지만, 시간이 지나면 인터랙티브한 문제 해결 흐름이 됩니다.
7. 귀납 타입
귀납 타입은 Lean에서 가장 깊이 있는 아이디어 중 하나입니다. 기본 빌딩 블록으로 구조를 정의할 수 있게 해줍니다.
inductive Color where
| red
| green
| blue보다 복잡한 재귀 구조:
inductive Tree where
| leaf
| node (left right : Tree)이 개념들은 다음을 기반으로 합니다.
- 대수적 데이터 타입
- 재귀적 추론
- 귀납법에 의한 증명
귀납 타입을 이해하면 Lean의 많은 기능을 활용할 수 있습니다.
8. simp를 효과적으로 사용하기
초보자는 simp를 과소평가하기 쉽습니다. Lean에서 가장 생산적인 도구 중 하나입니다.
example (n : Nat) : n + 0 = n := by
simpsimp는 알려진 규칙을 이용해 목표를 자동으로 단순화합니다. 프로젝트가 커질수록 단순화 기술을 마스터하는 것이 증명을 관리 가능한 수준으로 유지하는 데 필수적입니다. 실제 Lean 전문가의 대부분은 단순화를 어떻게 제어하느냐에 달려 있습니다.
9. 오류 메시지 읽기
Lean의 오류 메시지는 다소 복잡할 수 있지만, 이를 해석하는 능력은 큰 자산입니다. 많은 초보자가 오류를 장애물로만 여기고 포기합니다. 보통 Lean은 다음 중 하나를 알려줍니다.
- 타입 불일치가 존재한다.
- 인수가 누락되었다.
- 증명 단계가 잘못되었다.
시간이 지나면 프로그래머가 코드를 디버깅하듯 증명을 디버깅하는 직관이 생깁니다. 이는 Lean이 가르쳐 주는 가장 전이 가능한 스킬 중 하나입니다.
10. Curry–Howard 대응 이해하기
위협적으로 들릴 수 있지만, 이것이 Lean 뒤에 숨은 핵심 철학적 통찰입니다.
핵심 아이디어
- 프로그램은 증명이다.
- 타입은 논리적 명제이다.
즉, 올바른 프로그램을 작성하는 것과 증명을 구성하는 것이 깊게 연결된 활동이라는 뜻입니다. 그래서 Lean은 일반 프로그래밍 언어와 다르게 느껴집니다. 단순히 명령을 실행하는 것이 아니라 논리적으로 검증된 구조를 만드는 것이죠. 이 개념이 “깨달아지면” Lean은 훨씬 직관적으로 다가옵니다.
정리: 정리 증명 그 이상의 의미
Lean은 다음과 같은 미래를 가리킵니다.
- 소프트웨어를 형식적으로 검증할 수 있다
- 수학이 기계 검증 가능해진다
- 프로그래밍과 추론이 하나로 합쳐진다
이 미래는 아직 초기 단계이지만, 다음 분야에서 점점 더 중요해지고 있습니다.
- 컴파일러
- 보안 시스템
- 암호학
- 정리 증명
- AI 검증
- 형식 수학
그리고 중요한 점: Lean 4는 실용적이어서 일반 개발자도 오늘부터 이러한 아이디어를 탐색할 수 있습니다.
마무리 생각
많은 초보자가 저지르는 실수는 Lean 4를 또 다른 프로그래밍 언어처럼 배우려는 것입니다.
Lean 4는 다음 네 가지 역할을 동시에 수행한다고 이해하는 것이 좋습니다.
- 프로그래밍 언어
- 증명 시스템
- 논리 프레임워크
- 사고 도구
학습 곡선은 존재하지만, 지적 보상은 남다르게 큽니다.
증명을 실행 가능한 구조로 이해하기 시작하면, 프로그래밍의 많은 부분이 영원히 달라 보이게 됩니다.
여러분이 Lean 4에서 처음으로 접했을 때, 프로그래밍이나 수학에 대한 사고 방식을 진정으로 바꾼 개념은 무엇이었나요?