Lean 工具链是一组命令行工具，用于检查证明并编译由多个 Lean 文件组成的程序。 工具链由 elan 管理；它会按需安装工具链。 Lean 工具链采用自包含设计，大多数命令行用户除了 lake 和 elan 之外，无需显式调用其中的其他工具。 其中包含以下工具：

lean

Lean 编译器，用于精译和编译 Lean 源文件。

lake

Lean 构建工具，在跟踪依赖关系的同时增量调用 lean 和其他工具。

leanc

Lean 随附的 C 编译器，它是 Clang 的一个版本。

leanmake

make 构建工具的一种实现，用于编译 C 依赖项。

leanchecker

一种通过 Lean 内核重放 .olean 文件中精译结果的工具，为所有项均已得到正确检查提供额外保证。