打開鏡像下載：

上海交通大學鏡像

搜索 elan

下載elan和glean

elan 下載路徑 elan/elan/releases/download/eager-resolution-v2

打開上面下載的 elan-init ，然後輸入 1 選擇使用 default

將 glean 解壓放到用户目錄下的 .lean/bin 目錄下

搜索lean找到下面這個

git/lean4-packages/mathematics_in_lean

然後右鍵複製鏈接

git clone https://mirror.sjtu.edu.cn/git/lean4-packages/mathematics_in_lean

然後進入目錄，查看 lean-toolchain 裏面的版本號，

然後使用以下命令安裝上面查看的版本(但是這裏輸入版本號是從數字開始，比如查看到的是：leanprover/lean4:v4.8.0-rc2，輸入的是4.8.0-rc2)

glean -install lean -version 4.8.0-rc2

然後繼續在這個目錄中輸入 glean 命令回車

glean

然後再繼續輸入以下命令編譯安裝依賴，時間有點久。大概15-25分鐘左右。

lake build

查看當前lean設置

elan show

查看 lean-toolchain 文件裏面的版本號

使用以下命令設置工具鏈

elan default leanprover/lean4:v4.8.0-rc2