Lean 是什么
Lean 是一门可作为交互式定理证明工具的函数式编程语言。
Lean 的安装
首先安装 Lean 的版本管理器 elan：
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
然后使用 elan 安装：
elan self update
elan default leanprover/lean4:stable
创建 Lean 项目
可以使用 lake 来创建一个新的 Lean 项目：
mkdir lean-playground && cd lean-playground
lake init foo
之后会得到下面的目录结构：
├── Foo.lean
├── lakefile.lean
└── Main.lean
运行 lake build 可以构建并得到 foo 可执行文件。运行 ./build/bin/foo 会输出：
Hello, world!
使用 Lean 进行定理证明
可以参考 Theorem Proving in Lean 4 学习。
网友评论