官网的各种文档很丰富!

首先是安装 elan: Lean version manager, 熟悉 Rust 的自然了然于胸, 类似于 rustup. elan 是 Rust 编写的 (嗯, 会不会未来 Lean 的 C++ 也会切换到 Rust? 哈哈)

# source $HOME/.elan/env
elan self update
elan default leanprover/lean4:stable

然后, lake 类比于 Cargo

lake new lean-snippet
cd lean-snippet
lake build
./.lake/build/bin/lean-snippet

顺便提一下本人的第一个 Lean4 PR 5789, 哈哈~

Functional Programming in Lean

Theorem Proving in Lean 4