定理証明システム：Coq・Lean・Isabelle
証明アシスタントとライブラリの対応表
| 証明アシスタント (Tool / Language) | 主要な数学ライブラリ (Library) | 特徴 |
| Coq | UniMath / Mathematical Components | UniMathは「単一型理論(Univalent Foundations)」に基づく意欲的なライブラリです。 |
| Isabelle/HOL | AFP (Archive of Formal Proofs) | HOLは「高階論理」を指します。AFPは膨大な数学的証明の集積所です。 |
| Lean | mathlib | 現在、最も数学者コミュニティの勢いがあり、巨大な統一ライブラリを目指しています。 |
各関係性の補足
1. Coq と UniMath
Coqはフランスで開発された非常に歴史のあるツールです。UniMathは、数学者ウラジーミル・ヴォエヴォドスキーらが提唱した「ユニバレント数学」をCoq上で実装したものです。
※Coqには他にも、4色定理の証明に使われた Mathematical Components (math-comp) という非常に有名なライブラリもあります。
2. Isabelle と HOL (AFP)
Isabelle自体は「汎用的な論理フレームワーク」ですが、最も普及している設定が HOL (Higher-Order Logic) であるため、一般に Isabelle/HOL と呼ばれます。
この上で動く AFP は、査読付きの論文のように新しい数学的定義や証明が日々追加される巨大なアーカイブです。
3. Lean と mathlib
現在、最も「ライブラリと本体」の密着度が高いのがこれです。mathlib は単なるライブラリを超えて、Leanで数学をするための「標準OS」のような存在になっています。数学の最先端（パーフェクトイド空間など）を記述しようとするプロジェクトもこの上で動いています。
まとめると
- Coq / Isabelle / Lean ＝ 筆記用具や文法（どう書くか）
- UniMath / AFP / mathlib ＝ 書かれた内容や公式集（何を知っているか）
形式証明（コンピュータが証明の各ステップを検証する数学）を始めたい人にとって、どのツールを選ぶかは大きな分かれ目です。ここでは、よく並べて比較される Coq（Rocq）上の UniMath、Lean 4 と Mathlib、Isabelle/HOL の三つについて「何が違うのか」を整理します。
※製品名の表記は、Coq は近年 Rocq Prover という名称も使われますが、本文では慣習的に Coq と書きます。
まず押さえる三つの立ち位置
Coq ＋ UniMathは、主に 一価性（Univalence）などを含む「単一基礎」寄りの数学を、Coq の言語で積み上げるプロジェクトです。圏論やホモトピー型理論の文脈で名前が出やすい ライブラリ（UniMath） とセットで語られることが多いです。
Lean 4 ＋ Mathlibは、古典数学を広く形式化するための、いま最も活発なエコシステムの一つです。解析・代数・位相など、大学以降の数学の「標準的な教科書の延長」を目指した 巨大ライブラリ（Mathlib） が中心です。
Isabelleは、高階古典論理（HOL） を核に、Isar と呼ばれる読みやすい証明スタイルで記述できるのが特徴です。教育・検証・既存の形式化資産（配布に含まれる HOL や、別配布の Archive of Formal Proofs など）との相性がよく、「文章に近い証明を書きたい」という人にも向きます。
三つとも「間違った推論は通らない」という点では同じですが、前提とする論理・文化・ライブラリが別物です。
証明の「書き味」：ソースファイルと文体
- Coq（
.v）
命題を宣言し、Proof.からQed.までで証明を進めます。タクティク（中間目標を変形するコマンド）に頼るスタイルが一般的です。UniMath を使う場合は、その上に 型としての等式や同値を多用する書き方になります。 - Lean（
.lean）
Lean 4 はモダンな言語設計で、タクティクモードと項（プログラムとしての証明）を行き来しやすいです。Mathlib はファイル数・定理数ともに膨大で、コミュニティの慣習に沿った書き方を覚える分量が大きくなりがちです。 - Isabelle（
.thy）
Isar により、「〜である。なぜなら…」に近い構造で証明を並べられます。HOL 系なので、Coq や Lean の依存型の一部の習慣とは温度差がありますが、読み返しやすい長い証明には向きます。
論理の「土台」：
- **UniMath（Coq 上）**は、一価数学・圏論的な基礎を前面に出したいときの選択肢です（「すべてを集合として書く」というより、型と同値の扱いが中心になりやすい）。
- **Mathlib（Lean）**は、選択公理や排中律を含む古典数学を素直に積み上げる設計が強いです。
- Isabelle/HOLは、高階論理＋古典的な推論がデフォルトの世界観です。
したがって、**「同じ定理を三つで証明したら同じ結論か」**という意味での単純比較はできません。公理の置き方と、言語が許す述べ方が違うからです。
「定理の数」
ネット上では、ソース中の lemma や theorem などの出現回数を数えて比較する例もありますが、公平な指標にはなりません。理由は次のとおりです。
- キーワードの意味が違う（例：Lean の
exampleは演習的なものも多い）。 - 補題の分割の文化が違う（細かく切るほど「数」は増える）。
- 対象ライブラリの範囲が違う（Mathlib は意図的に広く、UniMath は目的が異なる）。
同じ定義にはしていないので「定理の定義が揃った統計」ではありません。あくまでソース上のキーワードの出現回数です。
| 対象 | 条件 | ヒット数（概算） | .v / .lean / .thy ファイル数（概算） |
|---|---|---|---|
| UniMath | 行頭付近の Lemma / Theorem / Proposition / Corollary / Fact / Remark | 約 14,367 | 約 1,635（UniMath/UniMath 以下の .v） |
| Mathlib | 行頭付近の theorem / lemma / example | 約 162,176 | 約 7,844（Mathlib 以下の .lean） |
| Isabelle HOL | 行頭付近の lemma / theorem / corollary / proposition | 約 64,876 | 約 1,467（src/HOL 以下の .thy） |
- Mathlib の
exampleは演習・小検証が多く、論文の「定理」とは一致しない。 - Coq 側は
DefinitionやRemark以外の証明付き宣言が一部漏れる。 - Isabelle は補題の細かい分割の文化があり、数が大きく見えやすい。
- 「Mathlib が ○ 倍豊富」といった結論には使えないが、「規模感のオーダー」「どれを数えたか」
どう選べばよいか
| 読者の興味 | 検討しやすい方向 |
|---|---|
| 一価性・圏論・ホモトピー型の流れを追いたい | Coq ＋ UniMath |
| 解析・代数・位相など「数学」を形式化したい | Lean 4 ＋ Mathlib |
| 証明を文章に近い形で残し、教科書型の議論に近づけたい | Isabelle（HOL や関連ライブラリ） |
Isabelleにおける論理の切り替え構造
Isabelleを起動する際や、新しい証明ファイル（Theoryファイル）を作成する際に、どの論理ベース（Session）を使用するかを指定します。
| 論理の名称 | 内容 | 特徴 |
| Isabelle/Pure | すべての基礎（メタ論理） | 他の論理を定義するための「論理を作るための論理」。 |
| Isabelle/HOL | 高階論理 | 最も一般的。 型付きの論理で、現代数学やソフトウェア検証に最適。 |
| Isabelle/ZF | ツェルメロ＝フレンケル集合論 | 伝統的な集合論（空集合、べき集合など）に基づいた数学を構築。 |
| Isabelle/FOL | 一階述語論理 | 基本的な論理演算のみの世界。教育用や基礎研究用。 |
なぜ切り替えができるようになっているのか？
Isabelleの開発思想は「特定の論理に依存しない（Generic）」ことにあります。
- 論理学の実験場: 「もし集合論ではなく、別の論理体系で数学を組み上げたらどうなるか？」といった研究が可能です。
- 柔軟性: ソフトウェア検証にはHOLが便利ですが、純粋な数学基礎論をやりたい人にはZF（集合論）の方が馴染みがある、といったニーズに応えられます。
現実的には「HOL」が圧倒的
「切り替え可能」ではありますが、現代ではIsabelle/HOLがあまりに強力でライブラリ（AFP）も充実しているため、初心者がIsabelleに触れる場合は、ほぼ100%「HOLモード」を使っていると考えて間違いありません。
- Isabelle は、論理をロードするためのプラットフォーム。
- HOL, ZF, FOL は、その上でロードされる論理設定（セッション）。
まとめ
- Coq（UniMath）、Lean（Mathlib）、**Isabelle（HOL）**は、いずれも優れた定理証明環境だが、論理の土台とライブラリの目的が異なるため、「順位」はつけられない。
- Cursorであればすぐにダウンロードして実行できるので３つダウンロードして使ってみて使い分けした方が早い。