[环境配置]Mathlib4安装和简单使用测试

git clone firc-dataset

发布于 2025-07-22 13:02:45

8970

我们从上海交通大学镜像站克隆 Mathlib 仓库。打开一个新的终端，运行

git clone https://mirror.sjtu.edu.cn/git/lean4-packages/mathlib4/

等待克隆完成：

在你的项目文件夹下，使用终端运行

lake update
lake exe cache get
lake build

如果你看到终端中显示了类似如下的提示：

Decompressing 1234 file(s)
unpacked in 12345 ms

同时你的项目文件夹中出现了lake-packages文件夹，那么证明你安装Mathlib成功了，重启系统即可使用。

这里提供一个实例来测试你的安装：

import Mathlib.Data.Real.Basic
example (a b : ℝ) : a * b = b * a := by
  rw [mul_comm a b]

如果你的Lean infoview没有任何报错，并且光标放在文件最后一行时会提示“No goals”，证明你的Mathlib已经正确安装了。

如果你想更新Mathlib，在终端中运行

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

本文参与腾讯云自媒体同步曝光计划，分享自作者个人站点/博客。

原始发表：2024-10-18，如有侵权请联系 cloudcommunity@tencent.com 删除