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