---
title: "Lean4とは？入門・インストールからMathlib4・VSCode設定、最初の証明まで"
url: "https://www.issoh.co.jp/tech/details/8641/"
published: 2025-09-03
updated: 2026-10-13
categories: ["プログラミング言語"]
publisher: "株式会社一創"
---

# Lean4とは？入門・インストールからMathlib4・VSCode設定、最初の証明まで

Lean4は、数学の定理やプログラムの性質を形式的に書き、その証明が正しいかをコンピュータに検査させる**定理証明支援系**です。同時に、ネイティブコードへコンパイルできる**関数型プログラミング言語**でもあります。最新安定版は2026年10月12日公開の[Lean 4.35.0](https://github.com/leanprover/lean4/releases)です。

この記事では、ブラウザで試す方法、VS Code拡張とelanによるインストール、lakeでのプロジェクト作成、Mathlib4の導入、基本文法、タクティクで書く最初の証明までを順に扱います。掲載したLeanのコードとmacOS向けのコマンドは、2026年10月13日にmacOS（Intel）上で実行して出力を確かめたものです（Lean本体だけの例は4.35.0、Mathlibを使う例はMathlibが指定した4.35.0-rc4）。Windowsの手順は公式ドキュメントからの引用です。

## まとめ

Lean4は「型が命題、プログラムが証明」という考え方で動く言語です。`theorem`で書いた主張に証明が通ると、カーネルと呼ばれる小さな検査器が「その命題がその証明から導ける」ことを確かめます。保証されるのは書いた命題の証明までで、命題が意図した仕様を正しく表しているかは人間が確かめます。証明の途中経過はVS Code拡張のInfoviewに「残りのゴール」として表示されるので、対話しながら証明を組み立てられます。

- **まず試す**：インストール不要の[Lean 4 Web](https://live.lean-lang.org/)で書いてみる
- **入れる**：VS Codeに拡張「Lean 4」（`leanprover.lean4`）を入れ、セットアップガイドの「Install Lean」でelanを導入する
- **作る**：`lake new hello`でプロジェクトを作り、`lake build`でビルドする
- **数学をやる**：Mathlib入りのプロジェクトは`lake +leanprover-community/mathlib4:lean-toolchain new 名前 math`で作り、`lake exe cache get`でビルド済みファイルを取得する
- **証明する**：`rfl`・`decide`・`rw`・`induction`・`simp`・`omega`・`grind`から覚える

Lean本体の公開直後はMathlibの対応タグがまだ無く、手元のLeanの版で`lake new … math`を実行すると失敗します（後述の実測）。以下、概要から順に見ていきます。

## Lean4とは：定理証明支援系と関数型言語を兼ねる理由

### 定理証明支援系としてのLean

Leanでは、命題を型として書き、その型を持つ値を作ることが証明になります（Curry-Howard対応）。たとえば`2 + 2 = 4`は型であり、`rfl`はその型の値です。人間が書いた証明はカーネルが1ステップずつ検査するので、推論の途中に飛躍や見落としがあれば受理されません。ただし`sorry`や追加の公理に頼った宣言も警告付きで通るため、何に依存しているかは後述の`#print axioms`で確かめます。

```
theorem two_plus_two : 2 + 2 = 4 := rfl

theorem bad : 2 + 2 = 5 := by decide
-- error: Tactic `decide` proved that the proposition
--   2 + 2 = 5
-- is false
```

誤った主張は、このように検査の段階で拒否されます。紙の証明では読み手が行間を補いますが、Leanでは省略した推論ステップがあれば検査を通りません。

### プログラミング言語としてのLean

Leanは証明専用の道具ではなく、`IO`を扱う実行ファイルも作れる純粋関数型言語です。Lean自身のコンパイラやビルドツールLakeの大部分もLeanで書かれています。下は`lake new hello`が生成する`Main.lean`そのもので、ビルドすると`Hello, world!`を出力します。

```
import Hello

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"
```

「新世代の純粋関数型言語になれるか」という問いには、条件付きで「なれる」と答えられます。型クラス、`do`記法、ネイティブコンパイル、強力なマクロがそろっている一方、Webフレームワークやデータベースドライバなどのライブラリ群は[Haskellの得意分野](/tech/details/5055/)と比べてもまだ薄いのが現状です。業務アプリの主言語にするより、「仕様を証明しておきたい中核ロジック」をLeanで書く使い方が現実的です。

### 開発体制とLean 3からの移行

Leanは2013年にLeonardo de Moura氏がMicrosoft Researchで開発を始めた言語です。現在の開発は、2023年7月にde Moura氏とSebastian Ullrich氏が設立した[Lean FRO](https://lean-lang.org/fro/about/)（Convergent Research内の非営利組織）が主導しています。de Moura氏自身は[2023年にAWSへ移っており](https://leodemoura.github.io/about/)、「Microsoftのプロジェクト」という説明は現在は当てはまりません。ライセンスはApache-2.0です。

Lean 3とLean 4のコードには互換性がありません。構文もライブラリも作り直されており、Lean 3向けのmathlib3は2024年7月24日にアーカイブされました。検索で見つかる解説が`import data.nat.basic`のような小文字・ドット区切りのimportを使っていたら、それはLean 3時代の資料です。

### Leanの利用分野：数学の形式化・ソフトウェア検証・AI研究

主要な用途の1つが数学の形式化です。コミュニティが育てる数学ライブラリMathlibは、[公式の統計ページ](https://leanprover-community.github.io/mathlib%5Fstats.html)で定義137,943件・定理289,925件・貢献者772人（2026年10月13日取得）を数えます。ソフトウェア検証では、AWSの認可ポリシー言語Cedarの検証などが[公式サイト](https://lean-lang.org/)で事例として挙がっています。AIに数学の証明を書かせる研究でも、出力の正しさを判定する「答案用紙」としてLeanが使われています（[DeepSeekMathの自己検証の仕組み](/tech/details/10022/)も参照）。

## Lean 4 Webでのブラウザ実行（インストール不要）

インストール前に雰囲気をつかむなら、公式のオンラインエディタ[Lean 4 Web](https://live.lean-lang.org/)（live.lean-lang.org）が最短です。[lean4webのREADME](https://github.com/leanprover-community/lean4web)によると、Leanはブラウザ内ではなくWebサーバー側で動いており、最新のMathlibもインストール済みです。`import Mathlib`を書いた例もそのまま試せます。

ただしREADME自身が、本格的な開発や大きなプロジェクトは対象外と明記しています。数十行の練習や、勉強会でコードを見せる用途に留め、複数ファイルに分けて継続的に書くなら、ローカルに入れて使います。

## Lean4のインストール手順：VS Code拡張とelan

### 推奨手順：VS Code拡張「Lean 4」のセットアップガイド

[公式のインストールページ](https://lean-lang.org/install/)が推奨するのは、VS Codeと拡張機能「Lean 4」を使う方法です。

1. VS Codeをインストールする
2. 拡張機能で「lean4」を検索し、提供元leanproverの「Lean 4」（ID：`leanprover.lean4`）を入れる
3. 自動で開くセットアップガイドに従い、「Install Lean」ボタンでelan（Leanのバージョン管理ツール）を導入する

ガイドが開かない場合は、エディタ右上の∀アイコンから「Documentation」→「Docs: Show Setup Guide」で呼び出せます。elanはRustのrustupにあたる道具で、プロジェクトごとに必要なLeanの版を自動で取得・切り替えます。Lean本体を直接入れるのではなく、elan経由で入れるのが前提です。

### 手動インストール：elan-initのコマンド

ターミナルで入れる場合は、[手動インストールの公式手順](https://lean-lang.org/install/manual/)にあるelan-initを使います。macOSとLinuxは次の2行です。

```
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env
```

WindowsはPowerShellスクリプト版を取得して実行します。

```
curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1
```

VS Code拡張は`code --install-extension leanprover.lean4`でも入ります。公式は手動よりもセットアップガイドを強く勧めているので、PATHの設定などでつまずいたら推奨手順に戻るのが早道です。

### インストール後の確認とディスク容量

```
$ elan --version
elan 4.2.4 (227caca13 2026-08-25)
$ lean --version
Lean (version 4.35.0, x86_64-apple-darwin24.6.0, commit eb6cafb7290e, Release)
$ lake --version
Lake version 5.0.0-src+eb6cafb (Lean version 4.35.0)
```

elanは初回にLeanを呼び出したタイミングでツールチェーンをダウンロードします。手元ではLean 4.35.0を1つ入れた時点で`~/.elan`が2.8GBになりました。Mathlibを使うと、Mathlibが指定する別の版のツールチェーンも同じ場所に増えていきます。入っている版は`elan toolchain list`で確認でき、使われていないと判定された版は`elan toolchain gc`で一覧でき、`elan toolchain gc --delete`で削除できます。判定はelanを実行したことのあるディレクトリの`lean-toolchain`をもとにするので、削除前に一覧を確認してください。

## LakeによるLean4プロジェクトの作成とビルド

### lake newの5種類のテンプレート

Lakeは、Leanに同梱されているビルドツール兼パッケージマネージャです。`lake new 名前 テンプレート`で雛形を作ります。Lake 5.0.0の`lake new --help`が示すテンプレートは5種類です。

| テンプレート     | 中身                        | 使う場面         |
| ---------- | ------------------------- | ------------ |
| `std`（既定）  | ライブラリ＋実行ファイル              | 言語として学ぶ      |
| `exe`      | 実行ファイルのみ                  | CLIツール       |
| `lib`      | ライブラリのみ                   | 他から使う部品      |
| `math-lax` | ライブラリ＋Mathlib依存           | 数学を気軽に       |
| `math`     | Mathlib依存＋Mathlib流のlint設定 | Mathlib準拠で書く |

設定ファイルは既定でTOML形式の`lakefile.toml`です。`lake new hello std.lean`のように`.lean`を付けると、Leanで書く`lakefile.lean`になります。

### lake buildとlake exeによるビルドと実行

```
$ lake new hello
$ cd hello
$ lake build
✔ [8/8] Built hello:exe (2.0s)
Build completed successfully (8 jobs).
$ lake exe hello
Hello, world!
```

生成されるのは`lakefile.toml`、`lean-toolchain`、`Main.lean`、`Hello.lean`、`Hello/Basic.lean`などです。初回の`lake build`は手元で約13秒でした。ビルド成果物は`.lake/`に出力され、`.gitignore`にも最初から入っています。

### lean-toolchainによるLeanのバージョン固定

プロジェクト直下の`lean-toolchain`には`leanprover/lean4:v4.35.0`のように使う版が1行で書かれています。elanはこのファイルを読み、そのディレクトリでは指定の版を自動で使います。チームでLean本体の版をそろえるには、このファイルを共有すれば足ります。ただし版を上げるときは、Mathlibなどの依存も対応する版へ`lake update`で更新し、破壊的変更に合わせてコードを直してから再ビルドします。

## Mathlib4の導入と依存管理

### Mathlibの収録分野と数学向けタクティク

Mathlib（Lean 4版を指してMathlib4とも呼ばれます）は、集合・群・環・位相・測度・解析までをカバーするコミュニティの数学ライブラリです。自然数の足し算程度ならLean本体だけで証明できますが、実数・行列・素数などを扱う証明は事実上Mathlibが前提になります。`ring`・`linarith`・`norm_num`といった数学向けのタクティクも、Lean本体ではなくMathlib側にあります。

### 新規プロジェクトへのMathlib導入とキャッシュ取得の実測

公式手順は、MathlibのリポジトリにあるLeanの版を指定してプロジェクトを作る方法です。

```
lake +leanprover-community/mathlib4:lean-toolchain new my_math math
cd my_math
lake exe cache get
```

`lake exe cache get`は、Mathlibのビルド済みファイル（.olean）を一括でダウンロードするコマンドです。キャッシュを取得していない状態で`lake build`すると、依存するMathlibのモジュールを手元でコンパイルし始め、何時間もかかることがあります。

2026年10月13日に手元（macOS・Intel）で実行した結果は次のとおりです。Lake 5.0.0では`lake new … math`の時点でMathlibの取得とキャッシュの展開まで進み、続けて実行した`lake exe cache get`は「No files to download」で約30秒で終わりました。

| 項目                        | 実測値                    |
| ------------------------- | ---------------------- |
| Mathlibが指定したLeanの版        | v4.35.0-rc4            |
| `lake new … math`の所要時間    | 5分48秒（rc4ツールチェーンの取得込み） |
| 取得したキャッシュ                 | 9,004ファイル              |
| プロジェクトの`.lake`            | 7.5GB（うちmathlib 6.8GB） |
| `import Mathlib`するファイルの検査 | 初回約2分10秒、2回目約34秒       |

今回の環境では、Mathlibのプロジェクト1つとツールチェーン2版（4.35.0とrc4で計5.6GB）を合わせて13GB前後のディスクを使いました。`.lake`はプロジェクトごとに作られるので、練習用のプロジェクトは1つにまとめてファイルを足していくほうがディスクを節約できます。`import Mathlib`を書いたファイルで`ring`・`norm_num`・`linarith`・`by_contra`を使う例も、この環境で通ることを確かめています。

```
import Mathlib

example (a b : ℝ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by ring
example : Nat.Prime 101 := by norm_num
example (x y : ℝ) (h₁ : x < y) (h₂ : 0 < x) : 0 < y := by linarith
```

### 失敗例：Lean公開直後のMathlib対応タグ不足

先頭の`+leanprover-community/mathlib4:lean-toolchain`を省くと、手元の既定の版（ここでは4.35.0）でプロジェクトが作られ、`lakefile.toml`に`rev = "v4.35.0"`が書き込まれます。Lean 4.35.0公開の翌日（2026年10月13日）の時点では、Mathlibにまだ`v4.35.0`タグが無く、`lake update`は次のエラーで止まりました。

```
$ lake new mymath math
$ cd mymath && lake update
info: leanprover-community/mathlib: fetching revision 'v4.35.0' from https://github.com/leanprover-community/mathlib4
fatal: couldn't find remote ref v4.35.0
error: leanprover-community/mathlib: failed to fetch the package revision
```

同じ時点のMathlibの`lean-toolchain`は`v4.35.0-rc4`で、タグも`v4.35.0-rc4`までしかありませんでした。Mathlibが本体の正式版に追いつく時期は一致しないことがあるので、Mathlibを使うプロジェクトでは手元の最新版ではなく「Mathlibが今使っている版」に合わせるのが原則です。公式手順の`+…:lean-toolchain`はそのための指定です。

### 既存プロジェクトへのMathlib追加とバージョン整合

`std`テンプレートで作ったプロジェクトに後から入れる場合は、`lakefile.toml`に依存を書き足し、`lean-toolchain`をMathlibと同じ版にそろえてから更新します。

```
[[require]]
name = "mathlib"
scope = "leanprover-community"
```

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

`lake update`は依存の版を解決して`lake-manifest.json`を書き換えます。Mathlibを更新するたびにLean本体の版も上がることがあるので、更新後はもう一度`lake exe cache get`を実行します。

### 定理の探し方：exact?・Loogle・ドキュメント

Mathlibの定理は数十万件あり、名前を覚えるより探し方を覚えるほうが早く進みます。証明の途中で`exact?`と書くと、今のゴールを閉じられる定理を探して提案してくれます。`exact?`はLean本体に入っているので、Mathlibが無くても使えます。

```
example (a b : Nat) : a + b = b + a := by exact?
-- Try this:
--   [apply] exact Nat.add_comm a b
```

型の形から定理を検索するなら[Loogle](https://loogle.lean-lang.org/)、名前空間から一覧を引くなら[Mathlibのドキュメント](https://leanprover-community.github.io/mathlib4%5Fdocs/)を使います。

## VS CodeでのLean4開発：Infoviewと記号入力

### Infoviewの仮定・ゴール表示の読み方

拡張を入れた状態で`.lean`ファイルを開き、`by`以下にカーソルを置くと、右側のInfoviewにその位置での仮定とゴールが表示されます。たとえば二重否定の証明で`intro h`まで進めると、次のように表示されます。

```
P : Prop
h : ¬¬P
⊢ P
```

`⊢`の上が使える仮定、下が示すべきゴールです。タクティクを1行書くたびにこの表示が変わるので、「次に何を示せばよいか」を常に確認しながら進められます。エラーは該当行に赤線で示され、すべてのゴールが閉じると「No goals」になります。

### 記号の入力方法：バックスラッシュ略語

Leanのコードには→や∀などの記号が出てきますが、キーボードから直接打つ必要はありません。拡張はバックスラッシュに続けて略語を打つと記号に置き換えます。

| 入力        | 記号 | 入力        | 記号 |
| --------- | -- | --------- | -- |
| `\to`     | →  | `\N`      | ℕ  |
| `\and`    | ∧  | `\or`     | ∨  |
| `\not`    | ¬  | `\forall` | ∀  |
| `\exists` | ∃  | `\iff`    | ↔  |
| `\le`     | ≤  | `\ne`     | ≠  |

対応表は拡張のソース（vscode-lean4の`abbreviations.json`）で確認しました。記号にマウスを乗せると入力方法がツールチップで出るので、他人のコードを写すときも困りません。VS Code以外では、EmacsとNeovimにもコミュニティ製の拡張があります。

## Lean4の基本文法

### def・#eval・#checkと型

`def`で定義し、`#eval`で評価、`#check`で型を確認します。`#`で始まるコマンドの結果はInfoviewに出ます。

```
def answer : Nat := 42
#eval answer + 1      -- 43
#check answer         -- answer : Nat
#eval 7 / 2           -- 3
#eval (7 : Float) / 2 -- 3.500000
```

型は`名前 : 型`の形で書き、省略できる場面では型推論が補います。整数リテラルは既定で`Nat`（自然数）になるので、`7 / 2`は切り捨てて3です。

### Natの切り捨て減算とIntとの違い

```
#eval (5 : Nat) - 10  -- 0
#eval (5 : Int) - 10  -- -5
```

`Nat`には負の数が無いため、引き算は0で止まります（切り捨て減算）。証明で「`a - b + b = a`」が常には成り立たない（`b ≤ a`のときだけ成り立つ）のはこのためで、初学者が最初にはまる箇所です。負の数が要る計算では最初から`Int`を使います。

### 関数・パターンマッチ・再帰

```
def double (n : Nat) : Nat := 2 * n

def fact : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * fact n

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

#eval fact 10  -- 3628800
#eval fib 20   -- 6765
```

引数の形で場合分けするパターンマッチで、再帰関数を素直に書けます。Leanは再帰が必ず止まることを確かめてから定義を受け付けます。`fact n`の呼び出しは引数が1つ小さくなっているので、自動で停止性が示されます。止まることを示せない再帰には、`termination_by`で減っていく量を指定するか、`partial`を付けて停止性の証明を省きます（その代わり、証明の中で関数の中身を展開して使えなくなります）（再帰そのものの考え方は[再帰関数の仕組みとスタック・末尾再帰](/tech/details/15264/)で扱っています）。

### 高階関数とラムダ式

```
def applyTwice {α : Type} (f : α → α) (x : α) : α := f (f x)

#eval applyTwice (· + 3) 10                  -- 16
#eval applyTwice (fun s => s ++ "!") "Lean"  -- "Lean!!"
#eval [1, 2, 3, 4].map (fun x => x * x)      -- [1, 4, 9, 16]
#eval [1, 2, 3, 4].filter (· % 2 == 0) |>.foldl (· + ·) 0  -- 6
```

`{α : Type}`の波かっこは暗黙引数で、呼び出し側では型を書かずに推論させます。`(· + 3)`は`fun x => x + 3`の短縮記法です。`map`・`filter`・`foldl`の考え方は他の関数型言語と共通なので、[関数型プログラミングの純粋関数・高階関数](/tech/details/4841/)の知識がそのまま使えます。

### structureによる構造体定義とReprによる表示

```
structure Point where
  x : Float
  y : Float
deriving Repr

#eval ({ x := 1.5, y := 2.0 } : Point)  -- { x := 1.500000, y := 2.000000 }
```

`deriving Repr`を付けると、`#eval`で中身を表示できるようになります。複数の場合を持つ型は`inductive`で定義します。

## 最初の定理の証明：タクティクの基本

証明は`theorem 名前 : 主張 := 証明`の形で書きます。`by`の後ろに「タクティク」と呼ばれる命令を並べると、ゴールを少しずつ変形して閉じていけます。この章のコードはすべてLean本体だけで通り、Mathlibは使っていません。

### rflとdecideによる計算を使った証明

```
theorem my_mul_zero (n : Nat) : n * 0 = 0 := rfl

example : 2 + 2 = 4 := by decide
```

`n * 0 = 0`は、自然数の掛け算が2番目の引数で定義されているため、両辺を計算するだけで一致します。`rfl`は「両辺が計算上等しい」ことを示す証明です。`decide`は具体的な値どうしの命題を計算で真偽判定します。

### inductionとrwによる帰納法と式の書き換え

一方、引数の順序を入れ替えた`0 * n = 0`は`rfl`では閉じません。既存の補題を使う`simp`なら一手で通りますが、ここでは仕組みを見るために帰納法で証明します。

```
theorem my_zero_mul (n : Nat) : 0 * n = 0 := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.mul_succ, ih]
```

`induction n with`で`n = 0`の場合と`n = k + 1`の場合に分かれます。`succ`の場合のゴールは`0 * (k + 1) = 0`で、`rw [Nat.mul_succ]`で`0 * k + 0 = 0`に書き換え、帰納法の仮定`ih : 0 * k = 0`で書き換えると閉じます。`n * 0`と`0 * n`で`rfl`が通るかどうかが分かれるのは、定義がどちらの引数で場合分けしているかで決まるからです。

### simp・omega・grindの自動証明と適用対象

```
example (a b : Nat) (h : a < b) : a + 1 ≤ b := by omega
example (a b c : Nat) : a + b + c = c + b + a := by omega
example (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length := by simp
example (a b : Nat) (h₁ : a = b) (h₂ : b = 3) : a + 1 = 4 := by grind
```

`omega`は整数・自然数の線形算術（足し算と定数倍、不等式）を自動で解きます。`simp`は登録された書き換え規則で式を簡約します。`grind`はSMTソルバーに着想を得た自動証明のタクティクで、[Lean 4.16.0（2025年2月）](https://lean-lang.org/doc/reference/latest/releases/v4.16.0/)に開発中の機能として入り、現在は仮定から等式をたどる証明を一手で閉じます。学習の初期は自動化に頼りすぎず、`rw`や`induction`で手を動かして、Infoviewのゴールの変化を見たほうが理解が進みます。

### 古典論理の証明：Lean本体とMathlibの背理法の違い

「¬¬PならばP」のような背理法を使う証明では、ネット上の解説によく`by_contra`が出てきます。ところがMathlibを読み込まずにLean 4.35.0で`intro h`→`by_contra nP`→`exact h nP`と書くと、`by_contra`の行が`unknown tactic`になりました。`by_contra`はMathlib側で提供されるタクティクだからです。Lean本体だけで通る書き方は次のとおりです。

```
theorem double_negation (P : Prop) : ¬¬P → P := by
  intro h
  exact Classical.byContradiction h
```

Lean本体だけで書くなら、上のように`Classical.byContradiction`を使うか、`by_cases hp : P`で場合分けします。Mathlibを読み込んでいれば`by_contra nP`と書けます。読んでいる解説のコードが通らないときは、まずそれがMathlib前提の記事かどうかを疑ってください。

### sorryと#print axiomsによる未完成部分・依存公理の確認

```
theorem todo (n : Nat) : n + 0 = n := by sorry
-- warning: declaration uses `sorry`

#print axioms my_zero_mul      -- 'my_zero_mul' does not depend on any axioms
#print axioms double_negation  -- depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms todo             -- depends on axioms: [sorryAx]
```

`sorry`は「証明はあとで書く」という仮置きで、警告は出ますがファイル全体のチェックは通ります。そのため、他人の「Leanで証明済み」を信用する前に`#print axioms`で依存を確かめます。`sorryAx`が出たら未完成です。それ以外に見慣れない公理（`axiom`で独自に追加したものなど）が並んでいないかも確認します。`Classical.choice`が出るのは古典論理を使った証明で、誤りではありません。

## メタプログラミングとmacroによる構文拡張

Leanでは、構文やタクティクそのものをLeanで追加できます。最小の例は`macro`による記法の追加です。

```
macro "twice! " n:term : term => `(2 * $n)
#eval twice! 21  -- 42
```

Mathlibの`ring`や`linarith`も、この仕組みでLean自身に書かれたタクティクです。分野ごとの記法（DSL）や独自の自動証明を足せることが、Leanを数学とソフトウェア検証の両方に広げた理由の1つです。入門段階では「標準のタクティクもユーザーが書いたコードである」と知っておけば十分です。

## Lean 4.35.0の主な変更点

[4.35.0のリリースノート](https://lean-lang.org/doc/reference/latest/releases/v4.35.0/)によると、この版には214件の変更が入りました。入門者に関係するものを挙げます。

- **vcgen**：命令的なプログラムの検証条件を生成する`mvcgen`の後継。`mvcgen`は非推奨に
- **lake check**：プロジェクトをビルドして書き出し、カーネルで検査し直す。標準以外の公理を使っているとエラー
- **lake comparator**：証明が与えられた命題と一致するかを照合する
- **Decidableの定義変更**：`Bool`と証明を持つ構造体になり、`rfl`で閉じる等式が増えた
- **constructorの警告**：複数の構成子が当てはまるときに警告。従来の動きは`constructor!`

`lake check`は検査対象のコードを`bwrap`のサンドボックスで動かす設計です。macOSで実行すると「`bwrap`, which needs Linux namespaces」というエラーで止まりました。macOSで使う場合はLinuxのコンテナやCI上で走らせる前提になります。

## Lean4を学ぶべき人と、向かない場面

Leanが向いているのは、次のどれかに当てはまる人です。

- 数学の証明を機械で検査したい、またはMathlibの形式化に参加したい
- AIが生成した証明やコードの正しさを判定する仕組みを作りたい
- 暗号・認可・プロトコルなど、間違えたときの損失が大きいロジックの仕様を証明しておきたい

逆に、テストを手厚くすれば足りるWebアプリの品質確保が目的なら、Leanから入るのは遠回りです。まず[プロパティベーステスト](/tech/details/16259/)で性質を書く習慣を付けるほうが、導入コストに対する効果は大きくなります。他の証明支援系との比較では、既存の大規模な検証資産（CompCertなど）を使うならRocq（旧Coq）、seL4のようなOS検証の蓄積を使うならIsabelleが候補になります。新しく数学を形式化する、AIと組み合わせる、という目的ならMathlibの規模と更新頻度からLeanを選んでよいでしょう。

学習教材は、公式の[Theorem Proving in Lean 4](https://lean-lang.org/theorem%5Fproving%5Fin%5Flean4/)（定理証明）と[Functional Programming in Lean](https://lean-lang.org/functional%5Fprogramming%5Fin%5Flean/)（プログラミング）、Mathlibで数学を書く[Mathematics in Lean](https://leanprover-community.github.io/mathematics%5Fin%5Flean/)が定番です。日本語では、有志による翻訳や解説をまとめた[lean-ja](https://lean-ja.github.io/)から入れます。ゲーム感覚で自然数の公理から証明を積み上げる[Natural Number Game](https://adam.math.hhu.de/)はブラウザ上で動くので、インストール前にタクティクの感覚をつかむ教材に向いています。数式を美しく書く側の道具は[LaTeX](/tech/details/9718/)で、Leanとは役割が違います。

## よくある質問

### Lean4はインストールせずにブラウザで試せますか？

試せます。公式のLean 4 Web（live.lean-lang.org）を開けば、環境構築なしでコードを書いて検査結果を確認できます。Leanはブラウザ内ではなくサーバー側で動いており、Mathlibもインストール済みです。大きなプロジェクトは対象外なので、続けて学ぶならローカルに入れてください。

### Lean4とLean3のコードに互換性はありますか？

ありません。構文もライブラリも作り直されており、Lean 3向けのmathlib3は2024年7月24日にアーカイブされました。`import data.nat.basic`のような小文字のimportを使う資料はLean 3時代のものです。

### Lean4は今もMicrosoftのプロジェクトですか？

違います。2013年にMicrosoft Researchで始まった言語ですが、現在は2023年7月に設立された非営利組織Lean FRO（Convergent Research内）が開発を主導しています。ライセンスはApache-2.0です。

### Mathlib4は必ず導入する必要がありますか？

必須ではありません。プログラミングや自然数・リストの基本的な証明はLean本体だけで書けます。実数・代数・解析を扱う場合や、`ring`・`linarith`・`by_contra`などを使いたい場合にMathlibが必要になります。

### VS Code以外のエディタでもLean4を使えますか？

使えます。EmacsとNeovimにはコミュニティ製のLean 4用プラグインがあり、Language Server経由でゴール表示もできます。ただし公式のセットアップガイドとInfoviewの体験はVS Code拡張が最も整っているため、最初はVS Codeから始めるのが確実です。

## 関連記事

- [DeepSeekMathとは？V2の自己検証の仕組みとIMO 2025実績・2024年版7Bとの違い](/tech/details/10022/)
- [関数型プログラミングとは？純粋関数・不変性・高階関数をTypeScriptの実例で解説](/tech/details/4841/)
- [Haskellの得意分野とは？金融・ブロックチェーンで使われる理由と向かない場面](/tech/details/5055/)
- [ゼロ知識証明（ZKP）とは？仕組みとzk-SNARKを実際に動かして解説](/tech/details/8735/)
- [LaTeXとは？読み方・TeXとの違い・使い方を初心者向けにわかりやすく解説](/tech/details/9718/)

---

出典: [Lean4とは？入門・インストールからMathlib4・VSCode設定、最初の証明まで](<https://www.issoh.co.jp/tech/details/8641/>)（株式会社一創）