这个教程是关于如何用lean4和mathlib4做数学的
https://leanprover.github.io/theorem_proving_in_lean4/
这个教程是lean4语言本身的教程，更偏向对语言机制的介绍，不包含mathlib的使用
目前共有4篇帖子。
lean4教程
 |
https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的 |
 |
感觉使用lean4很像用计算机编程
啊啊是谁都对：有无最简单的实例？
悄悄打开魔盒：回复 @啊啊是谁都对：有的，git clone https://github.com/leanprover-community/mathematics_in_lean.git下载mathematics_in_lean，在这个项目的目录下lake exe cache get就可以下载相应的依赖文件，然后在vscode里打开项目文件夹，在MIL子文件夹下就可以看到例子了
[查看詳情]
|
