安装教程推荐

Windows 下 Lean4 安装教程： 安装 – Lean定理证明 (subfish-zhou.github.io)

英文版：Extended Setup Notes – Lean Manual (lean-lang.org)

推荐：Lean4入门：安装配置篇_哔哩哔哩_bilibili

Lean4 参考教材地址：leanprover-community/mathematics_in_lean: The user home repository for the Mathematics in Lean tutorial. (github.com)

安装流程

配套软件安装顺序： glean(避免被墙) → o→ elan → o→ 确定项目依赖 → o→ 对应版本的 lean 4

到对应镜像地址下载 glean elan ; glean 下载后所需要的是其中的可执行文件 glean.exe ,执行安装 elan 压缩包里的安装文件 elan-init.exe 完成 elan 的安装，安装完后可以在用户目录下找到 .elan 文件夹，C:UsersUsername.elanin 也应该被自动添加进环境变量(若没有可以手动添加一下)；最后将 glean.exe 移动至 C:UsersUsername.elanin 文件夹里.
下载对应的项目文件，如 mathematics_in_lean，直接 git clone https://mirror.sjtu.edu.cn/git/lean4-packages/mathematics_in_lean ，如果不想使用镜像，可以到到对应的 github 仓库下载 .
到项目文件夹下的 lean-toolchain 查看所需 lean 4 的版本例如 leanprover/lean4:v4.xx.xx，使用 elan install leanprover/lean4:v4.xx.xx ；如果不想FQ，可以使用 glean -install lean --version 4.xx.xx 进行安装.
接下来进行编译，编译非常耗时，如果想节省时间且能FQ的话可以先在项目文件夹下执行 lake exe cache get 拉取 cache，再执行 lake build ; 如果不行，则只好花点时间直接在项目文件夹下执行 lake build，具体时间由 cpu 性能决定，一般 1h 内就可以编译好.
在 vscode 中安装 lean4 插件，即可完成基本项目环境的配置.

可能存在的问题：

使用 lake 相关指令后报错 error: could not detect the configuration of the Lake installation .

原因 : 路径中含有中文名，具体解决方案可以从参考这篇文章.

vscode 的 powershell 无法识别 elan 命令，具体如下

原因是因为找不到对应路径，解决方法如下：

ctrl+,打开 vscode 设置，搜索 terminal.integrated.env.windows，在 settings.json 中编辑，添加

  "terminal.integrated.env.windows": {
      "PATH":"C:/Users/Username/.elan/bin;${env:PATH}"
  },

注意，不要漏掉 ${env:PATH} 否则会导致丢失系统变量