Lean是什么？

Lean 是一门可作为交互式定理证明工具的函数式编程语言。

创建Lean项目

可以使用 lake 来创建一个新的 Lean 项目：

mkdir lean-playground && cd lean-playground
lake init foo

之后会得到下面的目录结构：

├── Foo
├── Foo.lean
├── lakefile.lean
├── lake-manifest.json
├── lean-toolchain
└── Main.lean

运行 lake build 可以构建并得到 foo 可执行文件。运行 ./build/bin/foo 会输出：

Hello, world!