定理証明支援：Coq（UniMath）・Lean・Isabelle

形式証明（コンピュータが証明の各ステップを検証する数学）を始めたい人にとって、どのツールを選ぶかは大きな分かれ目です。ここでは、よく並べて比較される 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 は目的が異なる）。

同じ定義にはしていないので「定理の定義が揃った統計」ではありません。あくまでソース上のキーワードの出現回数です。

• Mathlib の example は演習・小検証が多く、論文の「定理」とは一致しない。
• Coq 側は Definition や Remark 以外の証明付き宣言が一部漏れる。
• Isabelle は補題の細かい分割の文化があり、数が大きく見えやすい。
• 「Mathlib が ○ 倍豊富」といった結論には使えないが、「規模感のオーダー」「どれを数えたか」

どう選べばよいか

まとめ

• Coq（UniMath）、Lean（Mathlib）、**Isabelle（HOL）**は、いずれも優れた定理証明環境だが、論理の土台とライブラリの目的が異なるため、「順位」はつけられない。
• Cursorであればすぐにダウンロードして実行できるので３つダウンロードして使ってみて使い分けした方が早い。