9.1. Lean 배우기🔗

Lean 4 자체는 다음 자료들에서 설명됩니다:

• Theorem Proving in Lean 4는 Lean을 사용하여 증명을 작성하는 방법에 대한 튜토리얼입니다.

• Lean 4 매뉴얼은 언어와 그 기능에 대한 상세한 설명을 제공합니다.

• How To Prove It With Lean는 종이와 연필로 쓰는 수학적 증명 작성법을 소개하는 정평 있는 교재 How To Prove It를 Lean 기반으로 보완한 책입니다.

• Metaprogramming in Lean 4는 중위 연산자와 표기법부터 매크로, 사용자 정의 택틱, 완전한 사용자 정의 임베디드 언어에 이르기까지 Lean의 확장 메커니즘에 대한 개요를 제공합니다.

• Functional Programming in Lean은 재귀에 관한 농담을 즐기는 독자에게 흥미로울 수 있습니다.

하지만 Lean을 계속 배우는 가장 좋은 방법은 코드를 읽고 작성하는 것을 시작하고, 막힐 때 문서를 참고하는 것입니다. 또한, Lean Zulip은 다른 Lean 사용자들을 만나고, 도움을 요청하고, 다른 사람을 도울 수 있는 훌륭한 장소입니다.

9.2. Lean으로 하는 수학🔗

수학자를 위한 다양한 학습 자료는 커뮤니티 사이트에서 확인할 수 있습니다.

9.3. 컴퓨터 과학에서 의존 타입 활용하기🔗

Rocq는 Lean과 공통점이 많은 언어입니다. 컴퓨터 과학자에게는, 컴퓨터 과학에서 Rocq의 응용에 대한 훌륭한 입문서로 대화형 교재 시리즈인 Software Foundations가 있습니다. Lean과 Rocq의 근본적인 아이디어는 매우 유사하며, 두 시스템 사이에서 기술을 손쉽게 옮겨 사용할 수 있습니다.

9.4. 의존 타입을 사용한 프로그래밍🔗

프로그램을 구조화하기 위해 인덱스 패밀리와 의존 타입을 사용하는 방법을 배우고자 하는 프로그래머에게, Edwin Brady의 Type Driven Development with Idris는 훌륭한 입문서를 제공합니다. Rocq와 마찬가지로, Idris는 Lean의 가까운 사촌 격이지만 택틱은 없습니다.

9.5. 의존 타입 이해하기🔗

The Little Typer는 논리학이나 프로그래밍 언어 이론을 정식으로 공부한 적은 없지만 의존 타입 이론의 핵심 아이디어에 대한 이해를 쌓고자 하는 프로그래머를 위한 책입니다. 위에서 소개한 자료들이 모두 최대한 실용적인 것을 목표로 하지만, The Little Typer는 프로그래밍의 개념만을 사용하여 아주 기초부터 처음부터 쌓아 올리는 방식으로 의존 타입 이론에 접근하는 방법을 제시합니다. 참고: Functional Programming in Lean의 저자는 The Little Typer의 저자이기도 합니다.