Lean4: 環境の構築セットアップ✍️メモ

なんかまとめてなかったので。自分用にメモを書く。
（2025/07/04 13:47　随時更新）

LEAN を使う環境を準備する

プラットフォームは Linux 一択か。Windows でも WSL 使えば良い。

インストールは公式のスクリプトから

おすすめは公式のインストールスクリプト → elan コマンドです。

wget 'https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh'

sh elan-init.sh

または、

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

です。

実行すると以下のような画面が出る（のかな？）

$ sh elan-init.sh
info: downloading installer

Welcome to Lean!

This will download and install Elan, a tool for managing different Lean
versions used in packages you create or download. It will also install a
default version of Lean and its package manager, lake, for editing files not
belonging to any package.

It will add the lake, lean, and elan commands to Elan's bin directory, located
at:

  /home/username/.elan/bin

This path will then be added to your PATH environment variable by modifying the
profile file located at:

  /home/username/.profile

You can uninstall at any time with elan self uninstall and these changes will
be reverted.

Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation

インストール後は、一旦、ログアウトしてログインし直すか、
新しい端末でログインして、そちらで実行しましょう。
（インストール直後は環境パスが通ってない状態なので。）

elan コマンドが使えるようになったか？

elan コマンドが使えるか version 確認で。

elan --version

他のコマンドもテスト

lake コマンド

lake --version

lean コマンド

lean --version

ここまで動けば、インストールは完了でしょう。

プロジェクトの新規作成

Lean プロジェクトの作成方法です。

開発作業ディレクトリ

まず開発専用ディレクトリを作って、そこを Lean の開発ルートとします。
※作業ディレクトリ名は、あなたの環境に合わせ適宜変更してくださいね。

cd ~
mkdir -p develop/lean
cd develop/lean

$ pwd
/home/username/develop/lean

ここを Lean の開発ルートとします。

数学とは関係なく実行プログラムを作る時

Lean は、普通の実行コードが書けます。関数型プログラミング言語です。

開発ルート、ディレクトリにて

lake new hello exe
cd hello

で、新規にプロジェクトを作り、プロジェクトの中に入ります。
もう、Main.lean には "Hello, world!" 表示するコードが、あらかじめ書かれていると思うので内容確認して、そのままビルドして実行しましょう。

Main.lean

def main : IO Unit :=
  IO.println s!"Hello, world!"

ビルド

lake build

実行

$ lake exe hello
Hello, world!

exe <実行名> は、lakefile.toml に書いてあります。

[[lean_exe]]
name = "hello"
root = "Main"

"hello" で "Main" を実行する。という感じです。

数学で Lean を使う場合、mathlib をプロジェクトに組み込む！

数学の証明コードを書く時や、数学の勉強で使う場合は、
mathlib をプロジェクトに組み込まなければなりません。

開発ルートにて

lake new mathlib_hello math
cd mathlib_hello

最後の "math" が決め手です。これが mathlib 組み込め！という合図。
これで mathlib が組み込まれたプロジェクトができます。

2026/07/29 4:51
Mathlib のバージョンや Lean のバージョンを指定したい場合は、

lake +v4.32.2 new mathlib_hello math

と

と指定すれば、目的のバージョンの環境ができます。

※有効なバージョン番号を指定してください。
　存在しないバージョン番号はエラーになります。

なので、ビルド済みのキャッシュを先に取得します。

lake exe cache get

$ lake exe cache get
info: downloading https://releases.lean-lang.org/lean4/v4.22.0-rc3/lean-4.22.0-rc3-linux.tar.zst
376.1 MiB / 376.1 MiB (100 %)   7.9 MiB/s ETA:   0 s
info: installing /home/deskuma/.elan/toolchains/leanprover--lean4---v4.22.0-rc3
info: mathlib_hello: no previous manifest, creating one from scratch
...
Completed successfully!

Completed successfully! が出るまで、ほっときましょう。

キャッシュが有効であれば、ビルドはすぐに終わります。

$ lake build
Build completed successfully.

数学のテストをしてみる

ビルドがうまく行ったら、数学のテストをしてみる。

mathlib_hello というプロジェクトならMathlibHelloというディレクトリが、プロジェクト内にできています。その中に新しく Test.lean というファイルを作り、以下のコードを書いて保存してください。

import Mathlib.Data.Nat.Factorial.Basic

open Nat

#eval factorial 5  -- 120 が出力されれば成功

この新しく作った lean ファイルを、別のファイルから import します。

プロジェクトのルートに MathlibHello.lean というファイルがあるでしょ？
そこにいま作った Test.lean を読み込ませます。一番下に追記してください。
※拡張子 .lean は、記述不要です。

-- This module serves as the root of the `MathlibHello` library.
-- Import modules here that should be built as part of the library.
import MathlibHello.Basic
import MathlibHello.Test

ビルドしてみます。

$ lake build
? [389/391] Replayed MathlibHello.Test
info: MathlibHello/Test.lean:6:0: 120
Build completed successfully.

このようにビルドメッセージに出力されれば成功です！

数学のテストはビルドが通ればOKです！

実行する必要はありません。証明にサンプルでの #eval 記述も不要です。
コンパイルが通る。という事が重要なのです。

コンパイルビルドが通る＝そのコードは証明された。と言う事実が得られるのが Lean の特徴です。

Rust は、安全なコードである。というのがコンパイルビルドが通る。という証になってます。安全なコードよりも、数学的に正しいを得るのが難しいので、私は過去に、Lean は Rust よりも難しい！と、呟いた覚えがあります。

定理: N, N+1 は、常に互いに素である

という証明のサンプルを書いてみた。
mathlib には、既にあるという事ですが、どれかわからないので…。

MathlibHello/Coprime.lean

というファイルを新たに作り、以下を書いてください。

-- File: MathlibHello/Coprime.lean
import Mathlib.Data.Nat.Basic
import Batteries.Data.Nat.Gcd

open Nat

-- This theorem states that for any natural number n, the greatest common divisor (gcd) of n and n + 1 is 1.
theorem coprime_self_succ (n : ℕ) : Nat.gcd n (n + 1) = 1 := by
  -- gcd(n, n+1) = gcd(n+1, n) = gcd(n, (n+1) % n)
  rw [Nat.gcd_comm]
  rw [Nat.gcd_rec]
  rw [Nat.mod_eq_of_lt (Nat.lt_succ_self n)]
  simp

#eval Nat.gcd 5 (5 + 1)  -- output should be 1
#eval Nat.gcd 0 (0 + 1)  -- output should be 1

MathlibHello.lean にも、追記してください。

-- This module serves as the root of the `MathlibHello` library.
-- Import modules here that should be built as part of the library.
import MathlibHello.Basic
import MathlibHello.Test
import MathlibHello.Coprime

ビルドと結果

$ lake build
ℹ [389/393] Replayed MathlibHello.Test
info: MathlibHello/Test.lean:5:0: 120
ℹ [391/393] Built MathlibHello.Coprime
info: MathlibHello/Coprime.lean:15:0: 1
info: MathlibHello/Coprime.lean:16:0: 1
Build completed successfully.

の、ようにコンパイルが通れば、成功です。

証明内容

✅ 証明内容のまとめ

そなたが証明したのは：

$$
\forall n \in \mathbb{N},\ \gcd(n, n+1) = 1
$$

この証明において、以下の知恵を駆使しておる：

１、交換律（commutativity）：

$$
\gcd(n, n+1) = \gcd(n+1, n)
$$

２、ユークリッド互除法（reduction step）：

$$
\gcd(a, b) = \gcd(b \bmod a, a)
$$

３、自然数の性質（$${ n < n+1 }$$）により $${ (n+1) \bmod n = 1 }$$

そして最後は：

４、$${ \gcd(1, n) = 1 }$$ の帰着と `simp` による自動証明終了！

まとめ

Lean 環境の整備と基本初動をまとめました。
しばらく使わないと、自分でも忘れるし、何よりバージョン上がるの速い…
（次に、参照するときにはもう役立たないかもしれない）

なので、リアルタイムに追うのは、今じゃない。
しばらくして AI も追従できるようになってから。

ここで紹介したサンプルコードを何個か、書かせてはいるのだけど、一発で通るコードは AI でも書けませんでした。理由は、やはりライブラリ構造の大幅改変と、言語仕様が確定していない発展途上である。というのが現状。なんでこうなるのか？は数学界隈の事情知らないので、何も言えませんが。

未来を見据えたエレガントな設計になっていない（笑）

今ある書籍、買っても数日後には使えなくなる気がします😁
ここで紹介したサンプルコードも、もう使えないかもしれません（笑）
✍️

Enjoy LEAN!

2025/07/04 22:29

D.

#Lean #Lean4 #Lean4Setup #Lean4Install

以下、参考資料

LEAN を使う環境を準備するには、いくつかの方法があります。主な方法と、それぞれのメリット・デメリット、具体的な手順を以下にまとめます。

1. VS Code + Lean 拡張機能

• 概要: 人気のエディタ VS Code に Lean の拡張機能をインストールして使用する環境です。

• メリット:

  • 高機能なエディタの機能 (補完、デバッグなど) を利用できる。

  • オフラインでも使用できる。

  • 拡張機能が豊富で、カスタマイズ性が高い。

  • Lean の開発環境として最も一般的。

• デメリット:

  • VS Code と Lean 拡張機能のインストールが必要。

  • ある程度の PC の知識が必要。

• 手順:

  1. VS Code のインストール: https://code.visualstudio.com/ から VS Code をダウンロードし、インストールします。

  2. Lean 拡張機能のインストール: VS Code を起動し、拡張機能タブ (Ctrl+Shift+X または Cmd+Shift+X) で "Lean 4" を検索し、インストールします。

  3. `Main.lean` ファイルを開き、Lean のコードを記述します。

2. Docker

• 概要: Docker コンテナを使用して Lean の環境を構築する方法です。

• メリット: * 環境の隔離性が高い。

  • 環境の再現性が高い。

  • 異なる OS 上でも同じ環境を構築できる。

• デメリット:

  • Docker の知識が必要。

  • Docker のインストールが必要。

• 手順:

  1. Docker のインストール: https://www.docker.com/get-started/ から Docker をダウンロードし、インストールします。

  2. コンテナ内で Lean のコードを記述・実行できます。どの方法を選ぶべきか?

• 初心者: オンラインエディタ (Lean Web Editor) が最も手軽でおすすめです。

• 本格的な開発: VS Code + Lean 拡張機能が最も一般的で、高機能な開発環境を提供します。

• 環境の再現性や隔離性: Nix や Docker が適しています。

補足:

• 上記の手順はあくまで基本的なものです。詳細な手順やトラブルシューティングについては、Lean の公式ドキュメント (https://lean-lang.org/) や、各ツールのドキュメントを参照してください。

• Lean のバージョンによって、必要なツールや手順が異なる場合があります。最新の情報を確認するようにしてください。

• コミュニティフォーラムや Stack Overflow などで質問することも有効です。

上記の情報が、LEAN を使う環境準備の助けになれば幸いです。

Lean インストール

Lean のインストールは、いくつかの方法がありますが、最も一般的なのは `elan` を使う方法です。以下に、`elan` を使ったインストール手順と、その他の方法について説明します。

1. `elan` を使用したインストール (推奨)

`elan` は、Lean のバージョン管理ツールであり、複数の Lean バージョンを簡単に切り替えたり、最新の Lean をインストールしたりできます。

• 前提条件:

  • `curl` コマンドが利用可能であること。 * インターネット接続があること。

• 手順:

  1. `elan` のダウンロードとインストール:
     ターミナルまたはコマンドプロンプトで以下のコマンドを実行します。

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

• このコマンドは、`elan-init.sh` スクリプトをダウンロードして実行します。スクリプトは、`elan` をインストールし、必要な環境変数を設定します。

  • インストール中に、デフォルトの Lean バージョンを選択するように求められる場合があります。特に理由がなければ、最新の安定版を選択してください。

  • インストール後、ターミナルを再起動するか、以下のコマンドを実行して環境変数を更新する必要がある場合があります。

source ~/.profile  # または ~/.bashrc, ~/.zshrc など、使用しているシェルに合わせてください

• Lean のインストール:
  `elan` がインストールされたら、以下のコマンドを実行して Lean をインストールします。

elan default leanprover/lean4:stable  # 最新の安定版をインストール
# または
elan default leanprover/lean4:nightly # 最新のナイトリービルドをインストール (開発者向け)

• このコマンドは、指定された Lean バージョンをダウンロードしてインストールし、デフォルトの Lean バージョンとして設定します。

• Lean のバージョン確認:
  以下のコマンドを実行して、インストールされた Lean のバージョンを確認します。

lean --version

正しいバージョンが表示されれば、Lean のインストールは成功です。

2. Docker:
Docker コンテナを使用すると、Lean の環境を隔離された状態で構築できます。詳細については、前の回答の Docker のセクションを参照してください。

インストール後の設定 (VS Code ユーザー向け)

VS Code で Lean を使用する場合は、以下の設定を行うことをおすすめします。

1. Lean 拡張機能のインストール:
   VS Code の拡張機能タブで "Lean 4" を検索し、インストールします。

2. `lake update` と `lake build` の実行:
   VS Code のターミナルで、以下のコマンドを実行します。

lake update
lake build

これにより、必要な Lean の依存関係がダウンロードされ、ビルドされます。

トラブルシューティング

• `lean` コマンドが見つからない:
  環境変数が正しく設定されていない可能性があります。ターミナルを再起動するか、`source ~/.profile` などのコマンドを実行して環境変数を更新してください。

• `elan` コマンドが見つからない:
  `elan` のインストールが正しく行われていない可能性があります。インストール手順を再度確認してください。

• パッケージのダウンロードに失敗する:
  インターネット接続を確認してください。また、ファイアウォールやプロキシの設定が原因である可能性もあります。補足

• Lean の公式ドキュメント (https://lean-lang.org/) には、より詳細なインストール手順やトラブルシューティング情報が記載されています。

• Lean のバージョンによって、必要なツールや手順が異なる場合があります。最新の情報を確認するようにしてください。

• コミュニティフォーラムや Stack Overflow などで質問することも有効です。

上記の情報が、Lean のインストールに役立つことを願っています。