9.1. Lean 배우기🔗

Lean 4 자체에 대한 설명은 다음 자료에서 찾을 수 있습니다.

• 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의 확장 메커니즘을 개괄적으로 소개합니다.

• 재귀에 관한 농담을 즐기는 독자라면 Lean으로 하는 함수형 프로그래밍에 흥미를 느낄 수도 있습니다.

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

9.2. Lean으로 하는 수학🔗

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

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

Rocq는 Lean과 공통점이 많은 언어입니다. 컴퓨터 과학자에게는 대화형 교재 시리즈인 Software Foundations가 컴퓨터 과학에서 Rocq를 활용하는 방법을 훌륭하게 소개합니다. 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의 공동 저자이기도 합니다.