Executive Summary

忙しくて本文をお読みになれない方のために、本稿の内容をここにまとめます。

本文だけをお読みになる方は、この節を読み飛ばしても差し支えございません。
本文は、この節を読んでいなくても理解できるように書いてあります。

本稿の問い

依存型（dependent type）という言葉を、お聞きになったことがあるでしょうか。

型の中に、値が現れる型のことです。

たとえば「長さが3のリスト」という型を書けます。
3という値が、型の一部になっています。

Haskell でも、型レベル自然数を使えば似たことができます。
Vec 3 Int のような型を作った経験をお持ちの方もおられるでしょう。

本稿の問いは、次のものです。

依存型で表現できることが、実際の数学の定理の形式化で、どう使われているのか。

本稿の結論

結論として、3点を先にお伝えします。

（1つ目）

依存型は、数学の定理の形式化で、実際に広く使われています。

行列の次元、有限集合の添字、剰余群、実数の定義。
いずれも依存型の機能が支えています。

（2つ目）

ただし、「何でも型に載せればよい」わけではありません。

「長さが3である」という性質を型に載せることも、命題として別に持ち運ぶこともできます。
mathlib は、多くの場面で後者を選んでいます。

（3つ目）

その選択には、はっきりした理由があります。

数学では、途中で性質が変わる操作が頻繁に現れます。

たとえば、2つのリストを連結すれば長さが変わります。
リストを並べ替えれば、整列済みという性質が失われたり、新たに得られたりします。
そのたびに型が変わると、前に証明した定理が使えなくなるのです。

本稿で扱う2つの表

本稿では、表を2つに分けて掲載します。

表	内容
表1	実際に形式化された事例が確認できたもの。典拠を示します
表2	筆者が「使えるはずだ」と推測したもの。実際の事例は確認できていません

この区別を設けた理由は、「使えるはずだ」という推測と、「実際に使われた」という事実を、読者が取り違えないようにするためです。

本稿の論旨の流れ

本稿の位置づけ

依存型の機能を紹介する記事ではありません。

その機能が、実際の数学の定理の形式化で、どう使われたかを示す記事です。

筆者が「この定理の証明に使えるはずだ」と判断したものと、過去に実際に検査された実績があるものを、厳密に区別します。

想定読者

本稿は、次のような方を想定しています。

Haskell を書いた経験があり、型レベル自然数に触れたことがある方
定理証明支援系（Lean 4、Isabelle、Rocq など）を学び始めたばかりの方
依存型という言葉は知っているが、実際に何の役に立つのかを知りたい方

前提とする知識

プログラムを書いた経験
型があることの意味（コンパイルのときに型が検査される、など）

前提としない知識

依存型を使った経験
mathlib を読んだ経験
圏論の知識

本稿から得られること

依存型の機能が、実際の数学の定理の形式化でどう使われたかが分かります
「型に載せる」と「命題にする」の違いと、その使い分けが分かります
形式化の実績を、自分で調べる方法が分かります

本稿のコードについて

本稿に掲載するコードには、2種類あります。

ひとつは、mathlib から引用したコードです。
ソースコードを読んで転記しました。ファイル名と行番号を示します。
ただし、筆者の手元でビルドしたものではありません。

もうひとつは、筆者が書いたコードです。
こちらは mathlib を使わず、Lean 4 単体で動くように書き、実機で型検査を通しました。

第1章　依存型とは何か

1-1　Haskell の型レベル自然数から入る

関数型言語を書かれる皆様には、なじみ深い話題から始めさせてください。

リストの先頭を取り出す関数を考えてください。

head :: [a] -> a

この関数には、問題があります。

空のリストを渡すと、実行時にエラーになります。
型を見ただけでは、その危険が分かりません。

そこで、リストの長さを型に書き込む、という発想が生まれます。

data Vec (n :: Nat) a where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n + 1) a

Vec 3 Int と書けば、長さがちょうど3の整数のリストを表します。

【上級者向けコラム】HaskellのVecを実際に動かすには

本文のHaskellコードは、長さを型に書く発想を見せるための例です。そのままGHCで実行するには、GADT、型レベル自然数、型レベル演算に関する言語拡張やimportが必要になります。

ここでの比較の主題は、Haskellの実行環境の準備ではなく、「長さを型に書く」という発想をLean 4の Nat → Type へつなぐことです。

この型を使えば、先頭を取り出す関数を、次のように書けます。

vhead :: Vec (n + 1) a -> a

空のリストを渡そうとすると、コンパイルが通りません。

Vec 0 a は Vec (n + 1) a と型が合わないためです。

1-2　依存型では、もっと素直に書ける

Haskell で型レベル自然数を使った経験がある方なら、書くのが面倒だった記憶があるかもしれません。

型と値が別の世界に分かれているため、行き来するのに手間がかかります。

依存型を持つ言語では、この区別がありません。

Lean 4 で同じものを書くと、次のようになります。

inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

Nat → Type という部分に注目してください。

自然数を受け取って、型を返す。
これが、依存型の姿です。

先頭を取り出す関数は、次のように書けます。

def vhead {α : Type} {n : Nat} (v : Vec α (n + 1)) : α :=
  match v with
  | Vec.cons x _ => x

Vec.nil の場合を書いていないことに注目してください。

引数の型が Vec α (n + 1) なので、空のリストは、そもそも渡せません。
場合分けを書く必要がないのです。

実際に使ってみます。

def sample : Vec Nat 3 :=
  Vec.cons 1 (Vec.cons 2 (Vec.cons 3 Vec.nil))

#eval vhead sample

1 が表示されます。

このコードは、実機で型検査を通しました。
使用した処理系の版は、本稿の末尾に記載します。

【上級者向けコラム】依存型における「依存関数（Π型）」と「依存ペア（Σ型）」

型理論の専門的な文脈では、「依存型」は主に2つの基本的な構成子によって語られます。

依存関数型（Dependent Function Type / Π型）：引数の「値」によって戻り値の「型」が変わる関数の型です。本文で紹介した Nat → Type や、長さに応じたベクトルを返す関数などはすべてこのΠ型にあたります。
依存ペア型（Dependent Pair Type / Σ型）：1つ目の要素の「値」によって、2つ目の要素の「型」が決まるペアです。「ある長さ n」と「その長さ n を持つベクトル」をひとまとめにした組 (n : Nat) × Vec α n などがこれに相当します。

本文の地の文では、最も直感的に理解しやすい「値を受け取って型を返す関数（型コンストラクタ）」に焦点を当てていますが、数学の定理を記述する際には、これらΠ型とΣ型が背後で縦横無尽に組み合わされています。

1-3　長さが合わないと、どうなるか

次のコードを書くと、どうなるでしょうか。

def wrong : Vec Nat 3 := Vec.cons 1 (Vec.cons 2 Vec.nil)

要素が2つしかないのに、Vec Nat 3 と宣言しています。

コンパイルが通りません。

型検査の段階で、Vec Nat 2 と Vec Nat 3 が違うと判定されます。

これが、「型に載せる」ということです。

第2章　型に載せるか、命題にするか

2-1　型に載せるとは、どういうことか

Vec A 3 という型を考えてください。
この型の値は、必ず長さ3のリストです。

長さ4のリストを Vec A 3 として扱おうとすると、コンパイルが通りません。
型検査の段階で拒否されます。

つまり、「長さが3である」という事実が、型そのものに書き込まれています。

2-2　命題にするとは、どういうことか

一方、mathlib では次のように書きます。

xs : List A
h : xs.length = 3

xs は、ただのリストです。
長さの情報を持っていません。

そのうえで、h という別の値を用意します。
これは「xs の長さは3である」という証明です。

リストと、その性質の証明を、別々に持ち運ぶわけです。

実際に書いてみます。

def sampleList : List Nat := [1, 2, 3]

theorem sampleLength : sampleList.length = 3 := rfl

rfl は reflexivity（反射律）の略で、「同じものは同じである」という、もっとも基本的な証明です。

sampleList.length を計算すると 3 になるため、これだけで証明が済みます。

このコードも、実機で型検査を通しました。

2-3　Haskell で言い換えると

	Haskell での近いもの
型に載せる	型レベル自然数を使い、`Vec 3 a` という型を作る
命題にする	ただの `[a]` を使い、「長さ3である」ことは別に確かめる

Haskell で型レベル自然数を使った経験がある方なら、書くのが面倒だった記憶があるかもしれません。

Vec 3 a と Vec 4 a を連結すると Vec 7 a になる。
これを型検査器に納得させるには、3 + 4 = 7 を型のレベルで示す必要があります。

2-4　2つの方式を、表で比べる

	型に載せる	命題にする
間違いに気づく時期	型検査のとき	証明を書くとき
書きやすさ	型が合わない箇所が増える	性質を後から付け足せる
向いている場面	性質が変わらない場合	操作のたびに性質が変わる場合

【上級者向けコラム】なぜすべてを型検査器に背負わせないのか ── 停止性と自動化のトレードオフ

「何でも型に載せれば、バグが型検査の時点で100%防げて最高ではないか」と思えるかもしれません。しかし、これを行き過ぎて行うと、コンパイラ（型検査器）がパンクします。

依存型言語において、型の中に任意のプログラム（式）を埋め込めるようにすると、原理的に「型が等しいかどうかを判定する問題」がチューリング完全になり、型検査が停止しない（または実用的な時間で終わらない）危険性が生じます。

そのためLeanなどのシステムでは、型検査器が行う計算（Definitional Equality）はシンプルな簡約規則に限定し、複雑な等式変形や性質の証明は simp や omega、ring といった専用のタクティク（証明スクリプト）に任せるアーキテクチャを採っています。「命題として外に出す」設計は、証明支援系の動作を軽快に保ち、高度な自動証明系を効率よく働かせるための現実的な知恵でもあるのです。

2-5　「性質を後から付け足せる」とは、どういうことか

表の「書きやすさ」の欄に、「性質を後から付け足せる」と書きました。

これが何を意味するのか、実際のコードでご覧いただきます。

-- リストをふつうに作る。長さのことは、まだ考えていない
def xs : List Nat := [3, 1, 2]

-- あとから、長さについての性質を付け足す
theorem xsLength : xs.length = 3 := rfl

-- さらにあとから、別の性質も付け足せる
theorem xsNotEmpty : xs ≠ [] := by simp [xs]

-- 並べ替えても、リストの型は変わらない
def ys : List Nat := xs.mergeSort (· ≤ ·)

-- 並べ替えた結果についても、性質を付け足せる
theorem ysLength : ys.length = 3 := by
  simp [ys, xs]

このコードで、後から付け足した性質を、表にまとめます。

定理の名前	付け足した性質
`xsLength`	`xs` の長さは3である
`xsNotEmpty`	`xs` は空のリストではない
`ysLength`	`xs` を並べ替えた `ys` も、長さは3である

最初の1行に、注目してください。

def xs : List Nat := [3, 1, 2]

この1行は、ただ「3、1、2 という3つの数を並べたリスト」を作っているだけです。

List Nat という型には、長さの情報も、空でないという情報も含まれていません。

そのうえで、必要になった時点で、必要な性質だけを定理として書き足しています。

長さが必要になれば xsLength を、空でないことが必要になれば xsNotEmpty を証明する。
使わない性質は、証明しなくてよいのです。

型に載せる場合は、こうはいきません。

inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- 型に載せる場合、作る時点で長さを決めなければならない
def vs : Vec Nat 3 :=
  Vec.cons 3 (Vec.cons 1 (Vec.cons 2 Vec.nil))

Vec Nat 3 と書く時点で、長さが3だと宣言しています。

長さを間違えれば、その場でコンパイルが通りません。
「あとで考える」ことが、できないのです。

このコードは、いずれも実機で型検査を通しました。

どちらを選ぶかは、設計の判断です。

なぜ mathlib が命題を選ぶことが多いのかは、第5章で実機のコードとともにご説明します。

【上級者向けコラム】「型に載せる」と「命題にする」は二者択一ではない

本文では「型に載せる」と「命題にする」を対比しています。

実際の Lean / mathlib では、この2つを完全に二分しているわけではありません。

Subgroup G は、単純な Subtype そのものではなく、部分群として必要なデータと証明を持つ構造体です。また Fintype は具体的な有限性のデータを持つ一方、Finite は「有限である」という命題です。

さらに、型クラス、構造体、Subtype、Sigma、Prop の命題などを組み合わせて、必要な情報だけを持たせることもできます。

実際の設計では、計算に必要な情報なのか、証明にだけ必要な情報なのか、自動的に探してほしい情報なのか、といった観点から選択されます。

本稿の第7章では、Fintype と Finite を例に、この選択が実際の形式化でどう働いたかを見ます。

第3章　実際に形式化された事例（表1）

ここからが、本稿の中心です。

依存型の機能が、実際の数学の定理の形式化で、どう使われたかを示します。

3-1　表1　過去に形式化の実績が確認できたもの

依存型の機能	何を型で表現するか	数学の定理証明での実際の使われ方	典拠
行列の次元	次元が合わない積が書けない	`Matrix m n α` は添字を型で指定する。乗算の型が `HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)` と宣言されており、次元が合わない積は型検査で拒否されます	mathlib `Mathlib/Data/Matrix/Mul.lean` 302行
有限集合の添字（`Fin n`）	範囲外のアクセスが型で防がれる	`Fintype.card (Fin n) = n`。行列の添字、群の位数に使われています。`ZMod n` は、`n` が0でないとき `Fin n` として定義されています	mathlib `Mathlib/Data/Fintype/Card.lean` 497行、`Mathlib/Data/ZMod/Defs.lean` 138行
有限性を持ち運ぶ（`Fintype`）	「この型は有限である」というデータを、型クラスとして持つ	位数 pq の群の分類（2025）で中心的に使用。`Fintype`（データ）と `Finite`（命題）の使い分けが形式化の設計を左右しました。Lagrange の定理の型が `Fintype.card` から `Nat.card` へ変更された経緯も論じられています	S. Harper, P. Wu, arXiv:2501.09769
商型（`Quotient`）	「同値なものを同一視した型」を作る	剰余群、加群のテンソル積、環の余極限、Stone-Čech コンパクト化、Cauchy 完備化、実数と p 進数の定義、基数の定義に使われています。幾何代数の形式化では、テンソル代数の商として多重ベクトルを定義しました	mathlib の論文（CPP 2020）、arXiv:2110.03551
部分型（`Subtype`）	「条件を満たす要素だけ」を型にする	部分群 `Subgroup G` は、台集合 `carrier` と、それが条件を満たすことの証明を組にした構造体として定義されています。Lagrange の定理（`card_subgroup_dvd_card`）で使われています	mathlib `Mathlib/Algebra/Group/Subgroup/Defs.lean` 296行、`Mathlib/GroupTheory/Sylow.lean` 838行
等しさを持ち運ぶ（`Eq`）	等しさの証明を、値として関数に渡す	`Fintype.equiv_of_card_eq`（同じ濃度の有限型は同値）	mathlib のドキュメント
型クラスによる代数構造	「この型は群である」「体である」を型に載せる	Cap Set 問題の形式化で、mathlib の線形代数と多変数多項式を使用。半群からモノイド、群、環、体、ネーター環、単項イデアル整域まで	arXiv:1907.01449
宇宙レベル	型の階層を型として扱う	Lean は proof irrelevance、quotient types、non-cumulative universes を持ちます。完備離散付値環と局所体の形式化、アーデル環の形式化で使われています	arXiv:2310.01998、arXiv:2203.16344
依存型による分類定理の記述	「ある次元と、その次元の構造」を型で扱う	3次元以下の可解 Lie 環の分類（2025）。基底の添字を型で扱い、次元ごとの場合分けを行いました	arXiv:2505.19975

【上級者向けコラム】表①の項目は一種類の仕組みではない

表①は「Leanで数学を形式化するとき、型やその周辺の仕組みが実際にどう役立つか」を広く見渡す表です。行列の次元や Fin n は、値に応じて型が変わる例です。一方、型クラス、商型、宇宙レベルなどは、数学的な構造や形式化の基盤に関わる例です。

これらをすべて「同じ種類の依存型機能」と呼ぶ必要はありません。本稿では、それぞれが実際の形式化で果たした役割を確認するため、同じ表に載せています。

3-2　表1に出てくる数学の定理を、先に説明します

表1には、数学の定理や概念の名前が並んでいます。

数学を専門になさっていない読者のために、それぞれが何であるかを、先に説明します。

位数 pq の群の分類

「群」とは、何でしょうか。

足し算や掛け算のような演算が1つ決まっていて、いくつかの条件を満たすものです。

条件	内容
演算が閉じている	2つを組み合わせると、また同じ仲間になる
単位元がある	組み合わせても何も変わらないものが1つある（足し算なら0、掛け算なら1）
逆元がある	組み合わせると単位元に戻るものが、どれにも1つある

時計の文字盤を思い浮かべてください。

12時間で一周します。
「3時間進める」「5時間進める」を組み合わせると「8時間進める」になります。

これも群です。

「位数」とは、その群に含まれる要素の個数です。

時計の例なら、0から11までの12個。位数は12です。

「位数 pq の群の分類」という定理は、次のことを述べます。

p と q が素数のとき、要素が pq 個の群は、どういうものがありうるか。それをすべて列挙する。

たとえば p = 2、q = 3 なら、要素が6個の群です。
そういう群は、2種類しかないことが知られています。

「分類する」とは、「ありうるものを、すべて数え上げる」ということです。

Lagrange の定理

群の中に、小さな群が含まれていることがあります。 これを部分群と呼びます。

時計の例で考えます。

12時間の文字盤の中に、「0時、4時、8時」だけを取り出したものを考えてください。
4時間ずつ進める操作だけを使えば、この3つのあいだを行き来できます。

これも、それ自体が群になっています。 つまり部分群です。

Lagrange の定理は、次のことを述べます。

部分群の要素の個数は、元の群の要素の個数を割り切る。

時計の例なら、部分群の要素は3個、元の群は12個。
3は12を割り切ります。

この定理があるおかげで、「位数6の群に、位数4の部分群はありえない」といったことが、すぐに分かります。

Cap Set 問題

これは、組合せ論の問題です。

カードゲームの「セット」をご存じでしょうか。

3枚のカードが特定の条件を満たすと「セット」になる、というゲームです。

Cap Set 問題は、次のことを問います。

「セット」が1つもできないように、カードを選ぶとしたら、最大で何枚選べるか。

この問題は、2016年に大きく進展しました。

それまで知られていた上限より、はるかに小さい上限が示されたのです。
その証明が、2019年に Lean で形式化されました。

なぜ形式化したのか。 証明が短く、しかし巧妙だったため、機械で確かめる価値があったのです。

3次元以下の可解 Lie 環の分類

「Lie 環」（リー環）とは、何でしょうか。

ベクトルの空間に、特殊な掛け算を入れたものです。

ふつうの掛け算と違い、順序を入れ替えると符号が変わります。

物理学で、回転や対称性を扱うときに現れます。

「可解」とは、ある操作を繰り返すと、いずれ何もなくなる性質のことです。

「3次元以下の可解 Lie 環の分類」は、次のことを述べます。

次元が1、2、3のそれぞれについて、可解 Lie 環はどういうものがありうるか。それをすべて列挙する。

位数 pq の群の分類と、同じ形の定理です。

「ありうるものを、すべて数え上げる」という点で共通しています。

アーデル環

整数を素数で割った余りを考えることがあります。

2で割った余り、3で割った余り、5で割った余り。
それぞれ別の世界です。

アーデル環は、これらの世界をすべて束ねたものです。

数論で、複数の素数について同時に考えたいときに使われます。

非常に大きな構造であるため、形式化するのが難しい対象です。

完備離散付値環と局所体

「ある素数で何回割り切れるか」を測る仕組みを、付値と呼びます。

12は2で2回割り切れます。
18は2で1回割り切れます。

この「何回割り切れるか」を使って、数の近さを測ることができます。

局所体は、このような測り方のもとで、隙間がないようにした数の世界です。

実数が有理数の隙間を埋めたものであるのと、似た発想です。

テンソル積、余極限、Stone-Čech コンパクト化、Cauchy 完備化、基数

これらは、いずれも「何かから、新しいものを作る」構成です。

構成	どういう操作か
テンソル積	2つの空間から、より大きな空間を作る
余極限	複数のものを貼り合わせて、1つにする
Stone-Čech コンパクト化	無限に広がる空間に、「果て」を付け加えて閉じる
Cauchy 完備化	隙間のある数の世界に、隙間を埋める。有理数から実数を作る操作がこれ
基数	「要素の個数」を、無限の場合まで広げた概念

いずれも、「同値なものを同一視する」という操作を含みます。

そのため、7-4 で扱う商型が使われます。

3-3　いくつかの事例を、詳しく見る

行列の次元

mathlib の行列の乗算は、次のように定義されています。

instance [Fintype m] [Mul α] [AddCommMonoid α] :
    HMul (Matrix l m α) (Matrix m n α) (Matrix l n α) where
  hMul M N := fun i k => (fun j => M i j) ⬝ᵥ fun j => N j k

出典：
mathlib4、Mathlib/Data/Matrix/Mul.lean、302行目から304行目
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Matrix/Mul.lean

型に注目してください。

Matrix l m α と Matrix m n α を掛けると、Matrix l n α になります。

真ん中の m が共通していることが、型のレベルで要求されています。

数学では「$l \times m$ 行列と $m \times n$ 行列の積は $l \times n$ 行列」と書きます。
その決まりが、そのままコードになっています。

次元が合わない2つの行列を掛けようとすると、型検査の段階で拒否されます。

【上級者向けコラム】Matrixの行と列は添字の型で表せる

本文では Matrix l m α を「l行m列の行列」と読みました。通常の有限行列なら、この理解で十分です。

より一般には、l と m は行と列を指定する添字の型として使われます。たとえばn個の行を持つ場合は Fin n を添字にできます。

乗算の型で真ん中の添字 m が一致することが重要です。これによって、行と列の組み合わせが合わない行列の積を型で防げます。

有限集合の添字と、剰余環

ZMod n（整数を n で割った余りの環）は、次のように定義されています。

def ZMod : ℕ → Type
  | 0 => ℤ
  | n + 1 => Fin (n + 1)

出典：
mathlib4、Mathlib/Data/ZMod/Defs.lean、138行目から140行目

ℕ → Type という型に注目してください。

自然数を受け取って、型を返します。
第1章で見た Vec α : Nat → Type と、同じ形です。

n が0のときは整数の全体 ℤ、そうでないときは Fin (n + 1) を返します。

Fin n は、n 未満の自然数の型です。

つまり、ZMod 5 の値は、0から4までの5個しかありません。
5以上の値を入れようとすると、型検査で拒否されます。

この ZMod n は、位数 pq の群の分類でも使われています。

【上級者向けコラム】`ZMod` と `Fin` は「同じ型」なのか

本文では ZMod (n+1) が実装上 Fin (n+1) として定義されることを説明しています。

ただし、数学的な役割は同じではありません。

Fin n は「0以上 n未満の自然数」という有限な代表元を表す型です。一方、ZMod n は「整数を n を法として同一視したもの」という環を表します。

したがって、

Fin n → 有限な代表元を表す型
ZMod n → 加法・乗法などの代数構造を持つ剰余環

という違いがあります。

実装上の表現型と、その型に与えられた数学的構造は分けて考えると理解しやすくなります。

部分群

部分群は、次のように定義されています。

structure Subgroup (G : Type*) [Group G] extends Submonoid G where

出典：
mathlib4、Mathlib/Algebra/Group/Subgroup/Defs.lean、296行目

構造体の中には、次の2種類のものが入っています。

種類	内容
データ	`carrier`。部分群の要素の集まり
証明	`one_mem'`、`mul_mem'`、`inv_mem'` など。それが部分群の条件を満たすことの証明

「条件を満たす要素だけを集めたもの」を、1つの型として扱っています。

これが、部分型（Subtype）の考え方です。

Lagrange の定理（部分群の位数は、群の位数を割り切る）は、この型を使って述べられます。

【上級者向けコラム】`Subgroup` と `Subtype` は同じものなのか

本文では Subgroup G を説明したあと、「これが部分型（Subtype）の考え方です」と説明しています。

入門者向けにはこの説明で十分ですが、実装上は両者は同一ではありません。

Subgroup G は構造体です。部分群の台集合を表す carrier に加えて、単位元を含むこと、積について閉じていること、逆元について閉じていることなどの証明を持ちます。

一方、Subtype は一般に {x : α // p x} のように、「型 α の値 x」と「p x の証明」を組にしたものです。

部分群の元を「部分群に属する元」という型として扱うところでは、Subtype が登場します。

したがって、Subgroup は「部分群という数学的構造」を表す構造体であり、その元を扱うところでは Subtype が使われる、と区別するとより正確です。

第4章　使えると推測するもの（表2）

4-1　この表について補足説明をさせてください

以下は、筆者が「この機能は数学の定理の形式化に使えるはずだ」と推測したものです。

第3章の表1と異なり、実際の形式化の事例を確認できていません。

読者が実績を自分で調べる方法は、第6章でご紹介します。

4-2　表2　筆者が「使えると推測する」もの

依存型の機能	何を型で表現するか	筆者が推測する使い道	確認できたこと
長さつきリスト（`Vec`）	空のリストから先頭を取れないことが、型で保証される	有限列を扱う証明	mathlib では `List` と `Finset` が主に使われています。 `Vec` が、実際に数学定理の証明の検査に使われた実績は確認できませんでした
ソート済みリスト	順序の保証を型に載せる	整列アルゴリズムの正しさの証明	mathlib では `List.SortedLE` などの述語（命題）として扱われています。型に載せる方式が、実際に数学定理の証明の検査に使われた実績は確認できませんでした
依存和（`Sigma`）	「値と、その値についての証明」の組	分類定理の記述	`Mathlib/Data/Sigma/Basic.lean` に定義が存在することは確認しました。ただし、それが、実際に数学定理の証明の検査に使われた実績は確認できませんでした

【上級者向けコラム】依存和（Sigma）の実績と Subtype との関係

表2において、依存和（Sigma）について「数学定理の証明の検査に使われた実績は確認できなかった」と記載しています。この記述について、専門的な観点から2点補足します。

Subtype は Sigma の変種である：
第3章や第7章で登場する Subtype（部分型 {x : α // p x}）は、本質的には第2成分が命題（Prop）に特化した依存和（依存ペア）です。したがって、広い意味での「依存ペアの構造」は、部分群や各種の制約付き構造としてmathlib全域で極めて中心的に使われています。
高度な抽象数学における Sigma の直接利用：
本稿の表2は、初等代数や初等幾何など、初学者が直感的にイメージしやすい具体的な定理形式化の範囲を念頭に置いた調査結果です。より高度な抽象数学（例えば、圏論におけるファイバー積や関手圏、位相空間論における空間の直和（余積）、幾何学におけるファイバー束などの形式化）においては、データ成分同士を束ねる Sigma 型そのものも日常的に定理の記述や証明に用いられています。

本稿では「初学者が直感的に捉えやすい具体的な定理の例」として推測枠に置いていますが、数学ライブラリ全体を見渡せば、Sigma型もまた不可欠な基盤として活躍しています。

4-3　ソート済みリストは、命題として扱われている

mathlib では、次のように定義されています。

def SortedLE (l : List α) := Monotone l.get

出典：
mathlib4、Mathlib/Data/List/Sort.lean、382行目

def で始まっていますが、返しているのは命題です。

Monotone l.get は「リストの要素を取り出す関数が単調である」という主張です。

つまり、「ソート済みのリスト」という型を作るのではなく、ただのリストと、ソート済みであることの証明を持つ設計です。

同じファイルには、次の記述があります。

これらの述語は Monotone l.get と同値であるが、IsChain (· < ·) や Pairwise (· < ·) とも同値である。

筆者による日本語訳です。 原文は英語です。

出典：
mathlib4、Mathlib/Data/List/Sort.lean、372行目付近のコメント

複数の言い換えが用意されていることに注目してください。

命題として扱えば、必要に応じて別の形へ移せます。
型に載せていると、こうはいきません。

4-4　この表の存在が、本稿の主張を支えます

「依存型があるのだから、何でも型に載せればよい」と考えたくなります。

しかし、実際にはそうなっていません。

ソート済みリストは命題として扱われ、長さつきリストは主役ではありません。

なぜそうなるのか。 次の章で、実機のコードとともにご説明します。

第5章　なぜ mathlib は、命題を選ぶのか

5-1　実際に書いて、確かめてみます

第1章で定義した Vec を使って、2つのリストを連結する関数を書いてみます。

長さ m のリストと長さ n のリストを連結すれば、長さ m + n のリストになるはずです。

def append {α : Type} : {m n : Nat} → Vec α m → Vec α n → Vec α (m + n)
  | 0,     _, Vec.nil,       ys => ys
  | m + 1, n, Vec.cons x xs, ys => Vec.cons x (append xs ys)

素直に書いたつもりです。

空のリストなら、もう一方をそのまま返す。
先頭がある場合は、先頭を残して残りを連結する。

しかし、このコードは型検査を通りません。

5-2　何が起きたのか

実際に出たエラーを、そのまま掲載します。

error: type mismatch
  ys
has type
  Vec α x✝ : Type
but is expected to have type
  Vec α (0 + x✝) : Type

error: type mismatch
  Vec.cons x (append xs ys)
has type
  Vec α (m + n + 1) : Type
but is expected to have type
  Vec α (m + 1 + n) : Type

2つの食い違いが報告されています。

実際に得られた型	求められている型
`Vec α n`	`Vec α (0 + n)`
`Vec α (m + n + 1)`	`Vec α (m + 1 + n)`

人間の目には、どちらも同じに見えます。

$0 + n$ は $n$ ですし、$m + n + 1$ は $m + 1 + n$ です。

しかし、型検査器にとっては別の型です。

Lean 4 の自然数の足し算は、右側の引数について再帰的に定義されています。
そのため n + 0 は計算で n になりますが、0 + n は計算だけでは n になりません。

5-3　等式の書き換えを挟めば、通る

通らないのであれば、通るように直せばよい。 そう考えるのが自然です。

次のように書き換えると、型検査を通ります。

def append {α : Type} : {m n : Nat} → Vec α m → Vec α n → Vec α (m + n)
  | 0,     n, Vec.nil,       ys => by rw [Nat.zero_add]; exact ys
  | m + 1, n, Vec.cons x xs, ys => by
      rw [Nat.succ_add]
      exact Vec.cons x (append xs ys)

rw は、等式で書き換えるための命令です。

Nat.zero_add は「$0 + n = n$」、Nat.succ_add は「$(m + 1) + n = (m + n) + 1$」という定理です。

これらを使って、型を合わせています。

このコードは、実機で型検査を通しました。

5-4　命題として扱えば、書き換えは要らない

同じことを、命題として扱ってみます。

theorem listAppendLength {α : Type} (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length :=
  List.length_append xs ys

List.length_append は、どこで定義されているのか。

mathlib ではなく、Lean 4 の本体に含まれています。

@[simp] theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length := by
  induction as with
  | nil => simp
  | cons _ as ih => simp [ih, Nat.succ_add]

出典：
Lean 4 本体、src/lean/Init/Data/List/Basic.lean、521行目から524行目
https://github.com/leanprover/lean4/blob/master/src/Init/Data/List/Basic.lean

証明の中身にも注目してください。

induction as with は、リスト as についての帰納法です。

場合	証明
`nil`（空のリスト）	`simp`
`cons`（先頭がある場合）	`simp [ih, Nat.succ_add]`

Nat.succ_add が使われています。

5-3 で Vec の連結を書いたとき、筆者も Nat.succ_add を使いました。
同じ等式が必要になっているのです。

違いは、それをどこで使うかです。

	`Nat.succ_add` を使う場所
`Vec`（型に載せる）	関数の定義の中。型を合わせるために必要
`List`（命題にする）	定理の証明の中。長さについて述べるときだけ必要

List では、長さを扱わない場面では Nat.succ_add が要りません。
Vec では、連結するたびに必要になります。

書き換えは、1つもありません。

List はただのリストで、長さの情報を型に持っていません。
そのため、連結しても型が変わりません。

長さについての主張は、別の定理として述べます。

このコードも、実機で型検査を通しました。

5-5　2つの書き方を、並べて比べる

	型に載せる（`Vec`）	命題にする（`List`）
連結の型	`Vec α m → Vec α n → Vec α (m + n)`	`List α → List α → List α`
型検査を通すために	`rw` による書き換えが2か所必要	不要
長さについての主張	型に含まれる	別の定理として述べる

この差が、証明を積み重ねるほど効いてきます。

5-6　なぜ、これが問題になるのか

理由は2つあります。

（1つ目）

型が合わなくなるためです。

数学では、途中で長さが変わる操作が頻繁に現れます。
そのたびに型が変わると、前に証明した定理が使えなくなります。

Vec A (n + 1) と Vec A (1 + n) は、人間には同じに見えます。
しかし型検査器にとっては別の型です。
これを等しいと示す作業が、証明の本筋とは無関係に増えていきます。

5-2 で見たエラーが、まさにこれです。

（2つ目）

命題なら、あとから付け足せるためです。

リストを作ってから、「ところで、これは長さ3だった」と後から証明できます。
型に載せていると、作る時点で長さが決まっていなければなりません。

この点は、第2章の 2-5 で実際のコードとともにご説明しました。

そこでは、次の2つを比べました。

	どう書けるか
命題として扱う	`def xs : List Nat := [3, 1, 2]` と作ってから、長さや空でないことを別の定理として書き足す
型に載せる	`def vs : Vec Nat 3 := ...` と、作る時点で長さを宣言する

もうひとつ、第2章では触れなかった点があります。

並べ替えなどの操作を経ても、List の型は変わりません。

def ys : List Nat := xs.mergeSort (· ≤ ·)

theorem ysLength : ys.length = 3 := by
  simp [ys, xs]

xs も ys も、型は List Nat のままです。

そのため、xs について分かっていることを、そのまま使って ys の性質を示せます。

実際、ysLength の証明は simp [ys, xs] の一行で済んでいます。

Vec であれば、こうはいきません。

並べ替えた結果の長さが元と同じであることを、型のレベルで示す必要があります。
5-3 で見た rw による書き換えが、ここでも必要になるのです。

【上級者向けコラム】「型が変わると、前に証明した定理が使えなくなる」はどこまで正しいか

本文では、依存型の説明として「操作によって型が変わると、前に証明した定理が使えなくなる」と説明しました。

これは入門者向けの直感としては有用です。ただし、専門的には「定理が論理的に使えなくなる」という意味ではありません。

依存型では、ある型の添字が等しいことを証明して、その等式に沿って値や定理を別の型へ移すことができます。Lean では rw、subst、Eq.rec などが、そのような型の書き換えを支えています。

したがって、本文で問題としているのは、より正確には、以前の定理を再利用するために添字の等式を証明したり、型を合わせるための書き換えを追加したりする必要が生じることです。

一方で、依存型には、不正な状態を型検査で排除しやすいという大きな利点があります。

つまり、

型に載せる → 不正な状態を型検査で排除しやすい
命題にする → 値の型を変えずに性質を後から証明しやすい

という設計上のトレードオフがあります。

【上級者向けコラム】「型に載せる」と「命題にする」を繋ぐ架け橋 ── Subtype

第5章まで「Vecのように型に載せる」か「Listのようにただの型にして証明を持ち歩くか」を対比してきました。しかし、Leanにはこの2つの美点を併せ持つ強力な道具があります。それが Subtype（部分型） です。

Subtypeは {x : α // p x} という構文で書かれ、「元の型 α の値 x」と「それが述語 p を満たすという証明」を1つのパッケージにした型を作ります。

・Vec α n のような「添字付き帰納型（Indexed Inductive Type）」は、添字が変わるたびに別の型になってしまい、等式書き換えが大変になります。
・一方、Subtypeであれば、台となる値を取り出す射影関数（Subtype.val）を通じて元の List α の世界に戻れるため、既存の定理をそのまま適用しやすくなります。

第7章で登場する Subgroup（部分群）や Fin n も、本質的にはこのSubtype（または類似の構造体）の技術によって支えられています。

5-7　ソート済みリストの場合

mathlib が List.SortedLE という命題を使う理由も、同じです。

ソートの定理を証明するとき、リストを並べ替える操作が何度も現れます。
そのたびに型が変わると、扱いきれません。

5-8　本章のまとめ

依存型があるからといって、何でも型に載せればよいわけではありません。

どちらを選ぶかは、設計の判断です。
mathlib は、多くの場面で命題を選んでいます。

第6章　実績を自分で調べる方法

本稿では、表1と表2を分けました。

読者が自分で実績を調べられるよう、調べ方をご紹介します。

6-1　形式化の実績を集めたアーカイブ

アーカイブ	何が分かるか	URL
Formalizing 100 Theorems	有名な100の定理が、どの定理証明支援系で形式化されたか	https://www.cs.ru.nl/~freek/100/
1000+ theorems（Lean 版）	Wikipedia 収録の定理の形式化の進捗。定理ごとに mathlib の Lean のコードが表示される	https://leanprover-community.github.io/1000.html
Formalizing 100 theorems in Rocq	形式化に使われた公理と、動作を確かめた版まで表示できる	https://madiot.fr/rocq100/
Archive of Formal Proofs（AFP）	Isabelle で形式化された成果。証明の全文を読める	https://isa-afp.org/
Missing theorems（Lean）	Lean でまだ形式化されていない定理	https://leanprover-community.github.io/100-missing.html

これらのアーカイブの詳しい読み方は、筆者の別の記事で扱いました。

形式化された数学定理はどこで調べる？どの定理がどの証明支援系で形式化されたか？――『Formalizing 100 Theorems』から証明コードを読むまで

6-2　mathlib のソースコードを読む

特定の機能が、どこで使われているかを調べたいときは、ソースコードを直接読むのが確実です。

mathlib のソースコードは、GitHub で公開されています。

https://github.com/leanprover-community/mathlib4

本稿で引用した定義も、すべてここから読みました。

調べたいもの	探す場所
行列	`Mathlib/Data/Matrix/`
有限型	`Mathlib/Data/Fintype/`
剰余環	`Mathlib/Data/ZMod/`
部分群	`Mathlib/Algebra/Group/Subgroup/`
リストの整列	`Mathlib/Data/List/Sort.lean`

6-3　「形式化されていない」の意味

注意していただきたい点があります。

アーカイブで「形式化されていない」と書かれていても、その定理が誤っているという意味ではありません。

「まだ誰も、その定理証明支援系のコードに置き換え終えていない」という意味です。

この点も、上記の別記事で詳しく扱いました。

第7章　表1の各行を、コードで読む

第3章では、表1で実績を示しました。

本章では、そのうち第3章で詳しく扱わなかった行について、実際のコードを読みます。

第3章 3-3 で扱った3行（行列の次元、ZMod、部分群）は、本章では繰り返しません。

7-1　有限性を持ち運ぶ（`Fintype` と `Finite`）

表1の記述を、あらためて引用します。

有限性を持ち運ぶ（Fintype）
「この型は有限である」というデータを、型クラスとして持つ。
位数 pq の群の分類（2025）で中心的に使用。Fintype（データ）と Finite（命題）の使い分けが形式化の設計を左右しました。

まず、何が問題なのかを確かめます

数学では「有限個である」という言い方を、よく使います。

「この群の要素は有限個である」「この集合は有限集合である」といった具合です。

では、これをコードで書くには、どうすればよいでしょうか。

2つの書き方があります。

書き方	何を持つか
要素を全部並べる	「この型の要素は、1、2、3の3つです」と、実際に列挙する
「有限である」とだけ述べる	「有限個であることは確かです」とだけ言い、個数も中身も言わない

mathlib には、この2つに対応する仕組みが、別々に用意されています。

Fintype が前者、Finite が後者です。

`Fintype` は、要素を全部持っている

実際の定義を見てみます。

class Fintype (α : Type*) where
  /-- The `Finset` containing all elements of a `Fintype` -/
  elems : Finset α
  /-- A proof that `elems` contains every element of the type -/
  complete : ∀ x : α, x ∈ elems

出典：
mathlib4、Mathlib/Data/Fintype/Defs.lean、57行目から61行目

class は、型クラスを定義する宣言です。

Haskell の型クラスと似たものだと考えてください。

Haskell で Eq a と書けば、「型 a は、等しさを比べられる」という意味でした。

Lean でも同じです。 Fintype α と書けば、「型 α は有限である」という情報が、型に紐づきます。

そして、その情報の中身を取り出せます。 次に見るとおりです。

中身は2つです。

名前	何を持つか
`elems`	要素をすべて並べた `Finset`。実際のデータ
`complete`	どの要素も `elems` に含まれる、という証明

Finset は、有限集合を表す型です。

Set（集合）とは別のものです。

型	何を表すか
`Set α`	α の部分集合。無限でもよい
`Finset α`	α の有限部分集合。要素を並べたものとして表される

Finset は、要素を実際に並べて持っています。

つまり elems には、その型の要素が実際に全部入っています。

たとえば Bool 型を考えてください。

Bool の値は true と false の2つです。
Fintype Bool の elems には、この2つが実際に入っています。

complete は、「true も false も elems に入っている。それ以外の値はない」という証明です。

したがって、Fintype α があれば、α の要素を1つずつ取り出して数えられます。

`Finite` は、事実だけを述べている

こちらの定義です。

class inductive Finite (α : Sort*) : Prop
  | intro {n : ℕ} : α ≃ Fin n → Finite _

出典：
mathlib4、Mathlib/Basic/Finite/Defs.lean、101行目から102行目

Sort* という記号が出てきました。

Type と Prop の両方をまとめて指す言葉です。

記号	何を指すか
`Type*`	データの世界。`Nat`、`Bool`、リストなど
`Prop`	命題の世界。「6は偶数である」など
`Sort*`	その両方

Fintype は Type* に限っていましたが、Finite は Sort* まで受け付けます。

つまり、より広い範囲に使えるということです。

末尾の : Prop に注目してください。

Prop は、命題の世界です。

第2章で「型に載せる」と「命題にする」を比べました。
Prop に属するものは、後者、つまり命題です。

中身を読みます。

α ≃ Fin n は、「α と Fin n のあいだに1対1の対応がある」という意味です。

≃ という記号を、説明します。

「同値」と読みます。

2つの型のあいだに、互いに行き来できる対応があることを表します。

条件	内容
α から `Fin n` への関数がある	どの要素も、行き先が決まっている
`Fin n` から α への関数もある	逆向きにも行ける
行って戻ると、元に戻る	どちらの向きでも

要するに、「中身の名前が違うだけで、実質的に同じもの」ということです。

たとえば Bool と Fin 2 は同値です。

`Bool`	`Fin 2`
`false`	0
`true`	1

名前が違うだけで、2つの値を持つ型である点は同じです。

Fin n は、0から n - 1 までの n 個の値を持つ型でした。

つまり、この定義は次のことを述べています。

ある自然数 n があって、α の要素は Fin n の要素とぴったり対応する。

「ある n があって」という言い方に注目してください。

その n が何であるかは、述べていません。

決定的な違いは、ここです

Finite α を持っていても、n を取り出すことはできません。

なぜでしょうか。

ここで、proof irrelevance という言葉を説明します。

日本語では「証明の無関連性」と訳されます。

これは、次のような規則です。

同じ命題に対する証明は、どれも等しいとみなす。

どういうことか、例で考えます。

「6は偶数である」という命題を、2通りの方法で証明したとします。

証明の方法
6 = 2 × 3 だから偶数である
6 を2で割ると余りが0だから偶数である

手順は違いますが、結論は同じです。

proof irrelevance のもとでは、この2つの証明は区別されません。

「6は偶数である」という事実さえあればよく、どう証明したかは問わないのです。

なぜ、そういう規則にするのでしょうか。

証明の中身が、その後の計算に影響してはいけないためです。

もし証明の方法によって計算結果が変わるなら、「どちらの証明を使ったか」を気にしながらプログラムを書くことになります。

それでは、扱いが煩雑になります。

この規則の結果として、何が起きるか。

証明の中に入っていた情報が、取り出せなくなります。

Finite α の定義を、もう一度ご覧ください。

class inductive Finite (α : Sort*) : Prop
  | intro {n : ℕ} : α ≃ Fin n → Finite _

n という自然数が、証明の中に現れています。

しかし Prop に属しているため、proof irrelevance が働きます。

「どう証明したか」を区別しないのですから、その中の n も取り出せません。

「α は有限である」という事実だけが残ります。

【上級者向けコラム】proof irrelevance と「証明情報を取り出せない」の関係

本文では、Finite が Prop に属することと proof irrelevance を関連づけています。

proof irrelevance は、同じ命題の証明を、その証明内容によって区別しないという性質です。

ただし、「Prop の値は全部、実行時に単純に消される」という説明と proof irrelevance は同じ概念ではありません。

Finite の場合、定義の中に現れる n は有限性の証明に含まれています。しかし Finite α 自体は Prop にあるため、その証明を通常の計算データとして使って「この n を返す」という設計にはなっていません。

このため、「証明の中に情報があっても、それをそのまま計算データとして取り出すわけではない」と理解するとよいでしょう。

mathlib の同じファイルには、次の説明があります。

Finite という述語は計算上の関連を持たず、Prop 値であるため、proof irrelevance の恩恵を受ける。これは、型が有限であるという事実そのものを表している。

筆者による日本語訳です。 原文は英語です。

出典：
mathlib4、Mathlib/Basic/Finite/Defs.lean、19行目から20行目

「恩恵を受ける」と書かれていることに、ご注目ください。

取り出せないことを、欠点ではなく利点として述べています。

なぜ利点なのか。 中身を気にせず扱えるためです。

「有限である」という事実だけが必要な場面では、どう証明したかを持ち歩く必要がありません。

2つを、表で比べます

	`Fintype`	`Finite`
属する世界	`Type`（データの世界）	`Prop`（命題の世界）
持っているもの	要素を並べた `Finset`	「有限である」という事実のみ
要素を列挙できるか	できる	できない
個数を取り出せるか	できる	できない
本稿の言葉でいえば	型に載せるに近い	命題にするに近い
向いている場面	実際に数えたいとき	有限であることだけが必要なとき

これが、第2章で扱った対比と同じ構図であることにお気づきでしょうか。

Fintype は、情報を多く持つ代わりに、扱いが重くなります。
Finite は、情報が少ない代わりに、軽く扱えます。

実際の形式化で、この選択が問題になりました

位数 pq の群の分類の論文は、この使い分けが形式化の設計を左右したと述べています。

「位数 pq の群の分類」とは、どういう定理でしょうか。

p と q が素数のとき、要素の個数が pq 個である群は、どういうものがありうるか。
それを、すべて列挙する定理です。

ここで「要素の個数」が出てきます。

数えるのであれば Fintype が要ります。
しかし、Fintype を使うと、扱いが重くなります。

同論文によれば、Lagrange の定理の型が変更された経緯もあります。

Lagrange の定理は「部分群の位数は、群の位数を割り切る」という定理です。

変更前	変更後
`Fintype.card` を使う形	`Nat.card` を使う形

Nat.card は、Finite があれば使えます。

Fintype.card が「要素を並べて数える」のに対し、Nat.card は「有限であることが分かっていれば、その個数を返す」という形です。

実際に数える手続きを持たなくても、個数について述べられます。

つまり、「数えられる」という強い要求から、「有限である」という弱い要求へ、条件が緩められたわけです。

これは、本稿の主題そのものです。

必要以上に強い情報を型に載せると、扱いが重くなる。
必要な分だけを要求するのが、形式化の設計なのです。

出典：
S. Harper, P. Wu, "Classifying the groups of order pq in Lean", 2025. arXiv:2501.09769

【上級者向けコラム】`Finite` と `Fintype` の違いをもう一段深く見る

Fintype α には実際の Finset α が入っているため、要素を列挙したり個数を計算したりできます。

一方、Finite α は Prop に属します。定義には「ある自然数 n と α ≃ Fin n が存在する」という内容が現れますが、その証明自体を通常の計算データとして利用する設計ではありません。

ただし、「Finite から Fintype を作れない」という意味ではありません。Lean / mathlib には有限性から Fintype を得る仕組みがあります。典型的には、計算可能性を目的としない古典論理を用いた構成です。

したがって本文の「Finite から個数を取り出せない」は、「Finite の証明そのものから計算可能な形で個数を取り出すわけではない」という意味で読むと適切です。

【上級者向けコラム】Finite から Fintype を復元する「選択公理」と noncomputable

本文で「Finite は命題なので個数などの情報を取り出せない」と説明しました。では、数学者が「有限群 G の位数」を使って計算したいときはどうするのでしょうか？

実は Lean / mathlib では、選択公理（Axiom of Choice） を認めることで、Finite α という純粋な存在証明から、具体的な代表元を無理やり選んで Fintype α を合成する関数（Fintype.ofFinite など）が用意されています。

ただし、これを行うと関数や定義に noncomputable（計算不可能）という属性が付きます。プログラムとして実行して答えを出すことはできなくなりますが、数学的な定理の証明の中では自由に使うことができます。数学の形式化では「計算機としての実行可能性」を潔く手放し、「古典数学の自由さ」を取る場面が数多く存在します。

7-2　有限集合の添字（`Fin n`）

表1の記述です。

有限集合の添字（Fin n）
範囲外のアクセスが型で防がれる。
Fintype.card (Fin n) = n。行列の添字、群の位数に使われる。

`Fin n` とは何か

Fin n は、0から n - 1 までの自然数の型です。

型	値
`Fin 3`	0、1、2 の3つ
`Fin 5`	0、1、2、3、4 の5つ

Fin 3 に 3 を入れることはできません。

型検査の段階で拒否されます。

これが、「範囲外のアクセスが型で防がれる」ということです。

配列の添字に Fin n を使えば、範囲外を読もうとするコードが、そもそも書けなくなります。

要素の個数についての定理

Fin n の要素は、ちょうど n 個です。

当たり前に見えますが、これを定理として証明しておく必要があります。

@[simp]
theorem Fintype.card_fin (n : ℕ) : Fintype.card (Fin n) = n :=
  List.length_finRange

出典：
mathlib4、Mathlib/Data/Fintype/Card.lean、496行目から498行目

1行目の @[simp] は、Lean への指示です。

「この定理を、自動的な簡約に使ってよい」という印です。
これが付いていると、証明の中で自動的に使われます。

2行目が、定理の中身です。

Fintype.card (Fin n) は「Fin n の要素の個数」を表します。
それが n に等しい、と述べています。

3行目が、証明です。

List.length_finRange という、すでに証明済みの定理を使っています。

証明の中身を読む

finRange n は、0 から n - 1 までを並べたリストです。

finRange 3 であれば、[0, 1, 2] にあたります。

List.length_finRange は、「このリストの長さは n である」という定理です。

7-1 で見た Fintype の定義を思い出してください。

elems : Finset α という、要素を並べたデータを持っていました。

Fin n の場合、その elems が finRange n から作られています。

したがって、要素の個数は、リストの長さに帰着します。

「有限である」ことの中身が、リストという具体的なデータに支えられているのです。

7-3　等しさを持ち運ぶ（`Eq`）

表1の記述です。

等しさを持ち運ぶ（Eq）
等しさの証明を、値として関数に渡す。
Fintype.equiv_of_card_eq（同じ濃度の有限型は同値）。

「等しさの証明を、値として渡す」とは

ふつうのプログラミング言語では、関数に渡せるのは値だけです。

数、文字列、リスト。そういったものです。

定理証明支援系では、証明も渡せます。

第1章で見た vhead を思い出してください。

def vhead {α : Type} {n : Nat} (v : Vec α (n + 1)) : α :=

この関数は、「長さが n + 1 である」ことを型で要求していました。

Fintype.equiv_of_card_eq は、これと似た形をしています。

この定理が述べていること

言葉で述べます。

2つの有限型 α、β について、「要素の個数が等しい」という証明が与えられれば、α と β のあいだの1対1の対応が得られる。

「証明が与えられれば」という部分が要点です。

等しさの証明が、関数の引数として渡されます。

具体的に考える

α の要素が3個、β の要素も3個だったとします。

このとき、α と β のあいだに1対1の対応を作れるはずです。
どちらも3個ずつあるのだから、順番に対応させればよい。

しかし、これをコードにするには、「どちらも3個である」ことを示す必要があります。

その証明を、引数として渡すわけです。

Fintype.equiv_of_card_eq （個数が等しいことの証明） → 1対1の対応

証明を渡さなければ、対応は得られません。

個数が違う型について、うっかり対応を作ってしまうことが、型検査の段階で防がれます。

なぜ、こう書けるのか

これは、Curry-Howard 対応の帰結です。

Curry-Howard 対応とは、命題を型とみなし、証明をプログラムとみなす考え方です。

論理の側	プログラムの側
命題	型
証明	その型を持つ値

証明が「値」なのですから、関数に渡せます。

これが、定理証明支援系でできることの土台です。

【上級者向けコラム】`Eq` は依存型で何を支えているのか

本文では Eq を「等しさを持ち運ぶ」と説明しています。

依存型では、型の添字そのものが値に依存するため、Vec α n と Vec α m を同じように扱いたい場合、n = m という等式を使って一方から他方へ移す必要が生じます。

この「等式に沿って型を移す」仕組みが、依存型プログラミングの重要な基盤です。

本文の Vec の例で rw [Nat.zero_add] や rw [Nat.succ_add] が必要になったのも、まさにこの仕組みによります。

したがって、型が合わないので等式で書き換えるという現象は、依存型の欠点だけではなく、依存型が値と型を結びつけているからこそ必要になる基本操作でもあります。

7-4　商型（`Quotient`）

表1の記述です。

商型（Quotient）
「同値なものを同一視した型」を作る。
剰余群、加群のテンソル積、環の余極限、Stone-Čech コンパクト化、Cauchy 完備化、実数と p 進数の定義、基数の定義に使われる。

「同値なものを同一視する」とは

数学では、「別のものだが、同じとみなす」という操作が頻繁に現れます。

もっとも身近な例は、時計です。

13時は、1時と同じ位置を指します。
25時も、1時と同じです。

12で割った余りが同じなら、同じとみなす。 これが同一視です。

この操作を、型のレベルで行えるのが商型です。

「商」という言葉は、割り算の商と同じ語です。

12を12で割ると、1周して元に戻ります。
「割る」という操作が、同一視にあたるのです。

英語では Quotient と書きます。

実際のコードを読む

第3章で見た ZMod の定義を、もう一度ご覧ください。

def ZMod : ℕ → Type
  | 0 => ℤ
  | n + 1 => Fin (n + 1)

出典：
mathlib4、Mathlib/Data/ZMod/Defs.lean、138行目から140行目

1行目の ℕ → Type に注目してください。

自然数を受け取って、型を返します。

第1章で見た Vec α : Nat → Type と、同じ形です。
これが依存型の姿でした。

2行目と3行目が、場合分けです。

入力	返す型
`0`	`ℤ`（整数の全体）
`n + 1`	`Fin (n + 1)`

ZMod 5 は Fin 5 になります。

7-2 で見たとおり、Fin 5 は0から4までの5個の値を持つ型です。

「5で割った余り」は、0から4のどれかです。

つまり、ZMod 5 の値は、「5で割った余り」そのものを表しています。

5と10と15は、どれも ZMod 5 では 0 です。
別々の整数が、同じ値として扱われます。

これが、同一視ということです。

実数も、商型として定義されている

mathlib の論文によれば、実数そのものが商型として定義されています。

どういうことでしょうか。

実数は、有理数の列の極限として作られます。

たとえば円周率は、3、3.1、3.14、3.141、… という有理数の列の行き着く先です。

ところが、同じ実数にたどり着く列は、1つではありません。

3、3.1、3.14、… という列も、
3.2、3.15、3.142、… という列も、
同じ円周率にたどり着きます。

そこで、「同じ実数にたどり着く列は、同じとみなす」という同一視を行います。

これが、実数の構成です。

商型という仕組みが、この同一視を型のレベルで表しています。

【上級者向けコラム】商型と「数学的な商」は区別して考える

本文では Quotient を「同値なものを同一視した型」と説明しています。

これは商型の直感として適切です。ただし、数学でいう「商」と Lean の実装上の Quotient は、常に1対1に対応するわけではありません。

数学的な構成として商を考えていても、mathlib では、その上に別の構造体や定義を重ねて利用する場合があります。

また、商型を作ることと、その商に演算、位相、順序、代数構造などを与えることは別の作業です。

Quotient は「同値関係で割った対象」を実装するための基礎的な仕組みであり、数学上の完成した商構造そのものをすべて自動的に与えるものではない、と理解するとよいでしょう。

7-5　型クラスによる代数構造

表1の記述です。

型クラスによる代数構造
「この型は群である」「体である」を型に載せる。
Cap Set 問題の形式化で、mathlib の線形代数と多変数多項式を使用。

数学の構造には、階層があります

群、環、体。 数学には、さまざまな構造があります。

これらは、ばらばらに存在しているのではありません。

構造	何を持つか
半群	結合的な演算
モノイド	半群 + 単位元
群	モノイド + 逆元

下に行くほど、条件が増えます。

群であれば、当然モノイドでもあります。
モノイドであれば、当然半群でもあります。

この階層を、そのまま型の階層として表せます。

実際のコードを読む

第3章で見た部分群の定義を、もう一度ご覧ください。

structure Subgroup (G : Type*) [Group G] extends Submonoid G where

出典：
mathlib4、Mathlib/Algebra/Group/Subgroup/Defs.lean、296行目

3つの部分に分けて読みます。

（1つ目）

structure Subgroup (G : Type*)

Subgroup という構造体を定義しています。
G という型を引数に取ります。

（2つ目）

[Group G]

この角括弧が、型クラスの制約です。

「G は群である」という情報を、型のレベルで要求しています。

群でない型について Subgroup を作ろうとすると、型検査で拒否されます。

たとえば、Subgroup Nat と書いても通りません。
自然数の全体は、足し算について群になりません（引き算ができないため）。

（3つ目）

extends Submonoid G

部分群は、部分モノイドを拡張したものだと述べています。

先ほど見た階層が、そのままコードに現れています。

中身には、データと証明が入っている

構造体の中には、2種類のものが入っています。

種類	名前	内容
データ	`carrier`	部分群の要素の集まり
証明	`one_mem'`	単位元が含まれる
証明	`mul_mem'`	積について閉じている
証明	`inv_mem'`	逆元について閉じている

「条件を満たす要素だけを集めたもの」を、1つの型として扱っています。

これが、部分型（Subtype）の考え方です。

Lagrange の定理（部分群の位数は、群の位数を割り切る）は、この型を使って述べられます。

なぜ、この階層が役に立つのか

定理を、もっとも弱い条件で証明しておけば、強い構造でも使えるためです。

半群について証明した定理は、モノイドでも群でも使えます。
一度証明すれば、何度も使い回せるのです。

Cap Set 問題の形式化では、この階層の上に線形代数と多変数多項式が載っています。

線形代数を一から作り直す必要がありません。
すでに用意された階層を、そのまま使えます。

7-6　宇宙レベル

表1の記述です。

宇宙レベル
型の階層を型として扱う。
Lean は proof irrelevance、quotient types、non-cumulative universes を持つ。

「型の型」という問題

第1章で、次の型を見ました。

inductive Vec (α : Type) : Nat → Type where

ここに Type という言葉が2回出てきます。

α : Type は「α は型である」という意味です。

では、Type そのものは、何なのでしょうか。

Lean では、すべてのものが型を持ちます。
したがって、Type にも型がなければなりません。

素朴に考えると、矛盾が生じます

「Type の型は Type である」としてみます。

一見、うまくいきそうです。しかし、これは矛盾を招きます。

理由を、直感的に述べます。

「すべての型の集まり」を考えてください。
それ自身も型なら、その集まりは自分自身を含むことになります。

集合論では、これが矛盾を生むことが知られています。

「自分自身を含まない集合の集まり」を考えると、それが自分自身を含むかどうかで矛盾が生じます（ラッセルのパラドックス）。

そこで、階層を作ります

Lean では、次のようになっています。

もの	その型
`Nat`、`Bool`	`Type`
`Type`	`Type 1`
`Type 1`	`Type 2`
`Type 2`	`Type 3`

どこまでも続きます。

この階層を、宇宙（universe）と呼びます。

Type は Type 0 の略記です。

「non-cumulative」とは

表1に non-cumulative universes とありました。

「累積的でない」という意味です。

	内容
累積的（cumulative）	`Type 0` のものは、`Type 1` のものでもある
累積的でない（non-cumulative）	`Type 0` と `Type 1` は、きっちり分かれている

Lean 4 は、後者を採っています。

Nat は Type に属しますが、そのままでは Type 1 に属しません。

移したいときは、明示的に持ち上げる必要があります。

なぜ、これが形式化で問題になるのか

大きな構造を扱うときに、階層の管理が必要になるためです。

たとえば、圏論では「すべての集合の圏」を考えます。
これは、集合より大きなものです。

アーデル環の形式化や、完備離散付値環の形式化でも、複数の階層をまたぐ構造が現れます。

どの階層にあるかを、正しく管理しなければなりません。

出典：
M. I. de Frutos-Fernández, "Formalizing the Ring of Adèles of a Global Field", 2022. arXiv:2203.16344

【上級者向けコラム】Lean の `Sort`・`Type`・`Prop`

本文では Type* をデータの世界、Prop を命題の世界、Sort* をその両方として説明しています。

入門者向けには便利な説明ですが、Lean の型階層を概念的に書くと Prop = Sort 0、Type u = Sort (u+1) という関係があります。

そのため Sort は、命題と通常の型を共通の枠組みで扱う階層です。

本文の「データの世界」という表現は入門用の比喩として理解し、厳密には Type はさまざまな対象の型を置く universe だと考えるとよいでしょう。

【上級者向けコラム】宇宙レベルは「型の型」だけではない

本文では Type, Type 1, Type 2 といった階層を説明しています。

これは重要な直感ですが、宇宙は単に「型の型を無限に並べる仕組み」ではありません。

主な役割の一つは、「すべての型を1つの型にまとめる」という自己言及を避け、型理論の整合性を保つことです。

また、Lean では universe polymorphism があり、定義を特定の universe に固定せず、複数の universe レベルで再利用できるように書けます。

圏論や代数などの大きな構造を形式化すると、対象の universe と、その対象をまとめる構造の universe が異なる場合があります。そのため宇宙レベルの管理は、ライブラリを一般的に再利用するための重要な仕組みでもあります。

7-7　依存型による分類定理の記述

表1の記述です。

依存型による分類定理の記述
「ある次元と、その次元の構造」を型で扱う。
3次元以下の可解 Lie 環の分類（2025）。基底の添字を型で扱い、次元ごとの場合分けを行った。

分類定理とは

「この条件を満たすものは、次のどれかである」という形の定理です。

たとえば「位数が6の群は、巡回群か、3次対称群のどちらかである」といった主張です。

3次元以下の可解 Lie 環の分類であれば、次のようになります。

次元が1、2、3のそれぞれについて、可解 Lie 環はどれだけあるか。

すべて列挙する、という形の定理です。

次元ごとに、構造が変わります

1次元の Lie 環と、3次元の Lie 環は、別のものです。

基底の個数が違います。
1次元なら基底は1本、3次元なら3本です。

この「個数が違う」ということを、どう扱えばよいでしょうか。

`Fin n` を使えば、型で扱えます

7-2 で見た Fin n を思い出してください。

Fin 1、Fin 2、Fin 3 は、それぞれ別の型でした。

基底の添字を Fin n で表せば、次元 n が型に現れます。

次元	基底の添字の型
1	`Fin 1`
2	`Fin 2`
3	`Fin 3`

型が違うのですから、混同しようがありません。

1次元の Lie 環についての議論を、3次元のものに誤って適用することが、型検査の段階で防がれます。

次元ごとの場合分けが、型のレベルで行えるのです。

出典：
V. del Barco, G. Infanti, E. Rivas, P. Schwahn, "Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean", 2025. arXiv:2505.19975

7-8　本章のまとめ

表1の各行を、コードで読んできました。

節	行	コードで確かめたこと
7-1	`Fintype` と `Finite`	`Fintype` は要素を全部持ち、`Finite` は事実だけを述べる。 `Type` と `Prop` の違いが、そのまま「型に載せる」と「命題にする」の違いにあたる
7-2	`Fin n`	0から `n - 1` までの型。範囲外が型で防がれる。`Fintype.card_fin` の証明が、リストの長さに帰着している
7-3	`Eq`	等しさの証明を、関数の引数として渡せる。Curry-Howard 対応の帰結
7-4	商型	「同値なものを同一視する」操作。`ZMod n` は `Fin n`。実数そのものも商型として定義されている
7-5	型クラス	`[Group G]` という制約。半群からモノイド、群へという数学の階層が、型の階層になっている
7-6	宇宙レベル	`Type` の型は `Type 1`。階層がないと矛盾が生じる。大きな構造の形式化で必要
7-7	分類定理	`Fin 1`、`Fin 2`、`Fin 3` は別の型。次元ごとの場合分けが型で行える

とくに 7-1 が重要です。

Fintype と Finite の使い分けは、本稿の第2章で扱った「型に載せるか、命題にするか」という問いの、実際の形です。

位数 pq の群の分類という、具体的な定理の形式化において、この選択が設計を左右しました。

まとめ

本稿で見てきたことを、整理します。

見たこと	内容
依存型とは	型の中に値が現れる型。`Vec α : Nat → Type` の形
型に載せる	性質を型そのものに書き込む。型検査の段階で間違いに気づく
命題にする	ただの値と、その性質の証明を、別々に持ち運ぶ
実際の形式化での使われ方（表1）	行列の次元、`Fin n`、`Fintype`、商型、部分型、型クラス、宇宙レベルなど。典拠を示した
推測にとどまるもの（表2）	長さつきリスト、ソート済みリスト、依存和。実績は確認できなかった
mathlib が命題を選ぶ理由	操作のたびに型が変わると、書き換えが増える。実機で確かめた
`Fintype` と `Finite`	`Type` と `Prop` の違いが、「型に載せる」と「命題にする」の違いにあたる。位数 pq の群の分類で、この選択が設計を左右した

依存型は、数学の定理の形式化で、実際に広く使われています。

ただし、何でも型に載せればよいわけではありません。

どちらを選ぶかは、設計の判断です。

本稿で書いたコードの全体

以下は、筆者が書いたコードです。
mathlib を使わず、Lean 4 単体で動きます。

-- 長さつきリスト
inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- 長さ1以上のリストからだけ、先頭を取り出せる
def vhead {α : Type} {n : Nat} (v : Vec α (n + 1)) : α :=
  match v with
  | Vec.cons x _ => x

-- 例：長さ3のリスト
def sample : Vec Nat 3 :=
  Vec.cons 1 (Vec.cons 2 (Vec.cons 3 Vec.nil))

#eval vhead sample

-- 命題として扱う場合
def sampleList : List Nat := [1, 2, 3]

theorem sampleLength : sampleList.length = 3 := rfl

連結の例です。

inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- 等式の書き換えを挟めば、通る
def append {α : Type} : {m n : Nat} → Vec α m → Vec α n → Vec α (m + n)
  | 0,     n, Vec.nil,       ys => by rw [Nat.zero_add]; exact ys
  | m + 1, n, Vec.cons x xs, ys => by
      rw [Nat.succ_add]
      exact Vec.cons x (append xs ys)

-- 命題として扱えば、書き換えは要らない
theorem listAppendLength {α : Type} (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length :=
  List.length_append xs ys

性質を後から付け足す例です。

-- リストをふつうに作る。長さのことは、まだ考えていない
def xs : List Nat := [3, 1, 2]

-- あとから、長さについての性質を付け足す
theorem xsLength : xs.length = 3 := rfl

-- さらにあとから、別の性質も付け足せる
theorem xsNotEmpty : xs ≠ [] := by simp [xs]

-- 並べ替えても、リストの型は変わらない
def ys : List Nat := xs.mergeSort (· ≤ ·)

-- 並べ替えた結果についても、性質を付け足せる
theorem ysLength : ys.length = 3 := by
  simp [ys, xs]

実機での確認について

本稿に掲載したコードのうち、筆者が書いたものは、すべて実機で型検査を通しました。

項目	内容
処理系	Lean 4.15.0
使用したライブラリ	なし（Lean 4 単体）

mathlib から引用したコードについて

mathlib のソースコードを読んで転記しました。 ファイル名と行番号を、各引用に添えています。

ただし、筆者の手元でビルドしたものではありません。

引用の正確さは、ソースコードと照合して確かめました。

引用元	版
mathlib4	本稿の執筆時点の master

行数や行番号は、ライブラリの更新によって変わります。

関連記事

形式化の実績を調べる

形式化された数学定理はどこで調べる？どの定理がどの証明支援系で形式化されたか？――『Formalizing 100 Theorems』から証明コードを読むまで

定理証明支援系について

型理論について

「等しさ」を型として扱う

「等しさ」はどのレベルまで型として宣言し、型検査できるか？ ── Pythonから関数型言語・定理証明言語へ

定理証明支援系が使われるもうひとつの場面

本稿では、定理証明支援系が数学の定理の形式化にどう使われるかを見てきました。

しかし、使われる場面は数学だけではありません。
ゼロ知識証明の回路検証にも、使われています。

ある研究は、SNARK システムにおける回路のバグのおよそ96パーセントが「制約の欠落」であり、形式証明が事前に検出できるものだと報告しています。

本稿で扱った Lean 4 のほか、Coq や ACL2 が、この用途で使われています。

詳しくは、次の記事をご覧ください。

「AIがちゃんと計算したことを、どう証明するの？」── 有限体の上のニューラルネットワーク入門

同記事の第7話で、形式証明とゼロ知識証明の違いを取り上げて論じました。

	何を保証するか	確実さ
形式証明	回路の設計にバグがないこと	100パーセント
ゼロ知識証明	その回路が正しく実行されたこと	99.999…パーセント

出典一覧

mathlib のソースコード

mathlib4（GitHub）. https://github.com/leanprover-community/mathlib4
Mathlib/Data/Matrix/Mul.lean（行列の乗算）
Mathlib/Data/Fintype/Card.lean（Fintype.card_fin）
Mathlib/Data/ZMod/Defs.lean（ZMod の定義）
Mathlib/Algebra/Group/Subgroup/Defs.lean（部分群の定義）
Mathlib/Data/List/Sort.lean（List.SortedLE の定義）
Mathlib/Data/Sigma/Basic.lean（依存和）
Mathlib/Data/Fintype/Defs.lean（Fintype の定義）
Mathlib/Basic/Finite/Defs.lean（Finite の定義）

Lean 4 本体のソースコード

Lean 4（GitHub）. https://github.com/leanprover/lean4
src/Init/Data/List/Basic.lean（List.length_append）

形式化の事例

S. Harper, P. Wu, "Classifying the groups of order pq in Lean", 2025. arXiv:2501.09769. https://arxiv.org/pdf/2501.09769
V. del Barco, G. Infanti, E. Rivas, P. Schwahn, "Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean", 2025. arXiv:2505.19975. https://arxiv.org/pdf/2505.19975
S. R. Dahmen, J. Hölzl, R. Y. Lewis, "Formalizing the Solution to the Cap Set Problem", 2019. arXiv:1907.01449. https://arxiv.org/pdf/1907.01449
E. Wieser, U. Song, "Formalizing Geometric Algebra in Lean", 2021. arXiv:2110.03551. https://arxiv.org/pdf/2110.03551
M. I. de Frutos-Fernández, "Formalizing the Ring of Adèles of a Global Field", 2022. arXiv:2203.16344. https://arxiv.org/pdf/2203.16344
M. I. de Frutos-Fernández, F. A. E. Nuccio Mortarino Majno di Capriglio, "A Formalization of Complete Discrete Valuation Rings and Local Fields", 2023. arXiv:2310.01998. https://arxiv.org/pdf/2310.01998

mathlib について

The mathlib Community, "The Lean Mathematical Library", CPP 2020, pp. 367–381. doi: 10.1145/3372885.3373824. https://leanprover-community.github.io/papers/mathlib-paper.pdf
Lean community「Mathematics in mathlib」. https://leanprover-community.github.io/mathlib-overview.html
Lean community「Maths in Lean: linear algebra」. https://leanprover-community.github.io/theories/linear_algebra.html

形式化の実績の一覧

F. Wiedijk, "Formalizing 100 Theorems", Radboud University Nijmegen. https://www.cs.ru.nl/~freek/100/
Lean community「1000+ theorems in Lean」. https://leanprover-community.github.io/1000.html
Archive of Formal Proofs. https://isa-afp.org/