使い方の入口 — 一つのファイルを検査するまで

Lean 本体を直接入れる必要はありません。入れるのは elan（Lean の公式配布元が用意している導入スクリプトで入ります）だけで、これが Lean の版を切り替えます。

仕組みが分かっていると迷いません。プロジェクトの一番上には lean-toolchain という一行のファイルがあります。

leanprover/lean4:v4.33.1

そのディレクトリで lean や lake を呼ぶと、elan がこの一行を読み、必要ならその版を自動で取ってきて、それを使います。プロジェクトごとに違う版が要っても、手で切り替える操作は出てきません。

mathlib を使うプロジェクトは重いです。Lean の版そのもので 3 GB ほど、mathlib のビルド済みの成果物で 9 GB ほどディスクを取ります。メモリは、証明の中身次第で 4 GB から 16 GB を見ておきます。

何かがうまく動かないとき、まず訊くのは版です。

elan --version
lean --version
lake --version

この説明のコード片をすべて検査した環境では、こう出ます。

elan 4.2.4 (227caca13 2026-08-25)
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
Lake version 5.0.0-src+819816b (Lean version 4.33.1)

mathlib の版は lean --version には出ません。プロジェクトの lake-manifest.json に、依存ごとの取得元と改訂が書かれています。この環境では次のとおりです。

この改訂の値が、結果を再現するための本体です。「Lean 4 で検査した」だけでは足りません。mathlib は補題の名前も定義も動くので、同じソースが半年後には通らないことがあります。lake-manifest.json を一緒に配れば、そこが固定されます。

myproject/
├── lakefile.toml        パッケージの名前・依存・オプション
├── lake-manifest.json   依存の改訂を一点に固定する（lake が書く）
├── lean-toolchain       Lean の版（elan が読む）
├── Foo.lean             ライブラリの入口。Foo/ 以下を import して並べるだけ
├── Foo/
│   ├── Bar.lean         中身
│   └── Baz.lean
└── .lake/               取得物とビルド結果の置き場（手で触らない）

lakefile.toml は短いもので済みます。

name = "myproject"
version = "0.1.0"
defaultTargets = ["Foo"]

[leanOptions]
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.33.1"

[[lean_lib]]
name = "Foo"

relaxedAutoImplicit = false は入れておく価値があります。これを緩めておくと、綴りを間違えた識別子が暗黙の型変数として黙って受け入れられ、意味の違う命題が検査を通ります。

依存を初めて取るとき、mathlib をソースから建てると数時間かかります。ビルド済みの成果物を取ってくると数分です。

lake exe cache get

これが取ってくるのは olean——検査済みの宣言を収めた中間ファイルで、import のときに読まれるものです。

ファイル一本だけを検査するなら、これです。

lake env lean Foo/Bar.lean

lake env は、そのプロジェクトの依存の在り処（mathlib の olean を探す道筋など）を環境変数に立ててから、続くコマンドを実行します。だから lean を直に呼ぶのではなく lake env lean を使います。

たとえば次のファイルを検査します。

import Mathlib

theorem add_self_even (n : ℕ) : 2 ∣ n + n := ⟨n, by ring⟩

出力は空です。それが「通った」という意味です。Lean は成功を報告しません。終了コードは 0 で、エラーがあれば 1 になります。この静かさに慣れるまでは落ち着きませんが、出力が空であることは強い情報です——検査すべき宣言がすべて型検査を通り、警告も一つも出なかった、ということです。

lake env lean と lake build の違いはひとつだけです。

重い証明を含むプロジェクトでは、lake build は既定で CPU の数だけ同時に建てます。一本で数 GB を使う証明があると、それだけでメモリが尽きて落ちもせず進みもしない状態になります。その場合は LEAN_NUM_THREADS で同時数を絞ります。

型が合わない

example (a b : ℕ) : a + b = b + a := Nat.add_comm b a

3:37: error: Type mismatch
  Nat.add_comm b a
has type
  b + a = a + b
but is expected to have type
  a + b = b + a

行 3 の 37 文字目、書いた項が Nat.add_comm b a、その型が b + a = a + b、求められている型が a + b = b + a。引数の順が逆でした。Nat.add_comm a b に直せば通ります。

「型が合わない」は、命題が偽だという報告ではありません。渡した項が、いま埋めたい穴の形と違う、というだけです。has type と but is expected to have type の二行を見比べるのが、この種のエラーの読み方です。

unsolved goals

theorem zero_both (n : ℕ) : n + 0 = n ∧ 0 + n = n := by
  constructor
  · rfl

3:53: error: unsolved goals
case right
n : ℕ
⊢ 0 + n = n

読み方は三段です。case right が閉じ残った枝の名前——constructor が連言を left と right の二つに割り、· で始めた枝で左だけを閉じたので、右が残っています。その下の n : ℕ が、その場所で使えるもの。⊢ の右が、示すべき命題です。

位置が行 3 の末尾（by のところ）を指すのは、個々の tactic ではなく証明全体としてゴールが残っていることの報告だからです。

ここには小さな教材が埋まっています。左の枝は rfl で閉じるのに、右の枝は閉じません。自然数の加法は第二引数について再帰的に定義されているので、n + 0 は定義の展開だけで n になりますが、0 + n はなりません。右には simp か Nat.zero_add が要ります。紙の上で対称に見えるものが、定義の上では対称でない——Lean で書き始めた人が最初に出会う段差です。

#check two_add_two
#check Nat.add_comm
#check (2 + 2 : ℕ)
#eval 2 + 2
#eval (List.range 10).map (· ^ 2)

two_add_two : 2 + 2 = 4
Nat.add_comm (n m : ℕ) : n + m = m + n
2 + 2 : ℕ
4
[0, 1, 4, 9, 16, 25, 36, 49, 64, 81]

#eval の結果は証明ではありません。コンパイル済みのコードで評価した値であって、kernel を通っていません。定義を書いたあとに「思ったとおりの値が出るか」を確かめるための道具で、計算の札と同じ重さです。値を主張にするなら、同じことを decide か明示的な証明で書き直します。

mathlib は 8,000 本を超えるファイルの集まりです。要る補題を見つける道は四つあります。

ゴールをそのまま閉じる補題を探す — exact?

example (a b : ℕ) : a + b = b + a := by exact?

Try this:
  [apply] exact Nat.add_comm a b

仮定を組み合わせて当てる — apply?

example (a b c : ℕ) (h : a ≤ b) (h2 : b ≤ c) : a ≤ c := by apply?

Try this:
  [apply] exact Nat.le_trans h h2

どちらも、見つかった項を そのまま書き写して置き換えます。exact? を証明に残したままにはしません——探索は毎回走るので検査が遅くなり、mathlib が動くと結果も変わります。

ソースを grep する

取得された mathlib は .lake/packages/mathlib/ に置かれています。名前の一部を思い出せるなら、宣言の行だけを拾うのが速いです。

grep -rnE "^(lemma|theorem) card_le_card_of_inj" .lake/packages/mathlib/Mathlib/

.lake/packages/mathlib/Mathlib/Data/Finset/Card.lean:427:lemma card_le_card_of_injOn (f : α → β) (hf : Set.MapsTo f s t) (f_inj : (s : Set α).InjOn f) :
.lake/packages/mathlib/Mathlib/Data/Finset/Card.lean:434:lemma card_le_card_of_injective {f : s → t} (hf : f.Injective) : #s ≤ #t := by
.lake/packages/mathlib/Mathlib/SetTheory/Cardinal/Finite.lean:94:lemma card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β)
.lake/packages/mathlib/Mathlib/SetTheory/Cardinal/Finite.lean:316:lemma card_le_card_of_injective {α β : Type*} {f : α → β} (hf : Injective f) : card α ≤ card β := by

同じ名前が別の名前空間に何度も現れることに注意してください。Finset のものと Nat.card のものと基数のもので、仮定も結論も違います。grep で当たりを付けたら、#check @その名前 で言明を確かめます。

名前から綴りを逆算する

mathlib の名前は、結論を英語の語で読み上げた形になっています。この対応を覚えると、探す前に名前が当たります。

読む向きは「結論 _of_ 仮定」です。Nat.eq_one_of_dvd_one は「1 を割るなら 1 に等しい」——

#check @Nat.eq_one_of_dvd_one

@Nat.eq_one_of_dvd_one : ∀ {n : ℕ}, n ∣ 1 → n = 1

読みどおりです。逆に、示したい式を add・le・comm の綴りに直してから探すと、当たりが早くなります。

このサイトの記事で Lean の札が付いた主張は、ソース一式が配布されています。手順・必要なメモリ・定理の台帳・依拠する公理の一覧は、Lean 検証一式 にあります。

一手で走らせる形が用意されていますが、中身は上で見たものと同じです——依存を固定した lake-manifest.json を使い、lake exe cache get で mathlib の olean を取り、lake build で順に建て、最後に #print axioms の出力を並べる。結果が食い違ったら、それが知りたいことです。連絡先はそのページにあります。

出典と再現

次は 03 有限の判定を decide に載せる——手を動かす最初の例。用語は 12 用語集。