Lean4 개요

Lean은 대화형 정리 증명기(Interactive Theorem Prover)이자 범용 함수형 프로그래밍 언어입니다. 2013년 Microsoft Research의 Leonardo de Moura가 시작했으며, 2021년 Lean4가 공개되었습니다. Apache 2.0 라이선스로 배포됩니다.

Lean의 핵심 특징은 수학적 형식화와 프로그래밍의 결합입니다. 수학자는 정리를 코드로 변환하여 엄격하게 검증할 수 있고, 프로그래머는 의존 타입(Dependent Type)을 갖춘 순수 함수형 언어로 개발할 수 있습니다.

개발 환경 구성

핵심 도구

• elan: Lean 버전 관리 도구 (Rust의 rustup, Node.js의 nvm 대응)
• lake: 패키지 관리자 및 빌드 도구
• lean: 컴파일러 및 LSP 서버

elan 명령어

-- 설치 확인
elan --version

-- 업데이트
elan self update

-- 설치된 버전 확인
elan show

-- 특정 버전 설치
elan install leanprover/lean4:v4.21.0

-- 기본 버전 전환
elan default leanprover/lean4:v4.21.0

-- 현재 디렉토리 버전 고정
elan override set leanprover/lean4:v4.21.0

-- 특정 버전으로 실행
elan run leanprover/lean4:v4.21.0 lean --run hello.lean

lake 명령어

-- 새 프로젝트 생성
lake new my_project

-- mathlib 포함 프로젝트 생성
lake new my_project math

-- 현재 디렉토리 초기화
lake init

-- 빌드
lake build

-- 캐시 다운로드
lake exe cache get

-- 의존성 업데이트
lake update

첫 프로그램

단일 파일 실행

-- Hello.lean
def main : IO Unit := IO.println "안녕, Lean!"

실행:

lean --run Hello.lean

정리 검증 예시

-- proof.lean
-- 성공하는 증명
theorem trivial_proof : 1 + 1 = 2 := by
  simp

-- 실패하는 증명
theorem wrong_proof : 1 + 1 = 1 := by
  simp  -- unsolved goals 오류 발생

검증 성공 시 출력 없음, 실패 시 오류 메시지 출력.

프로젝트 구조

lake로 생성한 프로젝트의 주요 파일:

• Main.lean: main 정의를 포함하는 진입점
• lakefile.toml: 의존성 및 빌드 설정
• lean-toolchain: 사용할 Lean 버전
• lake-manifest.json: 의존성 기록 (자동 생성)

모듈 시스템

네임스페이스 정의

-- Arithmetic.lean
namespace Arithmetic
def plus (a b : Nat) : Nat := a + b
def minus (a b : Nat) : Nat := a - b
end Arithmetic

모듈 가져오기

-- Main.lean
import Arithmetic

#eval Arithmetic.plus 3 5  -- 8

네임스페이스 없이 정의하면 import 후 직접 사용 가능:

-- Utils.lean
def greet (name : String) : String := s!"Hello, {name}"

-- Main.lean
import Utils

#eval greet "Lean"  -- "Hello, Lean"

기초 문법

주석

-- 한 줄 주석

/-
여러 줄
주석 블록
-/

def value : Nat := 42  -- 끝에도 가능

표현식 평가

#eval 6 * 7           -- 42
#check 6 * 7          -- Nat
#eval (1 - 3 : Int)   -- -2

변수와 정의

-- 전역 정의
def greeting : String := "Hello"

-- 타입 추론
def inferred := 100  -- Nat로 추론

-- 지역 바인딩
def computeSquare (x : Nat) : Nat :=
  let temp := x + x
  temp * temp

#eval computeSquare 3  -- 36

기본 타입

함수 정의

다양한 정의 방식

-- 전통적 문법
def increment (n : Nat) : Nat := n + 1

-- 람다 표현
def double : Nat → Nat := fun x => x * 2

-- 간략 람다 (점 표기법)
def halve : Nat → Nat := (· / 2)

-- 패턴 매칭
def isEven : Nat → Bool
  | 0 => true
  | 1 => false
  | n + 2 => isEven n

고차 함수

def applyTwice (f : Nat → Nat) (x : Nat) : Nat :=
  f (f x)

#eval applyTwice (fun y => y + 3) 5  -- 11

부분 적용과 커링

def multiply (x y : Nat) : Nat := x * y

-- 부분 적용
def triple := multiply 3

#eval triple 4  -- 12

꼬리 재귀

-- 비꼬리재귀 (스택 사용)
def factorialNaive (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | k + 1 => (k + 1) * factorialNaive k

-- 꼬리재귀 (최적화 가능)
def factorialOpt (n : Nat) : Nat :=
  let rec loop (remaining acc : Nat) : Nat :=
    match remaining with
    | 0 => acc
    | k + 1 => loop k (acc * (k + 1))
  loop n 1

#eval factorialOpt 5  -- 120

데이터 타입

归納 타입

-- 요일 정의
inductive Weekday where
  | monday | tuesday | wednesday | thursday | friday
  | saturday | sunday

-- 자연수 정의
inductive MyNat where
  | zero : MyNat
  | succ (n : MyNat) : MyNat

구조체

structure Coordinate where
  lat : Float
  lng : Float
deriving Repr

def origin : Coordinate := { lat := 0.0, lng := 0.0 }

#eval origin.lat  -- 0.000000

-- 상속
structure Location extends Coordinate where
  name : String

def tokyo : Location := {
  lat := 35.6762,
  lng := 139.6503,
  name := "Tokyo"
}

생성자 커스터마이징

structure Point where
  point ::
  x : Float
  y : Float

#check Point.point  -- Point.point : Float → Float → Point

패턴 매칭

def describe : Nat → String
  | 0 => "zero"
  | 1 => "one"
  | 2 => "two"
  | _ => "many"

def listSum : List Nat → Nat
  | [] => 0
  | head :: rest => head + listSum rest

#eval listSum [1, 2, 3, 4]  -- 10

다형성

-- 타입 매개변수
def identity (α : Type) (x : α) : α := x

-- 암묵적 인수
def swap {α β : Type} (pair : α × β) : β × α :=
  (pair.snd, pair.fst)

#eval swap (1, "hello")  -- ("hello", 1)

타입 클래스

class Comparable (α : Type) where
  compare : α → α → Ordering

instance : Comparable Nat where
  compare x y :=
    if x < y then Ordering.lt
    else if x > y then Ordering.gt
    else Ordering.eq

-- 사용
def max {α : Type} [Ord α] (a b : α) : α :=
  if compare a b = .gt then a else b

리스트 처리

def nums : List Nat := [10, 20, 30]

-- 안전한 접근
#eval nums[0]?     -- some 10
#eval nums.head?   -- some 10
#eval ([] : List Nat).head?  -- none

-- 기본값 제공
#eval [].headD 999  -- 999

-- 함수형 조작
#eval [1, 2, 3].map (· * 2)           -- [2, 4, 6]
#eval [1, 2, 3, 4].filter (· % 2 = 0) -- [2, 4]
#eval [1, 2, 3].foldl (· + ·) 0       -- 6

do 표기법과 IO

def greetMultiple : IO Unit := do
  let people := ["Alice", "Bob", "Carol"]
  
  for person in people do
    IO.println s!"Hello, {person}!"
  
  let mut counter := 3
  while counter > 0 do
    IO.println s!"Countdown: {counter}"
    counter := counter - 1

def main : IO Unit := do
  IO.println "프로그램 시작"
  greetMultiple
  IO.println "종료"

mathlib4 활용

프로젝트 설정

lake new my_math math

또는 기존 프로젝트에 수동 추가:

# lakefile.toml
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"

설치 후:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

활용 예시

import Mathlib.Data.Real.Basic

example (x y : ℝ) : x * y = y * x := by
  rw [mul_comm x y]

정리 증명 입문

-- 정리 선언과 증명
theorem add_zero_right (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ k ih => simp [ih]

-- simp를 활용한 간결한 증명
theorem distrib_left (x y z : Nat) : x * (y + z) = x * y + x * z := by
  simp [Nat.mul_add]

핵심 용어 정리

• 패키지: Lake의 코드 배포 단위
• 모듈: 빌드 시스템의 최소 코드 단위
• 라이브러리: 공통 설정을 공유하는 모듈 집합
• 타겟: Lake 빌드의 기본 단위
• 외부 라이브러리: C 등 외부 코드로 빌드된 네이티브 라이브러리