Floor 1
Posted at: 5/2/24 11:21
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
