---
title: "Lean 4로 처음부터 정리 증명까지 — 무료 입문 시리즈 공개"
published: 2025-12-13T23:42:03.000Z
canonical: https://jeff.news/article/824
---
# Lean 4로 처음부터 정리 증명까지 — 무료 입문 시리즈 공개

Lean 4를 프로그래밍 언어와 정리 증명기 두 관점에서 처음부터 가르치는 무료 시리즈. 글 자체가 컴파일 가능한 정리이며, 브라우저부터 로컬까지 다양한 실습 환경을 제공.

- Lean 4를 처음부터 가르치는 무료 시리즈 "From Zero to QED"가 공개됨. 기존 Lean 학습 자료가 여기저기 흩어져 있고 불완전한 상황에서, 이 공백을 메우려는 시도임

- 재밌는 건 이 글 자체가 하나의 거대한 검증 가능한 정리(theorem)라는 점. 모든 코드 샘플, 증명, 정의가 소스 파일에서 추출되어 Lean 컴파일러가 빌드할 때마다 타입 체크함. 글이 컴파일되면 정리가 유효한 거임

- 시리즈는 두 개의 아크로 구성됨:
  - **Arc I** — Lean을 프로그래밍 언어로 다룸. 문법, 타입 시스템, 제어 흐름, 다형성, 모나드, IO까지. 이 아크를 끝내면 실제 프로그램을 작성할 수 있음
  - **Arc II** — Lean을 정리 증명기(theorem prover)로 다룸. 증명 작성, 타입 이론, 의존 타입, 전술(tactics), 고전적 수학 결과 증명까지. AI와 정리 증명의 교차점, 형식 검증이 왜 앞으로 10년간 더 중요해질지도 다룸

- 정리 증명기 사전 경험은 불필요하고, Haskell·OCaml·Scala 같은 타입 함수형 언어 경험이 있으면 도움이 되지만 필수는 아님

> [!TIP]
> 따라하기 환경이 잘 갖춰져 있음. 브라우저에서 바로 실행 가능한 Lean Live, GitHub Codespaces(월 120 코어시간 무료), Gitpod, Dev Container, 로컬 설치까지 4가지 옵션 제공. `lake exe cache get`으로 Mathlib 프리빌트 아티팩트를 다운받으면 빌드 시간이 몇 시간에서 몇 분으로 줄어듦

- 독자별 추천 학습 경로도 제시함:
  - **완전 초보**: Arc I을 순서대로 읽고, 패턴 매칭·재귀·타입 클래스에 익숙해지기 전에 Arc II로 넘어가지 말 것
  - **검증에 관심 있는 시스템 프로그래머**: Arc I을 꼼꼼히 읽고, Arc II에서는 Proofs, Verified Programs, Model Checking에 집중
  - **정리 증명에 관심 있는 AI 연구자**: 기초 후 바로 Proofs → Tactics Reference → Artificial Intelligence로 점프
  - **프로그래밍이 처음인 수학자**: Basics와 Control Flow부터 시작, Effects와 IO는 처음엔 스킵 가능

## 핵심 포인트

- Arc I은 프로그래밍 언어로서의 Lean, Arc II는 정리 증명기로서의 Lean
- 글의 모든 코드가 Lean 컴파일러로 타입 체크되는 검증 가능한 문서
- 브라우저, Codespaces, Gitpod, Dev Container, 로컬 등 5가지 실습 환경
- AI 연구자, 시스템 프로그래머, 수학자 등 독자별 학습 경로 제시

## 인사이트

Lean 4의 학습 자료 부족 문제를 정면으로 해결하려는 야심찬 프로젝트. AI와 형식 검증의 교차점을 다루는 부분이 시의적절함.