装好 Lean 4
做完这一节，你的电脑上会有一个 Test.lean 文件，Lean 在里面算出了 1 + 1 的结果。
官方推荐的装法是 VS Code 加 Lean 4 扩展，剩下的由扩展带着你做。下面先走这条路。
开始之前
- 一台 Windows、macOS 或 Linux 电脑，能上网
- 只是想先试试、不想安装：直接看本页最后的“先不安装”
第 1 步：安装 VS Code
到 code.visualstudio.com 下载并安装 VS Code。已经装过就跳过。
你应该看到：能打开 VS Code 的主界面。
- VS Code 能打开
第 2 步：安装 Lean 4 扩展
在 VS Code 的扩展市场里搜索并安装官方的 Lean 4 扩展，它的标识是 leanprover.lean4。
习惯用命令行的话，这一条命令效果相同：
code --install-extension leanprover.lean4官方提醒：命令里的 leanprover.lean4 要写全，否则装不上官方扩展。
- 扩展列表里有 Lean 4
第 3 步：跟着扩展完成设置
扩展自带一份设置向导。如果它没有自动打开：
- 新建一个空文件：
File > New Text File，或按Ctrl+N（macOS 是Cmd+N）。 - 点窗口右上角的
∀符号。 - 选
Documentation > Docs: Show Setup Guide…。
照着向导做完。它会替你装好 elan，也就是 Lean 的版本管理器。
- 设置向导走完了
第 4 步：让 Lean 算 1 + 1
- 新建文件，保存为
Test.lean。第一次保存时，VS Code 右下角会出现一个小弹窗，Lean 的工具链在后台安装，等它装完。 - 在文件里输入：
#eval 1 + 1你应该看到：没有任何警告和报错。把鼠标移到带下划线的 #eval 上，提示里显示计算结果：
2Test.lean里的#eval 1 + 1显示出 2
另一种装法：只用命令行
不用 VS Code 向导，也可以自己装 elan。Lean 需要 git 和 curl。
Linux 和 macOS：
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh出现提示时选 1，接受默认选项。然后让当前终端认得新装的命令：
source $HOME/.elan/envWindows（PowerShell）：
curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1装完后验证：
lean --version$lean --version
Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release)
你应该看到：以 Lean (version 开头的一行，后面是版本号。本课的代码用 4.35.0 检查过，你的版本更新一些也没关系。
官方仍然建议优先用上面的 VS Code 装法；命令行装完之后，写证明时还是需要一个能显示目标状态的编辑器。
先不安装
官方有一个在线版：live.lean-lang.org。Lean 运行在它的服务器上，你在浏览器里写代码。它的定位就是给新手在安装之前先试试，以及跑一些小片段，不适合做大项目。
这门课前几节的代码都很短，可以先在那里跟着做，学到归纳那一章再装也来得及。
没成功？
终端里提示找不到 lake 或 lean。 elan 的路径还没有生效。运行 source $HOME/.elan/env，或者关掉终端重新打开。系统如果建议你用 sudo apt install elan 来装，不要照做，按上面的办法把路径加上就行。
保存 Test.lean 后很久没反应。 第一次保存会在后台下载完整的工具链，右下角有进度弹窗。等它结束再看结果。
检查点
- VS Code 里装好了 Lean 4 扩展
Test.lean里#eval 1 + 1显示 2- 我知道在线版的网址，没装好的时候可以先用它
下一节
工具有了。第一个证明里，你会写下一条定理，并让 Lean 确认它。