この説明の全体

用語集

この説明に出てくる語を 43 語。かなの語を 50 音順に、記号と英字の語をアルファベット順に並べています。右の欄が、その語を詳しく扱っているページです。

かなの語

語	説明	詳しく
穴	証明の未完成な箇所。Lean では `sorry` を置いて残す。置いた定理は `#print axioms` に `sorryAx` が出て、何も主張していない状態になる。	01
陰性対照	仮定を外すと言明が偽になることを、わざと Lean に書いて確かめること。定義が強すぎて何でも通る状態や、要らない仮定が紛れている状態を見つけるために置く。	09
型	対象や命題の種類を表すもの。Lean では命題そのものが型で、その型を持つ項が証明にあたる。`ℕ`（自然数）・`ℚ`（有理数）・`ℝ`（実数）も型。	01
仮定	定理が前提に置いた条件。Lean では引数として書かれるので、`#check` で言明を出せば全部見える。仮定を足すほど定理は弱くなる——読むときに数える対象。	08・09
機械検査	証明の項が本当にその型を持つことを kernel が確かめること。保証されるのは「書かれた言明が、書かれた定義と列挙された公理から導ける」ことだけ。	01
項	型を持つ式。証明は項である。補題を使うことは、その補題の項に引数を渡すことと同じ形で書かれる。	01
公理	証明せずに受け入れる命題。Lean と mathlib で普通に出るのは `propext`・`Classical.choice`・`Quot.sound` の三つ。どれに依拠しているかは定理ごとに機械が答える。	01
証明書 certificate	探索の結果として見つかった答えを、検査しやすい形——木の形・整数の上下界・写像の表など——に書き出したもの。探索そのものは Lean の外で行い、証明書だけを Lean に確かめさせる。	07
全数列挙	候補を残らず挙げること。挙げた候補が条件を満たさないことは Lean で言えるが、候補がそれで尽きていることは多くの場合 Lean の定理の外にある。	09・10
定理	`theorem` で宣言された、名前の付いた命題とその証明。Lean の札に定理名を添えるのは、名前を辿れば言明が読めるようにするため。	09
標準三公理	`propext`・`Classical.choice`・`Quot.sound` のこと。依拠する公理がここに収まっていることが Lean の札の条件のひとつ。	01
命題	真偽を問える言明。Lean では型として書かれ、その型は `Prop` に属する。	01
連結版	複数のファイルに分かれた証明を、依存の順に一本にまとめたもの。受け取った側が自分の環境で通しで検査し直すときに使う。	09

記号と英字の語

語	説明	詳しく
`Classical.choice`	選択の公理。空でない型から要素をひとつ取り出せる。排中律の出所なので、背理法を使うと入る。	01
`decide`	判定手続きを kernel に走らせて命題を閉じる tactic。`Decidable` が付いている命題にだけ使える。対象が大きいと展開の深さやメモリで止まる。	03
`Decidable`	その命題の真偽を有限手続きで決められることを表す型クラス。`decide` が使えるかどうかは、これが付いているかで決まる。付いていなければ自分で書く。	03・11
`elan`	Lean の版を管理する道具。プロジェクトの `lean-toolchain` の一行を読み、必要ならその版を自動で取ってくる。	02
`exact?` `apply?`	ゴールをそのまま閉じる補題／仮定を組み合わせて当てられる補題を、mathlib から探す tactic。見つかった項は書き写して置き換え、呼び出しは証明に残さない。	02
`Finset`	有限集合の型。要素数 `#s`、和 `∑ x ∈ s, f x`、絞り込み `s.filter p` が使える。数え上げをそのまま証明の対象にできる。	04
`Fintype`	その型の要素が有限個で、全部並べられることを表す型クラス。`Fintype.card` で要素数が取れ、`∀` や `∃` が判定可能になる。	04
kernel	型検査だけを行う小さな中核。tactic が組み立てた項は、必ず最後にここを通る。信頼しなければならないのは、kernel の実装と公理と、命題の書き方だけ。	01
`lake`	依存の取得とビルドを行う道具。`lake exe cache get` で mathlib のビルド済み olean を取り、`lake build` で順に建てる。	02
`lake env lean`	ファイル一本を検査する呼び方。`lake env` が依存の在り処を環境変数に立て、そのうえで `lean` を走らせる。出力が空なら通った。	02
`lakefile.toml` `lake-manifest.json` `lean-toolchain`	プロジェクトの三点。順に、名前と依存の指定／依存の改訂の固定／Lean の版。結果を再現するにはこの三つが要る——「Lean 4 で検査した」だけでは足りない。	02
`LEAN_NUM_THREADS`	同時に建てるファイルの数を決める環境変数。一本で数 GB を使う証明があるプロジェクトでは、絞らないとメモリが尽きて進まなくなる。	02・11
`linarith`	線形の不等式を、与えられた仮定の線形結合として閉じる tactic。非線形の項は、先に置き換えておく必要がある。	06
Mathlib	Lean 4 の数学ライブラリ。8,000 本を超えるファイルからなる。補題の名前も定義も改訂で動くので、配るときは改訂を固定する。	02
`maxRecDepth`	項の展開の深さの上限。`decide` を大きな対象に当てると `maximum recursion depth has been reached` で止まる。上げれば進むこともあるが、たいていは書き方を変えるほうが速い。	01・11
`native_decide`	判定を機械語にコンパイルして走らせ、その結果を公理として受け入れる tactic。速い代わりに信頼の範囲がコンパイラと実行環境まで広がる。このサイトでは使わない。	01
`norm_num`	数値を含む式を正規形に直して閉じる tactic。具体的な数の等式・不等式に強い。	01
olean	検査済みの宣言を収めた中間ファイル。`import` のときに読まれる。mathlib のものを取ってくれば、ソースから建て直さずに済む。	02
`omega`	整数と自然数の線形算術を決定手続きで閉じる tactic。加減と定数倍、`≤`、剰余の一部まで。自然数の引き算の切り捨ても正しく扱う。	11
`Prop`	命題の型が属する宇宙。`Prop` の要素が命題で、命題の要素がその証明。	01
`propext`	命題外延性の公理。互いに同値な二つの命題は等しい。命題を等式として書き換える操作がここに依拠するので、`simp` を使うとほぼ入る。	01
`Quot.sound`	商の健全性の公理。商をとったとき、同値な代表元は等しい。有理数や有限多重集合のように商で作られた型を触ると入る。	01
`rfl`	両辺が定義の展開で同じ形になることを主張する項。公理を一つも使わない。定義の対称性が崩れると使えなくなる（`n + 0` は閉じるが `0 + n` は閉じない）。	02
`ring`	可換環の等式を、展開と整理で閉じる tactic。分数が混ざるときは `field_simp` で分母を払ってから当てる。	11
`simp`	書き換え規則を繰り返し当てて式を単純化する tactic。mathlib が持っている規則集を使う。何を使ったかは `simp?` で出せる。	11
`sorry`	証明の穴。置くと declaration uses `sorry` という警告が出て、検査自体は先へ進む。エラーだけを見ていると見落とす。	01
`sorryAx`	`sorry` が立てる公理。あらゆる命題を証明してしまうので、これが出た定理は何も言っていない。	01
tactic	証明の項を組み立てるプログラム。`by` の後に書く。作った項は kernel が検査するので、tactic の誤りが定理の誤りになるとは限らない。逆に、失敗しても命題が偽であることにはならない。	01
`#check` `#eval`	項の型を出す／計算して値を出す。`#check` に定理名を渡すと言明がそのまま出る。`#eval` の結果は証明ではない——kernel を通らないので、計算と同じ重さ。	02
`#print axioms`	その定理が依拠する公理を並べる。穴（`sorryAx`）と `native_decide` を見つけるいちばん確実な手。公理を使わない定理では `does not depend on any axioms` という別の言い回しになる。	01

よく出る tactic を一枚で

上の表に出た tactic を、それぞれが得意な形のゴールと並べたものです。

import Mathlib

-- Decidable が付いているか確かめてから decide を当てる
example : Decidable (3 ∣ 12) := by infer_instance
theorem three_dvd_twelve : 3 ∣ 12 := by decide

-- Finset と Fintype
#eval (Finset.range 10).filter (fun n => n % 3 = 0)
#eval (Finset.range 10).sum id
#eval Fintype.card (Fin 5 × Fin 3)

-- simp（規則の書き換え）
example (x : ℕ) : x + 0 = x := by simp

-- ring（可換環の等式）
example (x y : ℤ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by ring

-- omega（整数・自然数の線形算術）
example (a b : ℕ) (h : a + 3 ≤ b) : a < b := by omega

-- linarith（仮定の線形結合で不等式を閉じる）
example (x y : ℝ) (h1 : x ≤ y) (h2 : 0 ≤ x) : 0 ≤ 2 * y := by linarith

-- norm_num（具体的な数の式）
example : (7 : ℝ) / 2 < 4 := by norm_num

#eval の三行の出力：

{0, 3, 6, 9}
45
15

残りの宣言は出力を出しません。02 のとおり、出力が空であることが「通った」という意味です。

出典と再現

もの	種別	出典・道具
§03 のコード片と出力	機械検査	Lean 4.33.1 ＋ mathlib（改訂 `0df444a3…`）で検査し、出力をそのまま写した
公理・tactic の名前と役割	既知	Lean 4 の中核と mathlib
このサイトの定理が依拠する公理	機械検査	Lean 検証一式の台帳

改訂 2026-09-20：初版。43 語。