這個教程是關於如何用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子文件夾下就可以看到例子了
[查看詳情]
|
