安装

# linux, Ubuntu (会自动装vscode，如果你已经装了vscode，直接打开vscode去插件市场手动安装lean4插件就可以开始上手了)
wget -q <https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh> && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

# MacOS
/bin/bash -c "$(curl -fsSL <https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh>)" && source ~/.profile

# Windows
<https://leanprover-community.github.io/install/windows.html>

周边：安装git、vscode+lean4扩展

更新至最新

elan self update  # 以防你下载的不是最新版elan  
# 下载及应用最新的Lean4版本 (<https://github.com/leanprover/lean4/releases>) 
elan default leanprover/lean4:stable

创建一个以 .lean 为扩展名的新文件，并写入以下代码：

#eval Lean.versionString

以下即为安装成功，环境准备完毕

开启新项目

创建新Lean项目

用VS code打开一个新文件夹，你可以用两种方式创建新项目。

最简新项目

在终端中运行以创建一个名为your_project_name的空白新项目。

lake init <your_project_name>

如果你想把你的Lean程序编译成可执行文件，在终端中运行lake build命令。

带mathlib的新项目

方式一：创建一个名为your_project_name的一个引用Mathlib4的新项目

lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math