9.1. Learning Lean🔗

Lean 4 자체는 다음 자료에서 설명한다:

• Lean 4에서 정리 증명하기는 Lean을 사용한 증명 작성 튜토리얼이다.

• Lean 4 매뉴얼은 언어와 기능을 자세히 설명한다.

• Lean으로 증명하는 법은 종이와 연필로 수학적 증명을 작성하는 법을 소개하는 유명 교재 증명하는 법의 Lean 기반 보충 자료다.

• Lean 4 메타프로그래밍은 중위 연산자와 표기법부터 매크로, 사용자 정의 전술, 완전한 임베디드 언어까지 Lean의 확장 메커니즘을 개관한다.

• Lean 함수형 프로그래밍은 재귀 농담을 좋아하는 독자에게 흥미로울 수 있다.

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

9.2. Mathematics in Lean🔗

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

9.3. Using Dependent Types in Computer Science🔗

Rocq는 Lean과 공통점이 많은 언어다. 컴퓨터 과학자에게 Software Foundations 대화형 교재 시리즈는 컴퓨터 과학에서 Rocq를 응용하는 훌륭한 입문서다. Lean과 Rocq의 기본 아이디어는 매우 비슷하므로 한 시스템의 기술을 다른 시스템에도 쉽게 적용할 수 있다.

9.4. Programming with Dependent Types🔗

인덱싱된 패밀리와 종속 타입으로 프로그램을 구조화하는 법에 관심 있는 프로그래머에게 Edwin Brady의 Idris를 사용한 타입 주도 개발은 훌륭한 입문서다. Idris는 Rocq처럼 Lean의 가까운 친척이지만 전술은 없다.

9.5. Understanding Dependent Types🔗

The Little Typer는 논리나 프로그래밍 언어 이론을 정식으로 공부하지 않았지만 종속 타입 이론의 핵심 개념을 이해하고 싶은 프로그래머를 위한 책이다. 위 자료들이 최대한 실용적인 것을 목표로 하는 반면, The Little Typer는 프로그래밍 개념만 사용하여 종속 타입 이론의 기초부터 쌓아 올린다. 주의: Lean 함수형 프로그래밍의 저자는 The Little Typer의 저자이기도 하다.