소개🔗

Lean은 의존 타입 이론에 기반한 대화형 정리 증명기입니다. 원래 마이크로소프트 리서치에서 개발되었으나, 현재는 Lean FRO에서 개발이 이루어지고 있습니다. 의존 타입 이론은 프로그램의 세계와 증명의 세계를 통합합니다. 따라서 Lean은 프로그래밍 언어이기도 합니다. Lean은 자신의 이중적 본성을 진지하게 받아들이며, 범용 프로그래밍 언어로 사용하기에 적합하도록 설계되었습니다—Lean은 심지어 그 자체로 구현되어 있습니다. 이 책은 Lean으로 프로그램을 작성하는 것에 관한 책입니다.

프로그래밍 언어로 볼 때, Lean은 의존 타입을 갖춘 엄격한 순수 함수형 언어입니다. Lean으로 프로그래밍하는 법을 배우는 것의 상당 부분은 이러한 각 속성이 프로그램 작성 방식에 어떤 영향을 미치는지, 그리고 함수형 프로그래머처럼 사고하는 방법을 배우는 것으로 이루어져 있습니다. 엄격성은 Lean에서 함수 호출이 대부분의 언어에서와 유사하게 동작한다는 것을 의미합니다. 즉, 인자는 함수의 본문이 실행되기 시작하기 전에 완전히 계산됩니다. 순수성은 Lean 프로그램이 프로그램의 타입이 그렇다고 명시하지 않는 한 메모리 위치를 수정하거나, 이메일을 보내거나, 파일을 삭제하는 것과 같은 부수 효과를 가질 수 없다는 것을 의미합니다. Lean은 함수가 다른 값과 마찬가지로 일급 값이며 실행 모델이 수학적 표현식의 평가에서 영감을 받았다는 의미에서 함수형 언어입니다. Lean의 가장 특이한 기능인 의존 타입은 타입을 언어의 일급 요소로 만들어, 타입이 프로그램을 포함하고 프로그램이 타입을 계산할 수 있게 합니다.

이 책은 Lean을 배우고자 하지만 함수형 프로그래밍 언어를 반드시 사용해 본 적은 없는 프로그래머를 대상으로 합니다. Haskell, OCaml, F# 등의 함수형 언어에 익숙할 필요는 없습니다. 반면, 이 책은 대부분의 프로그래밍 언어에 공통적인 반복문, 함수, 자료구조와 같은 개념에 대한 지식은 전제로 합니다. 이 책은 함수형 프로그래밍을 처음 접하는 사람에게 좋은 입문서가 되는 것을 목표로 하지만, 프로그래밍 전반을 처음 배우는 사람에게 좋은 입문서는 아닙니다.

정리 증명기로 Lean을 사용하는 수학자들은 언젠가 사용자 정의 증명 자동화 도구를 작성해야 할 필요가 있을 것입니다. 이 책은 그들을 위한 것이기도 합니다. 이러한 도구들이 점점 더 정교해지면서 함수형 언어의 프로그램과 유사한 모습을 띠게 되지만, 대부분의 현업 수학자들은 Python이나 Mathematica와 같은 언어에 익숙합니다. 이 책은 그 간극을 메우는 데 도움을 줄 수 있으며, 더 많은 수학자가 유지 관리하기 쉽고 이해하기 쉬운 증명 자동화 도구를 작성할 수 있도록 힘을 실어 줍니다.

이 책은 처음부터 끝까지 순서대로 읽도록 구성되어 있습니다. 개념은 한 번에 하나씩 소개되며, 이후 절들은 이전 절들에 대한 이해를 전제로 합니다. 때때로 뒷부분의 장에서는 앞서 간략히 다루었던 주제를 깊이 있게 다루기도 합니다. 이 책의 일부 절에는 연습 문제가 포함되어 있습니다. 이 절의 내용을 확실히 이해하기 위해서는 이 문제들을 풀어 보는 것이 좋습니다. 책을 읽으면서 Lean을 직접 탐구하고, 배운 내용을 창의적인 새로운 방식으로 활용해 보는 것도 유용합니다.

Lean 설치하기🔗

Lean으로 작성된 프로그램을 작성하고 실행하기 전에, 자신의 컴퓨터에 Lean을 설치해야 합니다. Lean 도구 모음은 다음으로 구성됩니다:

elan은 rustup이나 ghcup과 유사하게 Lean 컴파일러 툴체인을 관리합니다.
lake는 cargo, make, Gradle과 유사하게 Lean 패키지와 그 의존성을 빌드합니다.
lean은 개별 Lean 파일을 타입 검사하고 컴파일하며, 현재 작성 중인 파일에 대한 정보를 프로그래머 도구에 제공합니다. 일반적으로 lean은 사용자가 직접 실행하기보다는 다른 도구에 의해 호출됩니다.
Visual Studio Code나 Emacs와 같은 편집기용 플러그인으로, lean과 통신하여 그 정보를 편리하게 제공합니다.

Lean 설치에 대한 최신 안내는 Lean 매뉴얼을 참조하십시오.

타이포그래피 규칙🔗

Lean에 입력으로 제공되는 코드 예제는 다음과 같이 서식이 지정됩니다:

def add1 (n : Nat) : Nat := n + 1#eval add1 7

위의 마지막 줄(#eval로 시작하는 줄)은 Lean에게 답을 계산하도록 지시하는 명령입니다. Lean의 응답은 다음과 같이 서식이 지정됩니다:

Lean이 반환하는 오류 메시지는 다음과 같이 서식이 지정됩니다:

Application type mismatch: The argument
  "seven"
has type
  String
but is expected to have type
  Nat
in the application
  add1 "seven"

경고는 다음과 같이 표시됩니다:

declaration uses `sorry`

유니코드🔗

관용적인 Lean 코드는 ASCII에 속하지 않는 다양한 유니코드 문자를 사용합니다. 예를 들어, α와 β 같은 그리스 문자와 화살표 →는 모두 이 책의 첫 장에 등장합니다. 이를 통해 Lean 코드가 일반적인 수학적 표기법에 더 가깝게 보일 수 있습니다.

Lean의 기본 설정에서는 Visual Studio Code와 Emacs 모두 백슬래시(\) 뒤에 이름을 입력하는 방식으로 이러한 문자를 입력할 수 있습니다. 예를 들어, α를 입력하려면 \alpha를 입력하십시오. Visual Studio Code에서 어떤 문자를 입력하는 방법을 알아내려면, 마우스를 해당 문자 위에 올려놓고 툴팁을 확인하십시오. Emacs에서는 해당 문자에 커서를 두고 C-c C-k를 사용하십시오.

릴리스 이력🔗

2025년 10월🔗

이 책은 최신 안정 버전의 Lean 릴리스(버전 4.23.0)로 업데이트되었으며, 이제 함수적 귀납법과 grind 택틱을 다룹니다.

2025년 8월🔗

이 릴리스는 책에서 코드를 복사해서 붙여넣을 때 발생하는 문제를 해결하기 위한 유지 관리 릴리스입니다.

2025년 7월🔗

이 책은 Lean 4.21 버전에 맞춰 업데이트되었습니다.

2025년 6월🔗

이 책은 Verso로 다시 포맷되었습니다.

2025년 4월🔗

이 책은 대폭 갱신되었으며, 이제 Lean 4.18 버전을 설명합니다.

2024년 1월🔗

이는 예제 프로그램의 회귀를 수정하는 사소한 버그 수정 릴리스입니다.

2023년 10월🔗

이번 첫 유지 관리 릴리스에서는 여러 소소한 문제가 수정되었으며, 본문 내용을 Lean의 최신 릴리스에 맞춰 최신화하였습니다.

2023년 5월🔗

이제 이 책이 완성되었습니다! 4월의 사전 공개판과 비교하여, 많은 세부 사항이 개선되었고 사소한 오류들이 수정되었습니다.

2023년 4월🔗

이번 릴리스에서는 택틱을 사용한 증명 작성에 관한 막간과 더불어, 성능 및 비용 모델에 대한 논의를 종료 증명 및 프로그램 동치 증명과 결합한 마지막 장을 추가합니다. 이는 최종 릴리스에 앞선 마지막 릴리스입니다.

2023년 3월🔗

이번 릴리스는 의존 타입과 인덱스가 있는 계열(indexed family)을 이용한 프로그래밍을 다루는 장을 추가합니다.

2023년 1월🔗

이번 릴리스에서는 do-표기법에서 사용할 수 있는 명령형 기능에 대한 설명을 포함하여 모나드 트랜스포머에 관한 장을 추가합니다.

2022년 12월🔗

이번 릴리스는 애플리커티브 펑터에 관한 장을 추가하며, 구조체와 타입 클래스도 더 자세히 설명합니다. 이와 함께 모나드에 대한 설명도 개선되었습니다. 2022년 12월 릴리스는 겨울 휴가로 인해 2023년 1월까지 연기되었습니다.

2022년 11월🔗

이번 릴리스에서는 모나드를 사용한 프로그래밍에 관한 장을 추가합니다. 또한, 강제 변환 절에서 JSON을 사용하는 예제가 완전한 코드를 포함하도록 업데이트되었습니다.

2022년 10월🔗

이번 릴리스는 타입 클래스에 관한 장을 완성합니다. 또한, 명제, 증명, 택틱을 소개하는 짧은 막간이 타입 클래스에 관한 장 바로 앞에 추가되었는데, 이는 이러한 개념에 대한 약간의 친숙함이 표준 라이브러리 타입 클래스 중 일부를 이해하는 데 도움이 되기 때문입니다.

2022년 9월🔗

이번 릴리스는 타입 클래스에 관한 장의 전반부를 추가합니다. 타입 클래스는 Lean에서 연산자를 오버로딩하는 메커니즘이며, 코드를 조직화하고 라이브러리를 구조화하는 중요한 수단입니다. 또한, 두 번째 장은 Lean의 스트림 API 변경 사항을 반영하도록 업데이트되었습니다.

2022년 8월🔗

이번 세 번째 공개 릴리스에서는 프로그램 컴파일 및 실행 방법과 더불어 부작용에 대한 Lean의 모델을 설명하는 두 번째 장이 추가되었습니다.

2022년 7월🔗

두 번째 공개 릴리스는 첫 번째 장을 완성합니다.

2022년 6월🔗

이것은 서론과 첫 번째 장의 일부로 구성된 최초의 공개 릴리스였습니다.

저자 소개🔗

David Thrane Christiansen은 함수형 언어를 20년, 의존 타입을 10년 동안 사용해 왔습니다. Daniel P. Friedman과 함께 그는 의존 타입 이론의 핵심 아이디어를 소개하는 책 The Little Typer를 저술했습니다. 그는 코펜하겐 IT 대학교에서 박사 학위를 받았습니다. 학업 기간 동안 그는 Idris 언어의 첫 번째 버전에 주요 기여자로 참여했습니다. 학계를 떠난 이후, 그는 오리건주 포틀랜드의 Galois와 덴마크 코펜하겐의 Deon Digital에서 소프트웨어 개발자로 일했으며, Haskell Foundation의 상무이사(Executive Director)를 역임했습니다. 이 글을 쓰는 시점에 그는 Lean 전문 연구 기관에서 Lean 작업에 전념하며 근무하고 있습니다.

라이선스🔗

This work is licensed under a Creative Commons Attribution 4.0 International License.

이 책의 원본 버전은 David Thrane Christiansen이 Microsoft Corporation과의 계약 하에 집필하였으며, Microsoft Corporation은 이를 관대하게도 Creative Commons Attribution 4.0 International License 하에 공개하였습니다. 현재 버전은 최신 버전의 Lean에서 발생한 변경 사항을 반영하기 위해 저자가 원본 버전에서 수정한 것입니다. 변경 사항에 대한 자세한 내용은 이 책의 소스 코드 저장소에서 확인할 수 있습니다.