安装工具链
用 elan 管理 Lean 版本，VS Code / Cursor 安装 Lean 4 扩展，Lake 创建项目。
I
Setup
安装和项目结构
官网推荐 VS Code / Cursor + Lean 4 扩展。命令行由 elan 管理 Lean 版本，lake 管理项目。
安装工具链
macOS 上安装 Lean 版本管理器 elan，然后加载环境变量。
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source ~/.elan/env安装编辑器扩展
Lean 的交互体验主要靠 InfoView：目标、假设、错误都会实时显示。
code --install-extension leanprover.lean4创建项目
所有正式 Lean 代码都建议放进 Lake 项目。
lake new MyLeanProject
cd MyLeanProject
lake build
code .
II
Code
先把 Lean 当成一门语言写
#eval 用来直接运行表达式；def 定义函数；theorem 写可被 Lean 检查的证明。
A
运行一个函数
def addTwo (n : Nat) : Nat :=
n + 2
#eval addTwo 40结果：42
B
当前练习文件
lean_playground/LeanPlayground/Basic.lean把新的函数和定理先放这里。每次保存后，编辑器右侧 InfoView 会显示当前目标。
III
Proof notes
证明笔记：从计算到归纳
Natural Number Game 的重点不是「Lean 会算」，而是把每一步改写暴露出来。本站已将 learn_proof 练习笔记同步到教材库，可对照 NNG 逐步练习。
2 + 2 = 4
theorem two_add_two : 2 + 2 = 4 := by
rfl标准 Lean 里 rfl 可以直接通过。游戏里会要求你用 rw 展开 succ，训练「等式改写」的手感。
归纳假设 hd
证明 zero_add 时，归纳步骤里有：
hd : 0 + d = d当目标里出现 0 + d，就可以：
rw [hd]它只是把当前目标里的 0 + d 替换成 d。
succ_add 关键点
theorem succ_add (a b : ℕ) : succ a + b = succ (a + b) := by
induction b with d hd
rw [add_zero]
rfl
rw [add_succ]
rw [add_succ]
rw [hd]
rfl卡点通常是少了第二个 rw [add_succ]：左边和右边都要把加法展开到能看见归纳假设的位置。
IV
Chinese books
中文教材库
官方教程与 Lean-zh 社区译本的 Markdown 已接入本站，共 13 本书。支持 LaTeX 公式、Lean 代码高亮与全文搜索。
Lean 常见问题（FAQ）
官方 FAQ 中文 · 用途、逻辑、可信代码基。
VS Code Lean 4 手册
安装、InfoView、项目与版本管理。
Lean 4 定理证明（TPIL4）
全书 12 章 · 依赖类型论、命题逻辑、策略、归纳类型。
逻辑与证明（Logic and Proof）
全书已译 · 自然演绎、一阶逻辑、集合、关系、数论。
Lean 函数式编程（FP in Lean）
全书已完成 · 单子、类型类、依赖类型、程序证明。
Lean 中的数学（MiL）
全书 13 章 · Mathlib、代数、拓扑、测度论。
逻辑验证漫游指南（LoVe）
全书 14 章 · 操作语义、Hoare 逻辑、元编程。
证明的机制（Math 2001）
严谨证明写作 + Lean · 全书已译（10 章 + 附录）。
Lean 语言参考手册
安装、类型系统、策略、Lake、Elan 等 240+ 篇译文。
证明练习笔记
5 章练习 · rfl、rw、归纳法与 NNG 风格示例。
搜索全部教材
按标题或正文搜索 2900+ 篇章节。
查看全部教材
进入教材库首页，含交互式与社区资源。
V
Learning path
外部学习资源
交互式教程无法导出为 Markdown，请在教材库「交互式学习」区查看完整列表；NNG4 建议配合本站证明练习笔记使用。
VI
Cloudflare Pages
部署到 Cloudflare
这个站是纯静态网站，最适合 Cloudflare Pages。部署前会先同步全部教材 Markdown 到 books/data/。
- 同步教材：
npm run build - 确认已登录：
npx wrangler whoami - 如果没登录：
npx wrangler login - 构建并部署：
npm run deploy
# 本地预览（含教材同步）
npm run preview
# 仅同步教材
npm run build
# Cloudflare Pages 部署
npm run deploy