lean是一款数学形式化语言，它可以用编程语言撰写数学证明，便于计算机进行形式验证，因此一定程度上可以避免人工检查数学证明所带来的负担和错误。

类似的语言有coq，isabelle，metamath等

lean4是lean的第四个版本，和lean3相比有很大改进。

除了lean官方的核心程序以外，lean社区还维护一个称为mathlib的库，它包含人类发展出的大多数数学领域的基本定义，公理，定理等。目前mathlib也已经更新到和lean4适配的mathlib4. 

lean4安装方法：

1. 安装VS Code

2. 在VS Code中安装扩展程序lean4

3. 创建新文件，语言选lean4，此时会自动下载安装lean4

4. 左边的输入窗口输入#eval 18 + 19，右边的信息窗口如果显示37，则说明安装完成

要导入数学定理库（例如mathlib4），参考https://github.com/leanprovercommunity/mathlib4/wiki/Using-mathlib4-as-a-dependency

不小心删除了一个横线，网址应该是https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency