lean4怎么安装mathlib

Lean 4 是一个开源的依赖于 Lean 3 的静态类型理论编程语言和环境，它支持数学证明和开发工具。MathLib 是 Lean 4 中的一个重要库，包含了大量的数学定理和数据结构。

要在 Lean 4 中安装 MathLib，你需要按照以下步骤操作：

1. **安装 Lean 4**: 首先确保你已经安装了 Lean 4。你可以从 Lean 4 的官方网站下载适用于你操作系统的版本，例如通过 `curl` 或者通过安装包（如在 Linux 上的 snap 包或 macOS 的 brew 安装）。

2. **设置 Lean 工作空间 (Workspace)**: 创建一个新的 Lean 工作空间，比如 `my_workspace`，可以创建一个名为 `init.lean` 的入口文件。

3. **添加依赖**:
- 打开终端或命令行，在工作空间根目录下运行:

     leanproject get mathlib

这会从 GitHub 获取最新的 MathLib，并将其作为一个项目加入到你的 Lean 工作空间中。

4. **引用库**:
在你的 `.olean` 文件或 `main.lean` 中，添加对 MathLib 的导入：

   import mathlib.data.nat.primes

这将引入数学库中的自然数质数部分。

5. **编译和验证**:
使用 Lean 编译器 `lean` 编译并验证你的代码:

   lean run main.lean

注意：如果你初次接触 Lean，可能需要一些时间理解和适应它的语法以及IDE配置。此外，MathLib经常更新，所以确保总是获取最新版的库。