Lean + Mathlib + VS Code の環境を構築してみる

環境

MacOS

% sw_vers
ProductName:            macOS
ProductVersion:         15.6.1

とはいえ Mac に限らず、　Windows や Linux でも同じ手順で環境構築できるように整備されているはず。

VS Code はインストール済み。

% code --version
1.123.0
6a44c352bd24569c417e530095901b649960f9f8
arm64

インストール

• VS Code で動作する
• https://github.com/leanprover/elan
  • elan という独自のパッケージマネージャーで管理されるらしい

拡張機能をインストールしたら以下のような VS Code 内のセットアップガイドが表示された。これに従いインストールする。

% lean --version
Lean (version 4.30.0, arm64-apple-darwin24.6.0, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release)

プロジェクトを作成

様々な数学的な対象を扱えると噂の Mathlib を触ってみたい。なので今回は Create a new project using Mathlib を選択した。

Mathlib がインストールされていないとのプロンプトが表示されたが、　OK をクリックすると自動的にインストールされ始めた。

---

プロジェクトが作成できました

次のステップ

環境構築はできたので以下の動画を参考にして数学の証明を試してみたいと思います。

体系的に学ぶには以下のドキュメントを読むのが良さそうです。
https://leanprover-community.github.io/mathematics_in_lean/

(おまけ) Mathematics in Lean を読む環境の構築

VS Code 内の Lean のアイコンから Download Project を選択。

Mathematics in Learn を選択すると例題をダウンロードできる。

ローカルで色々試しながら学べる。