1.lean4官方文檔的地址（可以不看）

https://leanprover-community.github.io/get_started.html

1. 安裝git 后，在github上下載安裝相關(guān)包;

2. 安裝vscod 增加 lean4插件；

3. 按官方流程安裝lean和mathlib4 并編譯 (在沒(méi)有FQ的情況下，這是很考運(yùn)氣的一件事，我沒(méi)有FQ，所以也沒(méi)按官方流程安裝) ；

4. 使用所謂的國(guó)內(nèi)源上海交大源glean，（也是浪費(fèi)時(shí)間的事情，估計(jì)是版本的問(wèn)題，很討厭這種做事做一半的風(fēng)格。浪費(fèi)了我嘴里前爹后媽的半天時(shí)間，但之后后思問(wèn)題應(yīng)該是因?yàn)樽约簛y來(lái)才安裝國(guó)內(nèi)源失敗，不能怪他人）。

ps:程序狗最恨配環(huán)境，配環(huán)境最是影響賺奶粉錢的速度。為了給大家省時(shí)間可以點(diǎn)下面的網(wǎng)盤鏈接，作者已經(jīng)做好了免安裝包。

https://pan.baidu.com/s/187q08wpNuCt400k2Xr-oVQ?pwd=fhgf

2.直奔主題，使用學(xué)習(xí)lean4和mathlib4：

1. 安裝git 非充要條件；

2. 安裝vscod也是非充要條件(用notepad或vi編代碼才體驗(yàn)無(wú)環(huán)境編程輕松)；

3. 有elan 和編譯好的mathlib4庫(kù)，才是真正的充分且必要條件。

[if !supportLists]l?[endif]所以真正的一鍵安裝方法:

1. 去一臺(tái)安裝好環(huán)境的電腦把elan和編譯好的mathlib4庫(kù)把內(nèi)容復(fù)制過(guò)來(lái)；

2. 把環(huán)境變量加到Path中，加到新系統(tǒng)的path中就可以。

只需如上圖的兩步操作便可！

因步驟1對(duì)一般人中是缺少前置條件，為此作者提供了網(wǎng)盤下載，補(bǔ)完條件一, 只需要解壓到任意無(wú)中文的目錄下，然后執(zhí)行批處理注冊(cè)環(huán)境變量。

百度網(wǎng)盤鏈接(資源lean4和mathlib4版本20241104從github在線下載)

https://pan.baidu.com/s/187q08wpNuCt400k2Xr-oVQ?pwd=fhgf

如擔(dān)心作者在bat里搞鬼可以自己手動(dòng)添加elan和mathlib4目錄到PATH環(huán)境變量中（如上圖）：

%您所解壓的目錄%.elan\toolchains\stable\bin

3.開(kāi)啟lean之旅

測(cè)試方法，win + r, 在任意地方寫一個(gè) lean4 + mathlib4 的Hello World! ?寫個(gè)a.txt代碼如下：

import Mathlib.Tactic.Abel

#eval "Hello World! "

然后在命令行中運(yùn)行: lean a.txt

到此有沒(méi)有感到輕松？有某種破除迷思的感覺(jué)？如果有，不用謝我，道理本就如此。

?3.補(bǔ)充

1.vscode還是可以裝，然后添加lean4插件，畢竟有代碼高亮，這是正路；

與無(wú)審美的色盲程序老狗不同，看啥都差不多才會(huì)老用notepad；

2.windows中執(zhí)行l(wèi)ean代碼最好是用powershell;

3.解決亂碼問(wèn)題，先在powershell中運(yùn)行：

$OutputEncoding = [Console]::OutputEncoding = [System.Text.Encoding]::UTF8。

4.學(xué)習(xí)mathematics_in_lean可以自己去改原來(lái)的開(kāi)頭import的內(nèi)容，免得又被奇怪的路徑問(wèn)題困擾，壓縮包里已經(jīng)有了一個(gè)例子，能用lean的帥哥看一眼就會(huì)明白原理。