Lean 技术栈

elan、Lake、Mathlib 与编辑器

把 Lean 想成「带类型检查的 R」会少走弯路：版本要锁，依赖要锁，包不能在全局环境里随便升级。本页对应实证轨里 renv + RStudio 的那一层。社区安装与项目说明见 Lean 文档与 Lean projects 页 (Lean prover community 2025年a, 2025年b)。

本仓库不在此时创建 Lean 工程。读完本页，应能在将来独立目录里初始化项目，而不把 Mathlib（Lean 的数学库）写进 _book/。

1 栈的分层

flowchart TB
  elan["elan<br/>工具链管理"] --> lean["Lean 4 编译器 + 内核"]
  lean --> lake["Lake<br/>包与构建"]
  lake --> cache["lake exe cache get<br/>预编译 Mathlib"]
  cache --> src["编写并检查 .lean"]
  editor["VS Code / Cursor<br/>Infoview"] --> src

组件 作用 实证侧类比
elan（Lean 工具链管理器） 按目录选择 Lean 版本 多版本 R / 模块系统
lean-toolchain 一行版本号，进 git renv.lock 的一部分
Lean 4 精化、内核检查、可执行解释器 R 语言本身
Lake（Lean + Make，包与构建） 依赖、构建、测试入口 Make / renv / devtools
lakefile.toml 包名、依赖、库根 DESCRIPTION
lake-manifest.json 钉死的 git 修订 锁文件
Mathlib（数学库） 可引用的定理与定义 CRAN（Comprehensive R Archive Network）上的矩阵与概率包，但是一个巨石库
Infoview（信息视窗） 当前目标与报错 RStudio 的环境 + traceback

2 elan（工具链管理器）与工具链文件

elan 相当于 Rust 的 rustup（Rust 工具链管理器）：往 PATH 里放 lean 与 lake 包装器，真正二进制按当前目录向上找到的 lean-toolchain 选择 (Lean FRO 2025年)。文件通常只有一行，例如：

leanprover/lean4:v4.24.0

打开该目录下的 .lean 文件时，扩展会让 elan 下载缺失的工具链。两个人复现同一证明，首先必须工具链一致。Mathlib 每个修订只对一个 Lean 版本构建；只改其中一个，常见症状是海量报错 (Lean prover community 2025年b)。

Windows 上偶发工具链损坏或杀毒软件干扰 lake exe cache get；社区故障排除写在同一项目页，包括删除 ~\.elan\toolchains 中坏掉的目录后再拉 (Lean prover community 2025年a)。

3 Lake：项目而不是单文件

单独打开一个 .lean 文件通常会得到令人困惑的错误。非平凡代码必须住在 Lake 项目里：git 仓库 + lakefile.toml（或旧式 lakefile.lean）+ lean-toolchain (Lean prover community 2025年a)。

常用命令：

lake +v4.24.0 new my_project math   # 带 Mathlib 的模板
cd my_project
lake update
lake exe cache get                  # 先拉 Mathlib 缓存，勿从源码编数小时
lake build

math 模板会写好 Mathlib 依赖、风格检查与 CI（Continuous Integration，持续集成）草稿。源码放在 MyProject/ 下，根文件 MyProject.lean 负责 import 表面——这与 lean-hansen-econometrics 的 HansenEconometrics.lean 相同。

lake exe cache get 只缓存 Mathlib 等上游的预编译产物，不缓存你自己的证明 (Lean prover community 2025年b)。自己的模块每次改动仍需局部构建。

构建产物与依赖克隆在 .lake/，应 gitignore。不要把 .lake 或 Mathlib 源码提交进 hansenpeer。

4 Mathlib：依赖而不是拷贝

正确姿势是在 lakefile.toml 里 require 社区 Mathlib，再让 lake-manifest.json 锁提交哈希。更新流程是：先把 lean-toolchain 换成 Mathlib 当前文件，再 lake update，然后 lake exe mk_all && lake build 看自己的文件是否仍通过 (Lean prover community 2025年a)。

对计量特别有用的入口（名称以你所用 Mathlib 版本的文档为准）：

  • 线性代数与矩阵：Mathlib.LinearAlgebra.*、Mathlib.Data.Matrix.*
  • 测度与积分：Mathlib.MeasureTheory.*
  • 条件期望：MeasureTheory.condExp，记号 μ[f | m]
  • 概率：Mathlib.Probability.*

库定理往往比 Hansen 更一般。教学包装层的工作是变薄，不是把 Mathlib 再写一遍。

5 编辑器与 Infoview

官方推荐 Visual Studio Code（VS Code）+ Lean 4 扩展。Cursor 基于 VS Code，通常可装同一扩展；以扩展文档为准。关键交互：

  • 光标所在处显示目标（⊢ 之后是待证命题）。
  • #check、#print、#print axioms 做只读探查。
  • Ctrl-Shift-Enter（macOS 为 Cmd-Shift-Enter）找回 Infoview。
  • Lean 4: Docs: Show Documentation Resources 可在编辑器内打开 Theorem Proving in Lean（TPIL）与 Mathematics in Lean（MIL）(Lean prover community 2025年a)。

没有 Infoview 的形式化，相当于不用 REPL（Read-Eval-Print Loop，交互式求值循环）写 R：理论上能提交脚本，实际上无法工作。

6 版本策略（将来的 L3）

若本项目日后单开 Lean 仓库：

  1. 跟当时的 Mathlib 稳定标签，不必绑定 lean-hansen-econometrics 的 4.29.0，也不必绑定某篇分析论文的 4.34.0-rc2。
  2. Lean 与 Mathlib 一次锁死，写入 lean-toolchain 与 lake-manifest.json。
  3. CI（持续集成）跑 lake exe cache get && lake build。风格检查可后加。
  4. README 写明：内核通过 ≠ 印刷原句。

方法页 技术栈·理论轨 已预告同一原则。

7 明确不放进 hansenpeer

不放 原因
lakefile.toml / .lake/ / Mathlib 源码 站点构建与 Lean 构建解耦；体积与许可证管理分开
把 .lean 塞进 _book/ 或 hansenEM/chapters_* 教材源稿与逻辑证书不是同一种文件
整库 fork lean-hansen-econometrics 对照与借鉴即可；差异化是中文 L1 与实证复现

学习阶段建议：另建目录克隆 Mathematics in Lean 或 lake new ... math，与 Quarto 站点并列，不要混 git。练习路线见 学习资源。

参考文献

Lean FRO. 2025年. elan: Lean Version Manager. https://github.com/leanprover/elan/.
Lean prover community. 2025年a. Lean Projects. https://leanprover-community.github.io/install/project.html.
Lean prover community. 2025年b. Using mathlib4 as a Dependency. https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency.