类似的语言有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