依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか

はじめに

「この OS の中核部分には、バグが存在しない」

こう言い切れるソフトウェアが、実際にあります。seL4 という名前の、OS の中核部分です。

ただし、ここでいう「バグが存在しない」とは、無条件に何も問題が起こらないという意味ではありません。明示された仮定のもとで、実装が仕様に従うことが証明されている、という意味です。この違いは、第７部で正確に説明します。

普通、ソフトウェアの品質は、テストで確かめます。しかしテストは、試した場合について正しいと分かるだけです。試さなかった入力が、必ず残ります。

seL4 は違いました。数学の証明によって、実装が仕様どおりに振る舞うことが示されています。 テストのように特定の入力を試したのではなく、あらゆる場合について論証したのです。そして、その証明を検査したのが、本記事の主役 Isabelle/HOL（イザベル・エイチ・オー・エル）という言語です。

ただし、この証明にも前提があります。 何が証明され、何が仮定されたのかは、第７部で正確に述べます。

証明の規模は、次のとおりです。

• 検証されたコード:8,700行
• 書かれた証明:20万行
• かかった労力:約20人年

コードの23倍の量の証明を、20年分の人手をかけて書き上げた。それが seL4 です。

なぜ、証明のほうがコードより長くなるのでしょうか。

理由は、コードは「何をするか」だけを書けばよいのに対し、証明は「なぜ、あらゆる場合に正しいのか」を書かなければならないからです。

たとえば、配列から最大値を取り出すプログラムを考えてみてください。
コードは十数行で書けます。

しかし「この関数は必ず最大値を返す」ことを証明するには、次のすべてを示す必要があります。

• 配列が空のときはどうなるのか
   
• 要素が１つのときはどうなるのか
   
• 繰り返しのあいだ、何が保たれているのか
   
• 繰り返しが終わったとき、なぜ答えが正しいのか

コードでは一行で済む処理が、証明では何十行にもなります。

さらに、seL4 のような大きなシステムでは、証明が積み重なります。

ある性質を示すために別の性質が要り、その性質を示すためにさらに別の性質が要る。

土台となる補題を何百個も用意して、ようやく目的の定理に到達するのです。

そして、証明には省略が許されません。

人間が読む数学の本なら「明らかに」と書いて飛ばせる箇所も、機械に検査させるには、すべて書き切る必要があります。

8,700行のコードに対して20万行の証明。

この比率は、「証明とは何をする作業なのか」をそのまま表しています。

20人年もかけるくらいなら、人間が証明したほうが早いのではないか？

もっともな疑問です。
実際、人間が紙の上で証明すれば、はるかに短い時間で済みます。

数学の世界 でも、同じこと が起きています。

ここで 形式化 という言葉を説明します。

数学者が論文や教科書に書く証明 は、日本語や英語の文章と数式が混ざったものです。
それを、機械が一段ずつ検査できる形に書き直す作業 を、形式化 と呼びます。

紙の証明では、「明らかに」「同様にして」と書いて先へ進める箇所 も、形式化では、その一段ずつを Isabelle や Lean 4、Rocq といった定理証明系のコードとして書き切らなければなりません。

そのため、Lean 4 や Rocq、Isabelle による大きな定理の形式化には、１０年以上の歳月をかけるプロジェクトになることがあるのです。

紙の上では数百ページで済む証明が、機械に検査させる形にすると膨大な作業になる傾向にあります。

それでも、この作業に取り組む人たちがいます。

理由は３つあります。

第１に、人間の証明は間違えるからです。

数学の論文にも、査読を通ったあとで誤りが見つかることがあります。

プログラムの検証となれば、なおさらです。

「何百人が読んで納得した」ことと、「あらゆる場合に正しい」ことは、別だからです。

seL4の検証 では、Ｃコードのバグ160件のうち144件が、検証の作業のなかで発見されました。

そのコードは、開発者たちが十分に注意して書き、テストも通したものです。
それでも、これだけの誤りが残っていました。

第２に、一度証明すれば、あとは何度でも自動で確かめられるからです。

紙の証明は、正しさを確かめるたびに人間が読む必要があります。

機械に検査させる形で書いておけば、コードを直したとき、その影響を受ける証明が壊れていないかを、機械が自動で確かめてくれます。

AWSの事例 を思い出してください。

25万行の証明を、市販のノートパソコンで30分で、検査をやり直すことができます。

開発が続くかぎり、検査のやり直しは、何百回と繰り返されることでしょう。
最初の20人年は、その後の無数の再確認と引き換えなのです。

第３に、何を仮定したのかが、すべて明示されるからです。

人間の証明では、人間の数学者やプログラマが無意識に前提としていることが紛れ込んでしまうことは避けがたいことです。

機械に検査させる場合は、そうしたことは発生しません。
すべての前提を、明示的に書き出さなければ証明が通らないからです。

この記事の後半で、seL4 が何を仮定していたのか を一覧でお示しいたします。

何を仮定に置き、「どこから先が、証明されていない仮定・前提だったのか」を厳密に言い切れるのは、Isabelle や Lean 4、Rocq（旧Coq） といった定理証明支援系に検査させたからです。

では、どんなときに割に合うのか

すべてのソフトウェアに、この労力をかける必要はありません。

判断の分かれ目は、誤りが起きたときに何を失うかです。

OSの中核部分が誤っていれば、その上で動くすべてのソフトウェアの安全が崩れます。

クラウド基盤の分離の仕組みが誤っていれば、他人のデータが見えてしまいます。

やり直しが利かず、影響が広く、しかも長く使われ続けるもの。
そうしたものには、20人年をかける価値があります。

逆に、すぐ作り直せるもの、影響範囲の狭いもの、寿命の短いものには、この手法は向きません。
テストのほうが、はるかに合理的だからです。

証明は、あらゆる場面で使うべき手法ではありません。
「ここだけは絶対に間違えられない」という部分を見極めて、そこに投じるものです。

seL4 は、まさにその判断が下された事例でした。

そして、ここで一つ確認しておきたいことがあります。

seL4 の検証が完了したのは、2009年です。
いまから17年前の出来事です。

「17年前に一度だけ成し遂げられた、記念碑的な仕事」なのでしょうか。

そうではありません。

2025年12月、AWS がクラウド基盤の中核部分を、同じ言語で検証したと発表しました。
この言語は、いまも実務の最前線にあります。

本記事では、この Isabelle/HOL という言語を、前提知識ゼロから紹介します。Python は書けるが、この分野の言語は学んだことがない、という方を想定しています。

「HOL」とは何か

先に、名前の意味だけ説明しておきます。

Isabelle/HOL の HOL は、Higher-Order Logic（高階論理） の略です。

高階論理 とは、「すべての〜について」と言える範囲が広い論理 のことです。

学校で習う論理では、「すべての自然数 $x$ について、$x + 0 = x$ が成り立つ」といった主張を書きます。

ここで、「すべての」 がかかっている対象は、個々の数 です。

高階論理 では、これに加えて、性質そのものや、関数そのものについても「すべての〜について」と主張することができます。

「すべての性質 $P$ について、〜が成り立つ」という主張を書くことができるのです。

この違いが何をもたらすのかは、第１部で詳しく説明します。

ここでは、「HOL は、数だけでなく、性質や関数についても語ることのできる論理のことだ」 とだけ押さえておいてください。

この言語は、いまから学ぶ価値があるのか

ところで、1986年に生まれた言語を、AIが証明を書き始めた2026年になって、いまさら学ぶ必要性や意味はあるのでしょうか？

筆者は、学ぶ価値がある と考えています。

筆者がそう考える理由を４点 挙げます。

第１に、実務におけるIsabelleの利用実績が、いまなお、更新され続けている からです。

seL4 は、2009年 の成果でした。

続く2025年12月、AWS が Nitro Isolation Engine というクラウド基盤の中核部分を、Isabelle/HOL で形式検証したと発表 しました。

AWS はこれを、 世界初の形式的に検証されたクラウドハイパーバイザー と位置づけています。

証明の規模は25万行だったとされています。
この規模は、seL4に匹敵するもの です。

皆様が日々、利用されているクラウドの土台が、Isabelleで検証されているかもしれない のです。

ほかにも、以下に示す数々の業績を、Isabelleは挙げ続けています。

• WebAssembly の型システムの健全性（2018年）
   
• 分散編集のアルゴリズムの正当性（2017年）
   
• 暗号プロトコル（1990年代から継続）
   
• ゲーデルの不完全性定理（2014年から2015年）
   
• 素数定理（2004年）

ソフトウェアの検証と数学の形式化の両方で実績を持つ定理証明支援系は、そう多くありません。

それぞれの業績について、補足しておきます。

WebAssembly は、ブラウザなどで動く実行環境です。
この実行環境の 意味論 を Isabelle/HOLで形式化 した仕事が2018年に発表され、型システムの健全性が証明されるとともに、実際に誤りも発見されました。　

ここで、意味論 とは、「このプログラムを実行すると、何が起こるのか」を厳密に定めたもの です。
「この命令は、値をこう変える」という規則を、曖昧さなく書き下したものだと考えてください。

分散編集のアルゴリズム は、複数の利用者が同時に文書を編集しても矛盾が起きないようにする仕組みです。CRDT と呼ばれるこの技術の正当性が、2017年に証明されました。

ところで、なぜ「勝手にマージ」できるのでしょうか。
その理由は、CRDTのデータ構造が 半束 と呼ばれる代数構造になっているからです。
この点については、筆者が以前に書いた記事で扱っています。

• Git・CRDT・eBPF・型理論 ── 2026年の夏、流行ではなく「土台」になる6つのテーマ

上記の記事では、CRDT が衝突しない理由を、代数構造から説明しています

暗号プロトコル の検証は、ポールソン自身が1990年代から取り組んできた分野です。
単年度の成果ではなく、長く続いている仕事のため、開始の年代を示しました。

ゲーデルの不完全性定理 の形式化には、２段階の発表があります。
2014年に第１と第２の両方の定理を扱った論文が、2015年にその詳細版が公表されました。
第二不完全性定理が機械で検査されたのは、このときが初めてです。

素数定理 は2004年の成果です。素数がどのように分布しているかを述べた、数論の基本的な定理です。

Isabelleの利用実績については、詳しくは第７部で扱います。

以上が、2026年のいま、Isabelleを学び始めることに意義を見出せる理由のひとつ目です。

ふたつ目の理由として挙げるべきと筆者が考えるのは、Isabelleの自動化の仕組みが優れていることです。

Isabelle には sledgehammer という仕組みがあります。

証明したい命題を前にして一語打つだけで、複数の外部の証明器が並列に走り、証明を探す仕組みです。

この仕組みのおかげで、私たち人間は、証明を書く作業のうち、退屈な部分を機械に任せられる のです。

これは、定理証明支援系を学びはじめようとする人にとって、参入障壁（学習コスト）を大きく下げてくれるものです。

第５部で、この sledgehammerの動きを見ていただきます。

Isabelleを学ぶべき３つ目の理由は、IsabelleとAIとの相性のよさです。

ここが、2026年のいま、最も注目すべき点かもしれません。

Isabelle は、大規模言語モデル（LLM）による定理証明の研究対象として、活発に取り上げられてきました。

2022年以降、LLM を Isabelle と組み合わせる研究が次々に発表されてきました。

Draft, Sketch, and Prove（2022年）は、LLM に自然言語で証明の下書きを書かせ、それを Isar に変換し（Isarについては、この後すぐに説明いたします）、残った隙間を sledgehammer に埋めさせるという分担を最初に示した研究です。

Lyra（2023年）は、Isabelle が返したエラーを LLM に戻して骨組みを修正させ、Baldur（2023年）は、誤った証明そのものをLLMに修復させました。

そして2026年には、IsabeLLM と Isabellm という２つのシステムが登場します。

後者は、そのコードのすべてが GPT・Gemini・Claude によって実装された と報告されており、しかも sledgehammer を含む標準の自動化では証明できなかった補題を、証明できた としています。

それではなぜ、LLMによる定理証明の研究プロジェクトに、Isabelleが選ばれるのでしょうか。

その理由を説明するために、まず最初に、Isabelle には証明の書き方が２通りある ことを解説致します。

Isabelleの記法のひとつは、タクティクを並べる書き方です。

ここで タクティク という言葉を説明します。

タクティク とは、「この方針で証明を組み立てよ」と処理系に与える指示の言葉 です。

証明そのものを一字一句書く代わりに、短い指示を並べて与えると、処理系がその指示に従って証明を組み立ててくれます。

• 「ここで場合分けせよ」
• 「これを簡単にせよ」

といった指示を、プログラマが Isabelleの処理系に順に与えていく記法です。

この書き方には、人間にとって、読みにくいという難点があります。

指示が並んでいるだけなので、そのコードを読んでも、途中で何が証明されているのかが分かりにくいのです。

一行ずつ処理系に実行させ、画面に表示される証明の状態の変化を目で追いながらでなければ、読み解けないのです。

この難点は、Isabelle の開発者たち自身も認めています。

ポールソン、ニプコウ、ヴェンツェルの共著論文 "From LCF to Isabelle/HOL" には、次のようにあります。

従来の手法の問題は、機械が検査した証明を見た者が、ある時点で何が証明されているのかを知りようがないことである。目隠しでチェスをするようなものだ。

日本語のウェブサイトにも、同じ指摘が見当たります。

mod_poppo さんは、タクティクの羅列を見て「証明がどのように進んだのかわかりますか」と読者に問いかけ、実際に処理系を動かさなければ内容が分からないのではないか、という見解を示されています。

檜山正幸さんの記事でも、この読みにくさが議論の出発点になっています。

• 定理証明支援系についての問題意識（mod_poppo さん、2025年）
   
• 証明支援系がダメだった理由と、AIでブーストする理由（檜山正幸さん、2023年）

タクティクを使う記法 は、Isabelle に限らず、Rocq や Lean 4 でも採用されています。

プログラマが、証明の手順を一つずつ、チェスや将棋の駒を動かしていくように処理系へ伝える と、処理系がその指示を受けて、証明の状態を一段進めてくれます。

証明の中身を一字一句自分で書き下す必要がないという、大きな利点 があります。

しかし、難点 もありました。

他の人が書いたタクティクの羅列を見たとき、あるいは数か月後に自分が書いたものを読み返したときに、そのコードが何を証明しているのかが、一目では分からないのです。

実際に、タクティクが羅列されたコードを見てみましょう。

次のコードは、Isabelle のタクティク記法で書かれた証明 です。

皆様は、このコードが何を証明しているのか、一目見た瞬間に、読み取ることができるでしょうか。

lemma mystery: "distinct (rev xs) = distinct xs"
  apply (induction xs)
   apply simp
  apply (simp add: distinct_rev)
  done

lemma の行を隠して、apply から下だけを見てください。

「場合分けせよ」「簡単にせよ」「この規則を加えて簡単にせよ」「終わり」。**
指示が４つ並んでいるだけです。**

この４行から、何が証明されているのかは読み取れません。

• 何を仮定したのか ── 書かれていません
   
• 途中でどんな主張が示されたのか ── 書かれていません
   
• なぜこの順序で指示を出すのか ── 書かれていません

分かるのは、「$n$ について場合分けし、２回簡約した」ということだけです。

その結果、どんな中間の状態が生まれ、それがどう解消されたのかは、コードのどこにも残っていません。

これを知るには、Isabelle を起動し、一行ずつ実行して、画面に表示される証明の状態を目で追う必要があります。

apply (induction xs) を実行した瞬間に、画面には２つの部分目標が現れます。
apply simp で１つ目が消えます。

しかし、その部分目標が何だったのかは、コードには一切書かれていません。

これが、開発者たちが「目隠しでチェスをするようなものだ」と述べたタクティク・コードの意味の読み取りにくさです。

同じ証明を Isar で書くと、こうなります。
（ Isar については、この後すぐに解説いたします ）

lemma "distinct (rev xs) = distinct xs"
proof (induction xs)
  case Nil
  show "distinct (rev []) = distinct []" by simp
next
  case (Cons a xs)
  show "distinct (rev (a # xs)) = distinct (a # xs)"
    by (simp add: distinct_rev)
qed

行数は増えました。 しかし、show の行を読めば、その段階で何を示そうとしているのかが分かります。

空のリストの場合はこれを示す。
要素が１つ増えた場合はこれを示す。

処理系を動かさなくても、証明の道筋を読み取ることができるのです。

先にコードを示してしまいましたが、いま皆様に見ていただいた Isabelleのコードは、IsabelleのIsar記法で書かれたコード です。

Isabelleには、タクティクを使う記法以外に、もうひとつ、Isarという書き方を行うことができるのです。

• 「仮定する」
• 「よって」
• 「示す」

という語を使い、論証の筋道を文章として書き記していくスタイルの記法です。

詳しくは第６部で見ますが、Isar記法で書かれたIsabelleのコードは、上から下に読んでいくと、日本語の証明文として読むことができます。その様子は、先ほどコードの実例を皆様に眺めていただいた通りです。

Isar記法で書かれたIsabelleのコードを読むことで、そのコードで一体、どんな証明過程を検証しようとしているのか、コードを書いた者（LLM/ AI Agentもしくは人間のプログラマ）の意図を容易に理解することができるのです。

このIsar記法は、AIとの役割分担において決定的な意味を持つと筆者は考えています。

役割分担の姿 を見ていきましょう。

まず、LLM が証明の骨組みを書きます。

LLM は、人間が書いた数学の証明文を学習しています。そのため、論証の筋道を文章として書く形式は、LLM が最も出力しやすい形 にあたります。

実際の手順を、具体例で見てみましょう。

LLMが、日本語や英語、中国語などの自然言語文で、証明の下書きを書きます。

「すべての自然数 $n$ について、$n$ に $0$ を足しても $n$ のままである」という定理なら、次のような文章です。

n についての帰納法で示す。

n が 0 のとき、0 + 0 = 0 であるから成り立つ。

n = k で成り立つと仮定する。
このとき k の次の数についても、加法の定義から成り立つ。

次に、この文章を Isar の骨組みへ変換します。

theorem add_zero: "n + 0 = (n :: nat)"
proof (induction n)
  case 0
  show "0 + 0 = 0" sorry
next
  case (Suc k)
  show "Suc k + 0 = Suc k" sorry
qed

sorry という語に注目してください。
これは Isabelle に「ここは、まだ証明していない」と伝える印です。

骨組みだけが立っていて、中身が空いている状態 です。

sorry は、英語の「ごめんなさい」と同じ語です。
「ここは証明していません、すみません」という含みがあります。

この印を残したままにすると、Isabelle は警告を出し続けます。
証明していないことを、忘れさせない仕組み です。

そして、この空いた箇所を sledgehammer が埋めにいきます。

Isabelle の sledgehammer が、sorry と書かれた箇所を見つけるたびに証明を探しにいき、埋められるものを埋めていく。 LLM が苦手な細部を、機械的な探索が引き受ける わけです。

なぜ、sledgehammer は隙間を埋められるのでしょうか。

第１の理由は、既に証明された定理が大量に蓄積されているからです。

Isabelle の 標準ライブラリ に加えて、Archive of Formal Proofs という Isabelle のためだけに運営されているアーカイブ があります。

ここに収められた証明は、すべて Isabelle で書かれ、Isabelle で検査されたものです。両者を合わせると、約27万9千の補題 が蓄積されています。

では、どんな証明が収められているのでしょうか。

AFP の特徴は、数学とソフトウェアの検証が混在していることです。
割合としてはソフトウェア側のほうが多い と報告されています。

Mathlib の開発者たちによる論文は、AFP について、「現在の記事の約半分が、個別のアルゴリズムの解析と検証を扱っている」と述べています。

収蔵されているものを挙げると、次のようになります。

＜ソフトウェアと計算機科学の証明＞

• プログラミング言語の意味論の形式化（最大のエントリは Java の一方言を扱ったもので、約77,100行）
• データ構造とアルゴリズムの正当性
• モデル検査の理論
• 暗号プロトコルの検証
• 分散システムのアルゴリズム

＜数学の定理＞

• ゲーデルの不完全性定理
• ジョルダン曲線定理
• ラムゼーの定理
• 素数定理

AFP を分析した論文には、こう書かれています。

最も多く貢献した上位５名の成果は、プログラミング言語、データ構造、モデル検査に集中しており、数学ではない。計算機科学への偏りは、記事の分類から予想される以上に大きい、と。

Lean 4 の Mathlib との比較

Lean 4 の Mathlib と並べると、性格の違いがはっきりします。

	AFP（Isabelle）	Mathlib（Lean 4）
規模	約453万行	約200万行
中心にあるもの	ソフトウェアの検証と数学の混在	数学の形式化
記事の約半分	アルゴリズムの解析と検証	該当せず
運営の形	査読つき。ISSN を持ち、学術誌のように運営	単一の統合ライブラリ。継続的に統合される
構成	独立した記事の集まり。それぞれが別の著者による作品	一枚岩の階層構造。全体が一つの体系をなす
得意な分野	複素解析が特に厚いとされる	代数、位相、解析、数論など、数学の広い範囲

この違いは、両者の成り立ちから来ています。

Lean 4のMathlib は、「数学の教科書の延長を、一つの体系として積み上げる」ことを目指しています。

全体がつながった一枚岩で、新しい定理は既存の体系の中に組み込まれます。

テレンス・タオのような著名な数学者が参加し、AI による定理証明の研究でも学習の土台として使われています。

それに対して、IsabelleのAFPは、「それぞれ独立した成果を、査読を通して収蔵する」形です。

一つ一つの記事が独立した作品であり、著者も目的も異なります。

seL4の検証 があれば、数学の定理の形式化 もある。

学術誌に近い運営 だからこそ、この多様さが成り立ちます。

どちらが優れているという話ではありません。

数学の形式化に取り組むなら、Lean 4のMathlib が持つ数学定理の証明結果の収蔵リストの厚みが有益です。

ソフトウェアの検証に取り組むならば、IsabelleのAFPの収蔵品リストが有益です。

Isabelleのsledgehammerが自動探索しに出かけていくのは、AFPとIsabelle標準ライブラリの知識資産です。

このアーカイブについては、第８部で改めて扱います。

Lean 4 に Mathlib という 数学ライブラリ があるように、Isabelle にも膨大な既存の資産があるのです。

隙間を埋めるために必要な定理は、その多くがすでに誰かによって証明済みです。
sledgehammer は、この山の中から使えそうなものを選び出します。

以上が、sledgehammer が隙間を埋められる理由のひとつ目 です。既に証明された定理が、大量に蓄積されている からでした。

ふたつ目の理由は、sledgehammer が選び出した定理を、外部の証明器に渡すからです。

sledgehammer が、使えそうな定理の候補を選び出します。しかし、それだけでは証明は完成しません。

「sledgehammer が選び出した定理を組み合わせれば、目の前の隙間が埋まるか」を判定する必要があります。

ここで働くのが、Z3、Vampire、E といった 外部の自動証明器 です。

これらは Isabelle とは別に開発されたソフトウェア で、与えられた定理から結論を導けるかどうかを機械的に探索する、専用の道具 です。

つまり、sledgehammer がしているのは、次の２つです。

1. sledgehammer が、膨大な既存の定理から、使えそうなものを選び出す
    
2. sledgehammer が、選び出した定理を外部の証明器に渡し、隙間が埋まるかを試させる

sledgehammer は、「証明を発明する」のではありません。「既にある定理を組み合わせる」のです。

だからこそ、Isabelle のライブラリが厚いほど、この仕組みは強くなります。

ここまでが、LLM が書いた骨組みの隙間を、sledgehammer が埋めるまでの過程です。

LLMが出力した自然言語の証明文も、そこから変換された Isar の骨組みも、どちらも 「論証の筋道を、上から順に書き並べたもの」 です。

LLMが学習済みの（人間が書いた）数学の文章と形が近いものです。

LLM にタクティクの列を出力させるより、はるかに自然なのです。

そして最後に、人間の定理証明プログラマが、その証明を読みます。

この段階で、Isar 記法で書かれた証明は、人間にとって読みやすい という利点が効いてきます。

論証の筋道が Isar 記法のコードとして残されているからこそ、人間はその証明の妥当性を判断できます。

もしここで、タクティクが羅列されたコードだけが目の前に示された場合、定理証明プログラマは、そのコードが何を証明していたのかを解読する作業 に、とても手を焼くことになるはずです。

LLM は論証の筋道を文章として書き、sledgehammer は残った隙間を埋め、人間はその証明を文章として読む。

Isabelle が持つ２つの記法と強力な自動化は、この３者の分担を、それぞれの得意な形で受け止められる のです。

第３に、最も重要な点として、これから先の時代、AIが数学やプログラムコードの証明を書く場面が増えれば増えるほど、その証明を読んで判断する人間の役割が重くなることです。

ここで、言葉を区別しておきます。

LLM が出力するのは、Isabelle や Lean 4、Rocq といった定理証明支援系によって、まだ検証されていない証明の候補です。

日本語や英語で書かれた論証の文章であったり、Isabelle のコードの形をしていたりしますが、その時点では、まだ未検証の状態ですので、正しいかどうかは分かりません。

これに対して、Isabelle のカーネルが検査を通したものが、検証済みの証明です。
ここを通って初めて、「正しいと確かめられた」と言えます。

LLM がどれだけ証明の候補を出力しても、それが正しいかを判定するのは、Isabelle のカーネルです。

そして、そもそも何を証明すべきかを決めるのは、人間 です。
仕様を書く仕事は、自動化されません。

この論点については、筆者が２本の記事で扱っています。

１本目は、証明という手法そのものの限界を論じたものです。

• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界

Isabelle のカーネルが保証するのは、「実装が仕様に従っていること」だけです。
その仕様が、人間の意図を正しく写し取っているかどうかは、機械には判定できません。

誤った仕様に忠実な実装が出来上がっても、カーネルは「正しい」と答えます。

この境界を、Correctness と Appropriateness という言葉で整理したのが、この記事です。

２本目は、同じ問題を AI Agent の文脈へ広げたものです。

• AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう ── 「何をしてよいか」を決める責任は、AIが賢くなるほど人間に集中する

この記事では、混同してはならない４つの論点を挙げています。そのうちの一つが、「もっともらしさ」と「正しさ」の区別 です。

外見上、もっともらしく、論理的に不整合なく動いていることは、その挙動が人間の設計・開発者が意図した通りに動いていることをなんら保証するものではない

この構図は、定理証明でもそのまま当てはまります。

LLM が出力した証明の候補が、Isabelle のカーネルの検査を通ったとしても、それは「仕様どおりである」ことの保証であって、「その仕様が正しい」ことの保証ではありません。

そして、上記の記事の結論は、本記事の第４の理由と重なります。

AI Agent 時代とは、人間の責任が軽くなる時代ではなく、人間が担うべき「判断」と「説明責任」に求められる社会的な役割の重みが、これまで以上に高まる時代なのです

AI が証明の候補を書く時代とは、人間が証明を書かなくてよくなる時代ではありません。

人間が「何を証明させるか」を決め、機械の検査を通った証明について「それが本当に確かめたかったことか」を判断する時代です。

その判断を行うために、人間（定理証明エンジニア）が、Isabelle がどう動くかを知っている必要があります。

以上が、筆者が「Isabelle を学ぶ価値がある」と考える４つの理由です。

• 実務での実績が更新され続けていること。
• sledgehammer という自動化の仕組みを持つこと。
• AI との役割分担が成り立つ設計になっていること。
• そして、AIが証明の候補を書く場面が増える時代になればなるほど、AIが生成した未検証の証明文を読んで、人間が意図した仕様が適切に反映された証明文に仕上がっているかどうかを判断する人間の役割が重くなること。

ところで、Isabelle には、苦手とすることもあります。

たとえば、依存型を使えないため、Rocq や Lean 4 なら型で直接表現できることを、別の方法で表現する必要があります。

また、開発環境が Isabelle/jEdit と専用版の VS Code に限られており、汎用のコーディング支援ツールから扱うには構造的な難しさがあります。

これらの点は、第９部と第10部で扱います。

本記事は「Isabelle を学ぶ価値がある」という立場で書かれています。

しかしその判断は、読者の皆様ご自身がこの記事を読み終えていただいた後に、最終的に下していただければと思います。

想定読者

• 「証明でソフトウェアの正しさを保証する」という話に関心はあるが、具体的に何をするのか知らない方
   
• Rocq や Lean 4 の名前は聞いたことがあるが、Isabelle は知らない方
   
• 形式検証の言語を学んでみたいが、どれを選べばよいか迷っている方

数学の予備知識は仮定しません。専門用語は、登場するたびに日常の言葉で説明します。

この記事を読む価値

1. 論理の体系は一つではないという前提から出発して、Isabelle という言語の設計思想を理解できるようになる
    
2. HOL が単一の言語ではなく、複数の処理系からなる系統の名前であることを知り、その中で Isabelle/HOL がどう違うのかを説明できるようになる
    
3. seL4 が何を証明し、何を仮定したのかを、公式情報に基づいて正確に押さえられる
    
4. Rocq や Lean 4 が採る依存型という仕組みを、Isabelle が採らなかった理由が分かる
    
5. 証明を機械に探させる sledgehammer という仕組みを、実際の出力とともに知ることができる
    
6. AI が証明を書く時代に、この言語がどう位置づけられるかを考える材料が得られる

目次

[:contents]

TL;DR

（この節の専門用語は、いずれも本文で説明します）

• Isabelle は、1986年にケンブリッジ大学のローレンス・ポールソンが公開した定理証明の言語である
   
• 設計の中心にあるのは、特定の論理に縛られない枠組みを先に作り、その上に論理を載せるという考え方。載せた論理が HOL のとき、それを Isabelle/HOL と呼ぶ
   
• HOL は単一の言語ではなく、系統の名前である。HOL4、HOL Light、そして Isabelle/HOL が含まれる。この中で Isabelle/HOL だけが、枠組みの上に載せる形で作られている
   
• Rocq や Lean 4 が採る依存型を、Isabelle は採らない。代わりに単純型理論と古典論理を採る。この選択が、強力な自動化を可能にしている
   
• sledgehammer は、証明を外部の自動証明器に探させる仕組みである。Isabelle の生産性を支える中核の仕組みである
   
• seL4 の検証は、8,700行の C コードに対して20万行の証明、約20人年。ただし何を仮定したのかも、公式に明示されている
   
• 2025年、AWS が Nitro Isolation Engine を Isabelle/HOL で検証 した。世界初の形式的に検証されたクラウドハイパーバイザーであり、証明は25万行。実績は、いまも更新されている
   
• Archive of Formal Proofs は、査読つきで ISSN を持つ、証明の公開アーカイブである
   
• そして、AI が自動で証明を生成する時代だからこそ、「何を証明すべきか」を設計し、機械の出力を人間が読んで判断するための言語として、この処理系の価値はむしろ高まっている

第１部 ── 前提の整理: 論理はひとつではない

Isabelleの設計原理 を理解するため、まず最初に押さえておくべき前提があります。

論理はひとつではない という世界観が、その前提 です。

Python でプログラムを書くとき、私たちは「変数の値が変わる」「関数を呼ぶと何かが起こる」という世界にいます。

動かしてみて、期待どおりの結果が出れば正しい。
品質の確認は、基本的にこの形です。

しかし、証明の世界 は違います。

動かして確かめるのではなく、あらゆる場合について論証します。

そのためには、「何をもって正しいと認めるか」の規則を、あらかじめ決めておく必要があります。

その規則の体系が、論理です。

そして、ここからが本題です。

論理の体系は、ひとつではありません。

私たちが学校で習う論理は、古典論理 と呼ばれるものです。

「$A$ が成り立つか、成り立たないか、どちらかである」という 原則（排中律） を認めます。

しかし、この原則を認めない論理もあります。

直観主義論理 と呼ばれる論理（公理体系）では、「$A$ が成り立たないとは言えない」ことを示しても、「$A$ が成り立つ」とは結論しません。

実際に $A$ が成り立つことを構成して見せる必要があるからです。

他にも、「すべての〜について」と言える範囲が違う論理があります。

一階述語論理 では、個々の対象について「すべての $x$ について」と言うことができます。
「すべての自然数 $x$ について、$x + 0 = x$ が成り立つ」という主張は書くことはできるのです。

しかし、性質そのものについて量化することはできません。

「すべての性質 $P$ について」という言い方は、（一階述語論理では）許されないのです。

高階論理 では、許されます。

性質についても、関数についても、「すべての〜について」と主張することが可能になる のです。

Isabelle/HOL の HOL は、この高階論理のことです。

論理は、他にもあります。
それぞれ、用途に応じて、扱える概念そのものが違います。

• 様相論理（modal logic）── 「必ずそうである」「そうでありうる」という区別を扱えます。古典論理では、命題は真か偽のどちらかですが、様相論理では「必然的に真」と「たまたま真」を区別できます
   
• 時相論理（temporal logic）── 様相論理を時間に適用したものです。「これから先、ずっと成り立つ」「いつかは成り立つ」といった、時間をまたぐ主張を書けます。並行して動くプログラムの検証で広く使われています
   
• 線形論理（linear logic）── 命題を資源として扱います。古典論理では「A が成り立つ」という事実を何度でも使い回せますが、線形論理では一度使うと消費されます。在庫や権限のように、使えば減るものを論じるのに向いています
   
• 記述論理（description logic）── 概念どうしの関係を扱う論理で、知識をコンピュータに記述させる場面で使われます。ウェブの意味情報を表す標準規格の土台にもなっています
   
• 量子論理（quantum logic）── 量子力学の測定にまつわる性質を論じるための論理です。古典論理では成り立つ分配法則が、ここでは成り立ちません

どの論理を採るかで、証明できることが変わります。

この論点については、筆者が以前に書いた記事で詳しく扱っています。

• if 文もSQLも、実は別々の「論理」だった ── 古典論理から量子論理まで、21の論理体系を５人で議論する対話篇です。最初に読むならこちらをお勧めします
   
• 論理公理系の産業応用 全地図 ── 古典・直観主義・線形・様相・時相・記述・量子論理が、それぞれどこで使われているのか
   
• トポスと論理の関係 ── ひとつの数学の宇宙を選ぶと、なぜ古典論理か直観主義論理かが決まるのか
   
• 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学

この前提が、Isabelle の設計の出発点になります。 論理が一つではないなら、処理系はどの論理を選ぶべきか。Isabelle の答えは、意外なものでした。

第２部 ── Isabelle とは何か

生まれた動機:論理を実装する速さが、追いつかない

Isabelle は、1986年にケンブリッジ大学の ローレンス・ポールソン が公開しました。

当時、証明を検査する処理系はいくつも存在していました。エディンバラ大学の LCF、そこから派生した Cambridge LCF、Nuprl、HOL などです。

LCF とは、1970年代にエディンバラ大学のロビン・ミルナーが作った証明支援システムです。

ここで生まれた設計思想が、その後の多くの処理系に受け継がれました。
証明の正しさを最終判定する部分だけを小さく作り、そこだけを信頼するという考え方です。

HOL 系のすべての処理系、そして Rocq も、この LCF の子孫です。

ちなみに、ML というプログラミング言語は、この LCF のために設計されました

（この経緯は、筆者の Rocq の記事で詳しく扱っています）。

しかし、当時のポールソンは、この方式に限界を感じていました 。

ポールソン自身が、後の論文でこう述べています。

LCF 方式のシステムを作るのは、時間がかかり、しかも確実性がなかった。１年ほどごとに、利用者が重大なバグを見つけた。

そして、より深刻な問題がありました。

「計算機科学者は、論理学者が新しい論理を考え出す速さに、実装が追いつかない」という懸念が広まっていた。

当時、新しい論理はどれだけの速さで生まれていたのか

この「追いつかない」という感覚は、誇張ではありませんでした。

1970年代は、計算機科学のための新しい論理が、次々に提案された時代です。

年	論理	提案者
1969年	ホーア論理	ホーア
1970年	アルゴリズム論理	サルヴィツキ
1976年	動的論理	プラット
1977年	時相論理（プログラムのための）	プヌエリ
1979年	命題動的論理	フィッシャーとラドナー

10年のあいだに、５つの新しい論理体系が現れています。

しかも、これらはいずれも「プログラムの正しさを論じる」という、当時の計算機科学の中心的な課題に向けられたものでした。

ポールソンが Isabelle の開発を始めた1985年は、この直後です。

そして、その勢いは止まりませんでした。

• 1983年 ── 区間論理（モシュコフスキ）。デジタル回路の検証のために、時間の区間を扱う論理です
• 1987年 ── 線形論理（ジラール）。資源の消費という観点から、古典論理と直観主義論理を捉え直す論理です

ある研究者は、この時期を振り返って 「1980年代以降、私たちは論理体系の増殖を目にしてきた」 と述べています。

• Igor Walukiewicz（ボルドー大学／CNRS）, "From Logic to Games", FSTTCS 2005 論文集, Lecture Notes in Computer Science 第3821巻, 79〜91頁, 2005年

そのペースは、2000年以降も続いているのか

続いています。

たとえば、1979年に提案された命題動的論理には、その後も変種が加えられ続けています。

交わりを扱うもの（2005年）、並行合成を扱うもの（2014年） といった具合です。

時相論理の側でも、

• 有限の実行列を扱うもの（2013年）
• 直観主義論理と組み合わせたもの（2010年代）

などが提案されています。

つまり、「新しい論理が生まれ続ける」という状況は、1980年代の一時的な現象ではありませんでした。
いまも続いています。

だからこそ、「論理が提案されるたびに処理系を一から作る」という方式では、いつまでも追いつけない のです。

ポールソンが枠組みという発想に至った理由が、ここにあります。

論理学者が新しい論理を提案するたびに、それを実装した処理系を一から作る。

作るのに何年もかかり、しかもバグが出る。この繰り返しでは、いつまでも追いつきません。

そこでポールソンは、発想を変えました。

特定の論理のための処理系を作るのではなく、どんな論理でも載せられる枠組みを作る。

新しい論理が提案されたら、その規則を枠組みの上に記述するだけでよい。処理系を一から作る必要はない。

これが Isabelle の出発点 です。

Isabelle/Pure ── 論理を載せる枠組み

Isabelleの土台 にあるのが、Isabelle/Pure と呼ばれる 枠組み です。

Pure には、数学の内容が入っていません。

「自然数とは何か」も「集合とは何か」も、Pure には書かれていません。

Pure にあるのは、推論の規則を書き表すための、ごく少数の道具だけ です。

技術的にいえば、Pure 自体も ひとつの論理 です。

直観主義的な高階論理の、ごく一部だけを取り出したもの で、含意と全称量化と等号だけを持ちます。

ただし、その役割は数学を展開することではなく、他の論理の規則を書き表すこと にあります。

具体的には、次の３つです。

記号	役割
⟹	「これが成り立つならば、これが従う」という 規則の形 を書く
⋀	「どんな x についても」という 規則の一般性 を書く
≡	「これをこう定義する」という 定義 を書く

この３つだけで、さまざまな論理の推論規則を書き表すことができます。

なぜ、これで足りるのでしょうか。

推論の規則 とは、結局のところ、「これとこれが成り立つならば、これが成り立つ」という形をしています。

そして、その規則 は、「どんな命題についても」成り立つ必要があります。

この２つさえ書くことができれば、規則は書けます。

Pure は、そこまで削ぎ落とした設計 です。

対象論理 ── 枠組みの上に載せるもの

Pure の上に、実際に議論したい論理を載せます。

たとえば「かつ（∧）」という記号を使いたいとします。その振る舞いを、Pure の言葉で書き下します。

P ∧ Q ⟹ P

「$P$ かつ $Q$ が成り立つならば、$P$ が成り立つ」と読みます。

左辺と右辺を結ぶ ⟹ が、Pure が提供する記号 です。

「かつ」がどう振る舞うのかを、Pure の言葉で推論の規則として書き表している わけです。

このようにして、ある論理の推論規則 をすべて書き表すことができれば、その論理が Isabelle の上で使えるようになります。

実際に、いくつもの論理が載せられてきました。

• Isabelle/HOL ── 高階論理を載せたもの。最大かつ最も開発が進んでおり、Isabelle の既定です
   
• Isabelle/ZF ── ツェルメロ=フレンケル集合論を載せたもの。ポールソンによる選択公理の相対的無矛盾性の形式化などの成果があります
   
• Isabelle/FOL ── 一階述語論理を載せたもの
   
• Isabelle/HOLCF ── 領域理論を、HOL の上にさらに載せたもの

ほかにも、様相論理 や マルティン=レーフ型理論など が実装されています。

なお、Isabelle では、どの論理を載せるかを、利用者が選びます。

この選択は、コードの冒頭で行います。 Isabelle のファイルは .thy という拡張子を持ち、必ず次の形で始まります。

高階論理を使う場合:

theory MyTheory
  imports Main
begin

end

集合論を使う場合:

theory MyTheory
  imports ZF
begin

end

一階述語論理を使う場合:

theory MyTheory
  imports FOL
begin

end

違いは、imports の後ろの一語だけです。

theory に続く MyTheory は、ファイル名に合わせて筆者が任意に付ける名前 です。
begin と end のあいだに、定義や定理を書いていきます。

そして imports の後ろが、載せる論理の指定 です。

Main は Isabelle/HOL の標準ライブラリ を指し、これを書けば高階論理の世界で作業することになります。

ZF ならツェルメロ=フレンケル集合論、FOL なら一階述語論理です。

この一語を変えるだけで、その先で使える論理が変わります。

あたかも、パイプオルガンの音栓を差し替えるように、土台となる論理を選ぶわけです。

なお、実際には Main を書く場合がほとんどです。

Isabelle/HOL のライブラリが圧倒的に充実しているためで、初めて Isabelle に触れる方は、まずこの一語だけ覚えれば足ります。

ところで、ある種の数学の世界（ 「トポス」理論と呼ばれる数学 ）では、どの世界を選ぶかによって、そこで使える論理のほうが決まってしまう のです。

論理が選ぶ対象ではなく、結果として定まる ものになります。

この対比に関心を持たれた方は、筆者が以前に書いた記事をご覧ください。

• トポスと論理の関係 ── ひとつの数学の宇宙を選ぶと、なぜ古典論理か直観主義論理かが決まるのか

そして、この中で圧倒的に使われているのが Isabelle/HOL です。

seL4 も、後述する Archive of Formal Proofs に収められた膨大な証明も、ほぼすべて Isabelle/HOL の上で書かれています。そのため、単に「Isabelle」と言えば、実質的に Isabelle/HOL を指すことがほとんどです。

名前にスラッシュが入るのは、この構造のためです。
「Isabelle という枠組みの上の、HOL」という意味です。

余談:なぜ「Isabelle」という名前なのか

ポールソンが、フランスの計算機科学者ジェラール・ユエの娘の名前にちなんで命名した と伝えられています（この由来は Wikipedia などに記載されていますが、筆者はポールソン自身による記述を確認できていません）。

なお、ユエは Isabelle の中核技術のひとつである高階単一化の手法を考案した人物 でもあります。ポールソン自身が論文で、この手法を採用した利点に触れています。

なお、ポールソンの論文 "Isabelle: The Next 700 Theorem Provers" というタイトルは、ランディンの有名な論文 "The Next 700 Programming Languages" のもじりです。

第３部 ── HOL 系の中で、Isabelle/HOL だけが違う

HOL は、単一の言語の名前ではありません。 高階論理を土台にした処理系の、系統の名前です。

この系統には、次のものが含まれます。

• HOL4 ── 伝統的な HOL の直系。30年以上にわたって維持されています
• HOL Light ── カーネルが約400行という極小さで知られます
• ProofPower ── 商用の背景を持ちます
• Isabelle/HOL ── 本記事の主役

共通点

これらはすべて、エディンバラ LCF の子孫です。実装言語は ML の変種で、証明の正しさを最終判定する部分（カーネル）だけを小さく作り、そこだけを信頼するという設計を共有しています。

論理の土台も似ています。関数を扱うための、ごく単純な土台の上に組み立てられており、Rocq の土台と比べると、規則の数が少なく理解しやすいという特徴があります。

決定的な違い

HOL系の処理系のあいだで証明やソースコードを移植する研究があります。
そのような研究の中で、ある論文が、次のように述べています。

最も異なるのは Isabelle/HOL である。 推論の規則を処理系のプログラムの中に直接書き込むのではなく、Isabelle という汎用の枠組みのインスタンスとして実装されている。

出典は、次の論文です。

• Mark Adams（Proof Technologies Ltd／ラドバウド大学）, "The Common HOL Platform", 第４回 Proof eXchange for Theorem Proving ワークショップ（PxTP 2015）論文集, Electronic Proceedings in Theoretical Computer Science（EPTCS）第186巻, 42〜56頁, 2015年

この論文は、HOL系の処理系が互いにコードや証明をやりとりできるようにするための共通基盤を提案したものです。

そして、Isabelle/HOL は差異が大きすぎるため、その共通基盤で扱うには標準の大幅な設計変更が必要になるとも述べています。

つまり、HOL 系の中でも、Isabelle/HOL は設計上かなり異なる位置にあるのです。

観点	HOL4 / HOL Light / ProofPower	Isabelle/HOL
推論の規則はどこにあるか	処理系のプログラムの中に直接	枠組みの上に載せる形で
他の論理を載せられるか	できない	できる（ZF、FOL など）
証明の書き方	タクティク中心	Isar による読みやすい書き方も選べる

言語比較：得意分野と主要実績

処理系	得意なこと	主な実績
Isabelle/HOL	自動化、大規模な開発、読みやすい証明、豊富なライブラリ	seL4、ソフトウェア検証、数学の形式化
HOL4	伝統的な直系。長期の維持	CakeML（検証済みの ML コンパイラ）
HOL Light	カーネルが約400行という極小さ	ケプラー予想の形式化、Intel の浮動小数点演算の検証
ProofPower	商用の背景	英国の防衛・鉄道分野

どの定理証明支援系が優れているのか、という比較論ではなく、用途に応じて最適な言語を選び取るのが適切です。

高階論理に立脚する点は共通しているのに得意分野が異なる理由

同じ高階論理を採用していても、各言語処理系にはそれぞれ異なる個性と強み・弱みがあります
その違いが、実績の違いを生みました。

違いは、大きく４つあります。

１. 実装に使った言語

処理系	実装言語
Isabelle	Standard ML と Scala
HOL4	Standard ML
HOL Light	OCaml
ProofPower	Standard ML

これは、単なる好みの問題ではありません。

HOL4 が Standard ML で書かれていることは、CakeML という成果に直結しました。
CakeML は「検証済みの ML コンパイラ」です。**

ML で書かれた処理系が、ML のコンパイラを検証する。**
処理系自身の言語を、その処理系で検証するという構図です。

また、HOL Light は、証明そのものが OCaml のプログラムとして書かれます。

定理証明エンジニアは、OCaml のコマンド行で証明を組み立て、必要なら自分で OCaml の関数を書いて機能を拡張できます。
この自由さが、大規模な数学の形式化を支えました。

２. 型システムの拡張

Isabelle/HOL だけが、型クラスという仕組みを持っています。

これは Haskell に似た機能で、「順序を持つ型」「足し算ができる型」といった性質を、型のまとまりとして 扱うことができます。

たとえば、「順序を持つ型については、この定理が成り立つ」 と 一度証明してしまえば、自然数にも実数にも文字列にも、その定理を使いまわすことができます。

大きなライブラリを整理して育てるうえで、この仕組みは威力を発揮します。**

AFPが数百万行に育ったことの背景には、これがあります。

他の HOL系の定理証明支援系には、この型システムの仕組みがありません。**

同じことをするには、型ごとに証明を繰り返すか、別の方法を採る必要があります。

３. ライブラリが厚い分野

同じ論理でも、何が証明済みかは処理系ごとに違います。

処理系	ライブラリが厚い分野
HOL Light	実解析・複素解析（多変数の積分、微分、位相）
HOL4	確率論
ProofPower	Z 記法（形式仕様の記述言語）
Isabelle/HOL	数学と計算機科学の両方（AFP に蓄積）

この違いが、実績の違いをそのまま説明します。

ケプラー予想の証明は、球の詰め込み方についての幾何学的な議論であり、大量の実解析を必要としました。

HOL Light が選ばれたのは、まさにその分野のライブラリが充実していたから です。

Intel の浮動小数点演算の検証 も、同じ理由によるものです。

ProofPower が英国の防衛・鉄道分野で使われたのは、Z 記法という形式仕様の記述言語に対応していたから です。これらの分野では、Z 記法で仕様を書く慣行がありました。

４. 開発体制

HOL Light は、基本的に一人の開発者（ジョン・ハリソン）によって維持されてきました。

これが、極小のカーネルと、一貫した設計を可能にしています。

小ささと単純さゆえに、他の処理系へ翻訳しやすいという利点も生まれました。

Isabelle は、ケンブリッジ大学とミュンヘン工科大学を中心に、多数の開発者が関わってきました。

そのぶん機能は豊富ですが、配布物の規模も大きくなります（2019年時点で、HOL Light の84MB に対し、Isabelle は133MB でした）。

まとめると

同じ高階論理を採用していても、実装言語・型システムの拡張・ライブラリの厚み・開発体制が違えば、向き・不向きの用途も互いに異なります。

• 数学の解析が必要なら HOL Light
• 自分自身の言語を検証したいなら HOL4
• Z 記法で仕様を書く現場なら ProofPower
• 大規模な開発と、豊富なライブラリが必要なら Isabelle/HOL

論理が同じであることは、処理系が同じであることを意味しません。

ここに興味深い事実があります。

ポールソン自身が、HOL 系は自分の LCF の初期の仕事から派生したものであり、そのタクティク言語は HOL Light に完全に保存されていると述べています。

そして、自身が HOL Light の証明を数万行、Isabelle/HOL に翻訳した経験を報告しています。同じ人物が、両方の系譜に関わっているのです。

• Lawrence C. Paulson（ケンブリッジ大学）, "Formalising Mathematics in Simple Type Theory", Centrone・Kant・Sarikaya 編 Reflections on the Foundations of Mathematics（Synthese Library 第407巻）, Springer, 437〜453頁, 2019年

第４部 ── なぜ依存型を使わないのか

依存型とは何か

Rocq と Lean 4 は、依存型 という仕組みを土台にしています。

依存型 とは、型の中に値が入る型のことです。

たとえば、「長さ 3 のリスト」という型 を、直接宣言して用いることができます。
ここで、型の中に「3」という値が入っています。

これは強力です。

「空でないリストの先頭を取る関数」 を定義したとき、空のリストを渡すプログラムを、実行する前に弾かくことができるからです。

型 が、「長さ１以上」のリストである、と約束（宣言）しているから です。

型と証明の関係 については、筆者が以前に書いた記事で、Python の型ヒントの延長として説明しています。**

以下の記事では、依存型と、それに近い「篩型」という仕組みの違い も扱っていますので、この節の内容をさらに深掘りして追いかけたい方は、ご一読いただけますと幸いです。

• Python の型ヒントの限界を超える「篩型」入門 ── "x > 0" を型に書くと何が起きるのか

依存型そのものについては、Rocq の記事と Cubical Agda の記事でも扱っています。

Isabelle は「依存型」を採用しない選択をした

Isabelle/HOL は、依存型を採用せず、高階論理を採用しています。

この２つは、できることが違います。

高階論理でできること
「すべての性質 P について」「すべての関数 f について」という主張を書くことができます。
個々の数だけでなく、性質そのものや関数そのものを、量化の対象にできるのです。数学の大部分は、この表現力で書き表せます。

依存型でできること
型の中に、値を書き込めます。 「長さ３のリスト」「２以上の自然数」といった型を、直接定義できます。すると、型を検査する段階で、条件を満たさない値を弾けます。 「空でないリストの先頭を取る関数」に空のリストを渡すプログラムは、実行する前にエラーになります。

Isabelle/HOL は、「長さ $n$ のリスト」という型を、直接書くことはできません。
同じことを表現したければ、型ではなく、証明する主張の中に条件として書き込む方法を取らざるを得ません。

具体例で見てみましょう。

「リストの先頭の要素を取り出す関数」を考えます。

空のリストには先頭がないので、この関数は空のリストに対しては使えません。

依存型を持つ Rocq や Lean 4 では、次のように表現することができます。

「空でないリスト」という型を作り、関数の引数の型 を その型 にします。

その結果、空のリストを渡そうとしたコードは、実行される前に型の検査で弾かれるようになります。
誤りが、動かす前に見つかるのです。

Isabelle/HOL では、そうはいきません。
引数の型は、ただの「リスト」です。

空のリストも渡すことを許してしまいます。

どうするのかというと、定理を書くときに条件を明示します。

theorem "xs ≠ [] ⟹ hd xs ∈ set xs"

上記のコードは、「xs が空でないならば、xs の先頭は xs の要素である」を意味しています。

xs ≠ [] という部分が、書き添えた条件です。
「空でない場合に限り、 この主張が成り立つ」と述べているわけです。

そして、この定理を使う場面が来るたびに、「いま扱っているリストは空ではない」ことを証明する必要があります。

違いは、いつ、誰が確かめるかです。

依存型 ならば、型の検査が自動で確かめます。

Isabelle/HOL では、証明の中で人が示します。
条件は書き手が意識して持ち運び、必要な箇所で証明しなければなりません。

書く手間は、確かに増えます。

それでも Isabelle がこの設計を選んだ理由が、次に述べる 自動化 です。

単純さが自動化を容易にする

答えは、自動化 です。

Isabelle/HOL を 数学の形式化に 使った研究者たち（ポールソン自身も共著者です）が、この設計について次のように述べています。

単純な型の仕組みと古典論理が、強力な自動化を可能にしている。これは大きな利点である。

出典は、次の論文です。

• Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson, "Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL", Experimental Mathematics 第31巻第2号, 401〜412頁, 2022年

型の仕組みが複雑になるほど、機械が扱うべき情報は増えます。

証明を自動で探そうとしても、探索の範囲が広がりすぎて手に負えなくなる。

型の仕組みを単純に保つことは、機械に仕事を任せるための条件だったのです。

ポールソン自身も、後年のブログで次のように書いています。

私が依存型理論より高階論理を好む理由の一つは、単純な意味論、うまく機能する等号、すべてをカーネルに入れる必要がないことに加えて、依存型は自動化をはるかに困難にするように思われることである。

技術的な事情も、この見方を裏づけています。

証明を自動で探す外部の道具 は、一階述語論理 や 高階論理 を前提に作られています。

Isabelle の場合、内部の表現をこれらの道具の言葉へ翻訳するのが比較的容易です。

その一方で、依存型を持つ言語 では、この翻訳が難しくなります。

Rocq や Lean 4 でも同種の道具が開発されていますが、翻訳の仕組みを一から設計し直す必要がありました。

Isabelle/HOL は、古典論理 を採用する選択をしました。

排中律（ $A$ が成り立つか、成り立たないか、どちらかである） と 選択公理 を認める立場を選択したのです。

この選択も、自動化に有利に働きます。

外部の自動証明器の多く は、古典論理を前提に作られている からです。

ここにあるのは、設計上の重心の違いです。

Isabelle/HOL の表現力が低いわけではありません。
Isabelle/Hol 数学の大部分を書けるだけの力を持っています。

また、依存型を採る処理系でも自動化の研究は進んでいます。

それでも、表現力を最大限に追求する方向ではなく、自動化しやすい単純な型の仕組みを選ぶ。

Isabelle/HOL の設計には、そうした重心の置き方があります。
次の第５部が、その選択がもたらしたものです。

第５部 ── sledgehammer: 証明を機械に探させる

「証明を機会に探させる」という表現についての補足 から始めさせてください。

sledgehammer が探しているのは、正確には「使うべき定理」です。

証明そのものを組み立てるのは Isabelle 自身です。

詳しくは本節の後半で説明いたします。

何をする道具か

sledgehammer（スレッジハンマー、大槌の意味）は、Isabelle の 生産性を支える中核部分 です。

証明したい命題を書いた状態で sledgehammer と打つと、sledgehammer が動き出します。

まず、sledgehammer が、標準ライブラリ と Archive of Formal Proofs に収蔵されている約27万9千の補題の中から、その命題の証明に使えそうな定理を選び出します。

数百から数千に及ぶ候補です。

次に、sledgehammerが選び出した定理そのものを、外部の証明器へ渡します。

Z3、CVC4、Vampire、E といった証明器 が、並列に走ります。

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

これらの外部の証明器は、Isabelle とは別に開発されたソフトウェア です。**

Isabelle のライブラリを読む機能も、Isabelle の内部構造を知る手立ても持ちません。
**外部の証明器が使うことができるのは、sledgehammer から渡された定理だけ です。

つまり、ライブラリから定理を選び出すのが sledgehammer の仕事であり、渡された定理を組み合わせて証明を探すのが外部の証明器の仕事です。

そして、この分担のもとでは、sledgehammerがどの定理を渡すかが、結果を左右します。

候補が多すぎれば探索が終わらず、少なすぎれば必要な定理が漏れる。

この絞り込みの精度が、sledgehammer の性能を決めます。

そして、選び出された定理を受け取った Z3、CVC4、Vampire、E といった外部の証明器が、証明を探します。
前述のとおり、複数の外部の自動証明器（Z3、CVC4、Vampire、E など）は、並列に動きます。

これら外部の自動証明器は、それぞれ得意とする問題が互いに異なります。

sledgehammer は、証明に使えそうな既知の定理を大量の候補から選び出し、それらを各証明器に渡して、答えを待ちます。

そして、外部の証明器にうち、どれかが証明を見つけたら、その結果を Isabelle の証明として使える形に変換します。

ところで、外部の証明器が出した証明を、Isabelle は正しいかどうかを検証することができません。

外部の証明器は Isabelle とは別に開発されたソフトウェアであり、その内部で行われた推論は、Isabelle のカーネルが検査できる形をしていないから です。

そこで sledgehammer が受け取るのは、「外部の証明器が、その証明の中で実際に使用した定理の一覧」だけです。

数百から数千の候補を渡したうち、実際に必要だったのは数個であることがほとんどです。

そして、その数個の定理を材料に、Isabelle の内部で証明を組み立て直します。

ここで使われるのが、Isabelle に組み込まれた metis という証明の仕組みです。組み立て直された証明は、Isabelle のカーネルによって検査されます。

外部の証明器を信用しないこと。 これは Isabelle の設計思想そのものです。ポールソン自身が、こう書いています。

外部の証明器を信用しないことは、我々の LCF の精神に本質的なものである。

外部の道具の力を借りながら、正しさの保証は自分のカーネルで完結させる。

この２段構えが、sledgehammer という仕組みを成り立たせています。

素朴な疑問と疑問に対する回答

ここで、疑問が浮かぶかもしれません。

「外部の証明器が出した証明を捨てるなら、はじめから sledgehammer が選んだ定理を Isabelle に渡せばよいのではないか。外部の証明器を呼ぶ意味はあるのか」

意味はあります。

sledgehammer が選び出すのは、数百から数千の定理です。

この量の定理を渡されても、Isabelle は証明を組み立てることができません。

どの定理とどの定理を、どの順序で組み合わせればよいのか、手がかりがないからです。

外部の証明器がしているのは、この数百から数千を、実際に必要な数個まで絞り込むことです。

Z3 や Vampire は、大量の論理式の中から必要な組み合わせを探し当てるために、何十年もかけて磨かれてきた専用の道具 です。この探索を現実的な時間で終わらせられるのは、そうした専用の道具だけです。

そして、必要な数個が分かってしまえば、話は変わります。

「この５つの定理を組み合わせればよい」と分かった状態から証明を組み立てるのは、Isabelle にとって難しくありません。

探し当てるのは難しいが、答えを教われば組み立てるのは易しい。 この差を利用しているのです。

つまり、外部の証明器の成果は捨てられていません。

捨てられるのは、外部の証明器が組み立てた証明の中身だけです。

「どの定理を使えばよいか」という最も価値のある情報は、外部の証明器からIsabelleへと、しっかりと手渡されているのです。

証明に使えそうな定理の候補の絞り込みは、２段階で行われている

つまり、定理の絞り込みは、２段構えで行われているのです。

第１段は、sledgehammer による絞り込みです。

標準ライブラリと Archive of Formal Proofs にある約27万9千の補題から、その命題に関係しそうなものを 数百から数千 まで絞ります。この段階では、「関係がありそうか」 という粗い基準で選んでいます。

第２段は、外部の証明器による絞り込みです。

sledgehammer が渡した数百から数千の定理を受け取り、実際に証明を組み立ててみることで、本当に必要な定理を数個まで絞り込みます。 こ

こでは、「実際に使えるか」 という厳密な基準で選ばれます。

約27万9千から、数百から数千へ。そして数個へ。 これが、絞り込みの流れです。

そして、この数個が分かった状態で、Isabelle が証明を組み立て直します。

なぜ２段に分けるのでしょうか。

第１段を飛ばして、約27万9千の補題をそのまま外部の証明器に渡すことはできません。

外部の証明器は、数万を超える論理式を扱えないからです。まず粗く絞る必要があります。

逆に、第２段を飛ばすこともできません。

数百から数千の定理を渡されても、Isabelle はそこから証明を組み立てられません。
どれとどれを組み合わせればよいのかを探し当てる作業が、外部の証明器の仕事 だからです。

粗く絞るのが sledgehammer、厳密に絞るのが外部の証明器。

この分担が、sledgehammer という仕組みを成り立たせています。

実際の出力

コードを見てみましょう。

lemma "rev (rev xs) = xs"
  sledgehammer

lemma は 「これから証明する命題」の宣言 です。

中身は「リストを２回反転させると、元に戻る」という主張です。

rev は ライブラリの関数、
xs は 筆者が任意に付けた名前 です。

そして、２行目に sledgehammer と書きます。
証明の中身は、一行も書いていません。

実行すると、証明器の名前 とともに、次のような形の提案 が返ってきます。

"e": Try this: by simp

先頭の "e" は、証明を見つけた外部の証明器の名前です。

これは E prover という自動証明器を指します。
ドイツの Stephan Schulz が開発したもので、Vampire や SPASS と並び、この分野で長く使われてきた道具です。

sledgehammer は、複数の証明器を同時に走らせ、最初に答えを出したものの名前を表示します。

続く Try this: は、「これを試してください」という提案です。

そして by simp の部分が、その提案の中身にあたります。

ここで、simp について説明しておきます。

simp は、定理の名前ではありません。Isabelle に組み込まれた証明の手法の名前です。
「簡約規則を使って、式を簡単にせよ」という指示にあたります。

Isabelleの標準ライブラリ には、簡約に使ってよい規則 として印を付けられた定理が大量に登録されています。

simp と打つと、Isabelle はそれらの規則を使って式を変形し続け、それ以上簡単にできない形まで持っていきます。

その結果、証明したい命題が明らかに成り立つ形になれば、証明は完成します。

つまり、この提案が言っているのは、こうです。

「E prover が調べたところ、この命題は simp に任せれば片付きます。外部の証明器を呼ぶ必要すらありません」

利用者は、提案された部分をそのままコードに書き写せばよいのです。

lemma "rev (rev xs) = xs"
  by simp

なお、提案される証明の手法は、simp だけではありません。
命題によっては auto、metis、smt といった名前が返ってきます。metis は、外部の証明器が見つけた証明を、Isabelle の内部で組み立て直すための手法です。

lemma "rev (rev xs) = xs"
  by simp

これで証明が完成します。

ここで、誤解のないように補足します。 この命題が by simp の一語で片付いたのは、AI のように、何もないところから証明を考え出したからではありません。

Isabelle の標準ライブラリには、リストに関する定理が大量に蓄積されています。その中に、この命題を自明にする規則が既に含まれていました。sledgehammer がしたのは、「この命題は、標準の簡約の仕組みに任せれば片付く」と見抜いて提案することです。

既に証明された膨大な資産の中から、いま使えるものを探し出す ── これが sledgehammer の働きです。

なお、提案される証明の方法はさまざまです。simp（簡単にする）のほか、metis、smt といった名前が返ってくることもあります。

metis は、外部の証明器が見つけた証明を、Isabelle の内部で組み立て直すための仕組みです。

ここが重要な点です。

外部の証明器が「証明できた」と言っても、Isabelle はそれをそのまま信用しません。外部の証明器が使った定理の一覧を取り出し、それをもとに Isabelle の中で証明を組み立て直します。

最終的な判定を下すのは、あくまで Isabelle のカーネルです。

もう少し本格的な例

先ほどの例は、by simp の一語で片付く簡単なものでした。

実際の証明では、複数の定理を組み合わせる必要が出てきます。

次の命題を考えてみましょう。

lemma "(a::nat) ≤ b ⟹ c ≤ d ⟹ a * c ≤ b * d"

日本語にすると、「自然数 $a$ が $b$ 以下で、且つ $c$ が $d$ 以下ならば、$a$ と $c$ の積は、$b$ と $d$ の積以下である」となります。

ここで sledgehammer と打つと、複数 の証明器が 並列 に走り、それぞれが異なる提案を返してきます。

"e": Try this: by (simp add: mult_le_mono)
"vampire": Try this: by (metis mult_le_mono1 mult_le_mono2 le_trans)
"z3": Try this: by (metis mult_le_mono)

３つの証明器が、３通りの提案を出しました。

提案の中身を読む

それぞれが使っている定理を見てみましょう。

mult_le_mono ── 「$a ≤ b$ かつ $c ≤ d$ ならば、$a × c ≤ b × d$」。求めている命題そのものに近い定理が、標準ライブラリに既にありました。

mult_le_mono1 ── 「$a ≤ b$ ならば、$a × c ≤ b × c$」。片方だけを動かした場合の定理です。

mult_le_mono2 ── 「$c ≤ d$ ならば、$a × c ≤ a × d$」。もう片方を動かした場合の定理です。

le_trans ── 「$a ≤ b $かつ $b ≤ c$ ならば、$a ≤ c$」。不等号をつなぐための定理です。

Vampire の提案は、３段構えです。

まず mult_le_mono1 で $a$ を $b$ に置き換え、
次に mult_le_mono2 で $c$ を $d$ に置き換え、その２つを le_trans でつなぐ。
遠回りですが、確かに証明になっています。

証明の道筋を順に追ってみましょう。

示したいのは a × c ≤ b × d です。

第１段。 mult_le_mono1 は「$a ≤ b$ ならば、$a × c ≤ b × c$」という 定理 です。
前提 から $a ≤ b$ が使えるので、これを 適用する と $a × c ≤ b × c$ が得られます。

この式を見比べてください。

左辺は $a × c$、右辺は $b × c$ です。
掛けられている $c$ は、どちらも同じです。
違うのは、その相手が $a$ であるか $b$ であるかだけです。

『$a$ は $b$ 以下』 なのですから、
同じ $c$ を掛ければ、$a × c$ のほうが $b × c$ 以下になる。

これが、この定理 の述べていることです。

第２段。 mult_le_mono2 は「$c ≤ d$ ならば、$b × c ≤ b × d$」という 定理 です。

前提 から $c ≤ d$ が使えるので、これを　適用する　と $b × c ≤ b × d$ が得られます。

今度は右側だけを、$c$ から $d$ へ置き換えました。

第３段。 ここまでで、２つの不等式が手元にあります。

• $a × c ≤ b × c$
   
• $b × c ≤ b × d$

真ん中に、同じ $b × c$ があります。
そこで le_trans の出番 です。

この 定理 は、「$x ≤ y$ かつ $y ≤ z$ ならば、$x ≤ z$」という、不等号をつなぐためのもの です。これを使うと、$a × c ≤ b × d$ が導かれます。

これが、示したかった命題です。

左側と右側を、一度に動かすのではなく、片方ずつ動かして、最後につなぐ。
遠回りですが、確かに証明になっています。

E prover と Z3 の提案は、一発です。
mult_le_mono という、まさに求めているものに近い定理 を 見つけて きました。

ただし、この２つの提案も、同じではありません。

（コードを以下に再掲します。なお、Vampireから返された提案は省略した上で再掲しています）

"e": Try this: by (simp add: mult_le_mono)
"z3": Try this: by (metis mult_le_mono)

E prover は by (simp add: mult_le_mono) を返しました。

これは「mult_le_mono を簡約の規則に加えたうえで、simp で証明せよ」という指示です。

Isabelle に組み込まれた簡約の仕組みを使う形です。

Z3 は by (metis mult_le_mono) を返しました。

こちらは「mult_le_mono を使って、metis で証明せよ」という指示です。

metis は、Isabelle の内部で外部の証明器と同じ方式の推論を行う仕組みです。

使う定理は同じでも、その定理をどう使うかの指示が違うのです。

simp は式を変形していく仕組み、
metis は論理の推論を組み立てる仕組みです。

同じ結論に、別の道筋で到達しています。

どれを採用するか

ここで、エンジニア（人間）の判断が入ります。

３つとも正しい証明です。

どれを書き写しても、Isabelle のカーネルは通ります。

では、何を基準に 選ぶのでしょうか。

第１に、短いものを選びます。

使う定理が少ないほど、後で読むときに追いやすくなります。
この例では、E prover と Z3 からの提案が短いです。

第２に、後の変更に強いものを選びます。
定理を多く使う証明は、そのうちの一つでもライブラリの更新で名前が変われば、壊れます。
使う定理が少ないほど、壊れる可能性も減ります。

第３に、証明の手法を見ます。

E prover は simp add: を、
Z3 は metis を提案しました。

simp のほうが速く動くことが多く、また Isabelle の標準的な仕組みなので、こちらを好む書き手が多いようです。

この例では、E prover の提案を採ることになるでしょう。

lemma "(a::nat) ≤ b ⟹ c ≤ d ⟹ a * c ≤ b * d"
  by (simp add: mult_le_mono)

絞り込みは、sledgehammer 自身も行っている

なお、この「短くする」作業は、sledgehammer 自身もある程度行っています。

外部の証明器は、必要以上に多くの定理を使って証明を組み立てることがよくあります。

そこで sledgehammer には 最小化の機能 が備わっており、返ってきた定理の集合から一部を取り除いて再度試す、という作業を繰り返し、本当に必要な定理だけに絞り込みます。

Vampire が三つの定理を返してきたのは、最小化を経てもなお、３つ必要だったということです。
証明の道筋が違えば、必要な定理の数も変わります。

エンジニアの仕事は、機械が絞り込んだ複数の提案から、後で読みやすいものを選ぶこと。

ここが、人間に残された判断です。

この仕組みの意味

ここで、sledgehammer が何をしているのかを正確に述べておきます。

sledgehammer が返すのは、証明そのものではありません。

「この方法を試せば証明できそうだ」という 提案 です。

実際に証明を組み立てるのは、その提案を受け取った Isabelle 自身です。

流れを整理すると、こうなります。

1. エンジニアが、証明したい命題を書く
    
2. sledgehammer が、外部の証明器（Z3、Vampire、E など）に問い合わせる
    
3. 外部の証明器が、証明の候補を見つける
    
4. Isabelle が、その候補をもとに証明を組み立て直す
    
5. カーネルが、組み立てられた証明を検査する

外部の証明器の言うことを、Isabelle はそのまま信じません。
必ず自分で組み立て直し、カーネルの検査を通します。
だからこそ、外部の道具の力を借りながら、正しさの保証は失われないのです。

人間のプログラマが書いたのは、証明したい命題だけです。
証明の道筋 は、sledgehammer と外部の証明器が探しました。

もちろん、いつも成功するわけではありません。

難しい命題では、sledgehammer は答えを見つけられずに終わります。

そのときは、エンジニア（人間）が 補助の定理を先に証明しておくなどして、道筋を作ってやる必要 があります。

しかし、日常的に現れる多くの命題は、この一語で片が付きます。

証明を書く作業のうち、退屈な部分を機械に任せられる。

これが Isabelle の生産性 を支えています。

ここで、疑問を抱かれるかもしれません。

「どうせ Isabelle が組み立て直すなら、外部の証明器に渡す意味はあるのか」

外部の証明器に渡す意味はあります。その理由を説明いたします。

外部の証明器から受け取るものは、証明そのものではありません。
「外部の証明器が、その隙間を埋める証明を組み立てるにあたって使用した定理の一覧」です。

外部の証明器は、自分の内部では証明を完成させています。
しかし、その証明を Isabelle はそのまま受け取りません。

外部の証明器は、Isabelle とは別に開発されたソフトウェアです。

その内部で行われた推論が本当に正しいかどうかを、Isabelle は確かめる手立てを持ちません。
外部の証明器が「証明できた」と言っても、Isabelle にとっては、検査していない主張にすぎない のです。

そこで、Isabelle は、定理の一覧だけを受け取ります。

この一覧を手がかりに、Isabelle は自分で証明を組み立て直すのです。

そして、組み立て直した証明を、自分のカーネルで検査します。
カーネルを通ったものだけが、Isabelle にとっての証明です。

sledgehammer が渡す候補は、数百から数千に及びます。

その中から、実際に必要だった定理はこれとこれだ、と絞り込んで返してくるのが、外部の証明器の仕事 です。

この絞り込みは、総当たりでは終わりません。
何十年もかけて磨かれた専用の道具だからこそ、現実的な時間で見つけられます。

そして、必要な定理のリストが絞り込まれたあとの作業は、作業負荷が軽減化されています。

「この５つの定理を組み合わせればよい」と分かってしまえば、Isabelle が自分で証明を組み立て直すのは容易です。

必要な定理を探し当てるのは難しいが、必要な定理さえ探り当ててもらえれば、後続の証明を組み立てる作業は、負荷が軽減化されるのです。

上位の役割分担を整理すると、こうなります。

• sledgehammer ── 膨大な既存の定理から、使えそうな候補を数百から数千の規模で選び出す
   
• 外部の証明器 ── その候補の中から、実際に必要な定理を数個まで絞り込む
   
• Isabelle ── 絞り込まれた定理を使って、自分のカーネルが認める形の証明を組み立てる

外部の証明器は、Isabelle とは別に開発されたソフトウェアです。

その中身が正しいかどうかを、Isabelle は確かめようがありません。

だからこそ、使った定理のリストだけを受け取り、証明そのものは自分で作り直す のです。

証明できないときは、反例を探す

Isabelle には、反対方向の道具 もあります。

nitpick と Quickcheck は、命題が成り立たない例を探す道具です。

証明しようとして行き詰まったとき、実は命題そのものが間違っている、ということがあります。
条件を書き忘れていた、特殊な場合を見落としていた、といった具合です。

そうしたとき、これらの道具が反例を見つけて示してくれます。

「$n = 0$ のとき、この命題は成り立ちません」と教えてくれるわけです。

証明を探す道具と、反例を探す道具の両方がある。
これも Isabelle の特徴です。

大規模な開発を支える仕組み

Isabelle には、大きな検証を進めるための仕組み もあります。

AWS が NIEの検証 で活用したと述べているものを、２つ挙げます。

型クラス は、第３部でも触れた仕組みです。

「足し算ができる型」といったまとまりを作り、+ という記号に、整数にも実数にも機械語の語にも自然な意味を与えられます。

ロケール（locale）は、仕様の階層を作るための仕組み です。

「こういう前提が成り立つ状況」をひとまとまりとして定義し、その中で 証明を積み上げられます。

そして、その前提を満たす具体的な対象 が見つかったとき、積み上げた証明をまとめて適用できます。

大きな検証 では、仕様が何層にも重なります。**

これらの仕組みが、その階層を整理して扱うことを可能にしています。**

第６部 ── Isar: 数学の答案のように証明を書く

２つの書き方

Isabelle には、証明を書く方法が ２通り あります。

タクティクスタイル は、処理系への指示 を並べる書き方です。

• 「ここで場合分けせよ」
• 「これを簡単にせよ」

という 命令を順に書きます。

Isar（アイザー）は、数学の答案に近い形で証明を書く方法です。

• 「仮定する」
• 「よって」
• 「示す」

という語を使い、論証の筋道をそのまま書きます。

Isar は、マルクス・ヴェンツェル が開発しました。

博士論文は2002年、ミュンヘン工科大学に提出されています（実装自体は1999年の版に入っていました）。

同じ定理を、両方の書き方で

同じ定理を、２通りに 書いてみます。

「すべての自然数 $n$ について、$n$ に $0$ を足しても $n$ のままである」という 定理 です。

タクティクを並べる記法の場合

まず、タクティクを並べるスタイル です。

theorem add_zero: "n + 0 = (n :: nat)"
  apply (induction n)
   apply simp
  apply simp
  done

(n :: nat) という書き足しに、注目してください。

これは「$n$ は自然数である」という 型の指定 です。

なぜ必要なのでしょうか。

Isabelle/HOL では、+ や 0 は 型クラス の仕組みによって、自然数にも整数にも実数にも使える ようになっています。

そのため、単に n + 0 = n と書くと、処理系は $n$ がどの型なのかを決められません。
すると、「どの型について の場合分けをすればよいのか」も決まらず、証明が進みません。

型を明示することで、自然数についての場合分けが使えるようになります。

この一手間には、意味があります。

型を明示する ということは、機械が探すべき範囲を、こちらから狭めてやることです。

自動化が強力であるほど、探索の範囲を絞ることは、大きな効果をもたらします。

人間のエンジニアが機械に与えるのは、証明そのものではなく、探す範囲の手がかりなのです。

apply に続くのが、処理系に対する指示 です。

induction n（$n$ について場合分けせよ）、
simp（簡単にせよ）が並び、
done で終わります。

指示の列であって、証明過程（証明の道筋）を綴った文章ではありません。

Isar記法の場合

次に、Isar で書きます。

theorem add_zero: "n + 0 = (n :: nat)"
proof (induction n)
  case 0
  show "0 + 0 = 0" by simp
next
  case (Suc k)
  show "Suc k + 0 = Suc k" by simp
qed

予約語だけを拾って並べてみてください。

theorem（定理）、proof（証明）、case（〜の場合）、show（示す）、next（次に）、qed（証明終わり）。

数学の答案の書き方が、そのまま言語の予約語になっています。

Isar記法のコードをそのまま人間の目で読むと、日本語（や英語、中国語）の証明文になります。

「定理:　$n + 0 = n$。
　証明: $n$ について場合分けする。
$n$ が $0$ の場合、$0 + 0 = 0$ を示す。
次に、$n$ が $k$ の次の数である場合、$Suc k + 0 = Suc k$ を示す。
証明終わり。」

なお、Suc k は、「$k$ の次の数」 を表します。

Isar には、他にも論証のための語があります。

代表的な語彙を挙げると、 assume（仮定する）と thus（よって）があります。

assume "P"
thus "P ∨ Q" by simp

「P を仮定する。よって、P または Q が成り立つ」と読めます。
２行のコードが、そのまま日本語の論証になっています。

より長い証明では、これらを重ねて論証の筋道を組み立てていきます。

この書き方の価値

証明は、書くだけのものではありません。
他の人間や、数か月後・数年後に自分（人間）が読むものです。

数か月後に自分が読み返すとき、他の人が査読するとき、論文として発表するときに、
論証の筋道が文章として読めることは、大きな価値を持ちます。

なお、この「宣言的スタイル」という書き方については、本記事とは別に、独立した記事を近く公開する予定です。

Mizar という言語が最初に示したこの方式が、どのように他の言語へ広がったのか。
そして、AIが証明を書く時代にこの書き方が持つ意味を、より多くのコード例とともに扱います。

タクティク記法と Isar 記法は、どう使い分けるのか

ここで、自然な疑問が生じます。

「Isar のほうが読みやすいのなら、すべて Isar で書けばよいのではないか」

この問いに答えるには、まず 一方でしか証明できない命題があるのか を確かめる必要があります。

答えは、ほとんどの場合「ない」です。

Isabelle の公式文書(The Isabelle/Isar Reference Manual)は、タクティク記法 について次のように述べています。

Isabelle/Isar は、構造化された証明文書を中心に据えている。とはいえ、証明の状態を後ろ向きに段階的に洗練していくことで、証明スクリプトを模倣することは可能である。

つまり、タクティク記法でできることは、Isar でも書けます。
実際、Isar には apply を埋め込む仕組みがあり、両者を混ぜて書くこともできます。

ただし、例外もあります。

同じ公式文書 には、続けてこう書かれています。

構造化された Isar の証明からは触れられない、暗黙の証明状態の情報を参照できる証明手法も、いくつか存在する。

証明の途中で機械が内部に持っている情報に、直接触れる必要がある場面。

ここだけは、タクティク記法でなければ書けません。

ただし、これは 特殊な状況 であり、日常的な証明で遭遇することはほとんどありません。

では、なぜタクティクを使うのか

理由は、書いているときの都合です。

第１に、探索に向きます。

証明を書き始めた時点では、どういう道筋で証明できるのかが分かっていません。

apply auto と打ってみて、何が残るかを見る。
apply (induction n) と打って、場合分けの形を確かめる。

手を動かしながら道筋を探る作業に、タクティク記法は向いています。

Isar で書くには、「何を仮定し、何を示すのか」を先に決めておく必要があります。

道筋が見えていない段階では、この形では書き始められません。

第２に、短く済みます。

同じ証明を書いても、Isarは行数が増えます。
中間の主張を明示的に書き出すためです。

使い捨ての補題や、自明に近い命題までIsarで書くのは、労力に見合いません。

実務での使い分け

多くの書き手は、次のように使い分けているようです。

まずタクティクで書いて、道筋を見つける。

apply を並べ、sledgehammer を打ち、試行錯誤しながら証明を完成させる。

そのうえで、残すべきものを Isar に書き直す。

• 後で読み返す可能性のある証明
• 他の人が読む証明
• 長く保守される証明

これらは Isar で書いておく価値があります。

すべてを Isar にする必要はありません。
一行で片付く補題は、by simp のままでよいのです。

保守のしやすさという観点

もう一つ、見過ごせない違いがあります。

Isabelle の開発者たちは、Isar について次のように述べています。

Isar は、証明の書き手が読みやすさと保守しやすさの適切な均衡を得ることを可能にする。
定義や定理の記述に小さな変更を加えたとき、証明への変更もそれに見合った小ささで済むようにできる。

タクティクの列は、変更に弱いという性質があります。

ある定義を書き換えると、apply が生み出す部分目標の数や順序が変わることがあります。
すると、その後に続く apply の列が、すべて崩れます。

Isar では、「何を示すのか」が各段階に書かれています。
定義が変わっても、示すべきことが変わらなければ、証明の骨格は保たれます。
壊れる範囲が、局所に留まるのです。

Archive of Formal Proofs も、Isar を推奨しています。

投稿の案内には「apply スタイルより構造化された Isar の証明を好むが、義務とはしない」と書かれています。

長く保守されるアーカイブだからこその方針でしょう。

コラム:Isar のような書き方は、他の言語にもあるのか

「仮定する」「よって」「示す」という語を使い、数学の答案に近い形で証明を書く方式 は、Isabelle だけのものではありません。

この方式は 宣言的スタイル（ declarative style ）と呼ばれ、複数の定理証明支援系 に取り入れられています。

この方式を最初に示したのは、Mizar です。

1974年にポーランドで始まったこの言語は、記法が人間の書く数学の文章に極めて近い ことを設計の中心に据えました。

theorem、proof、let、thus、end といった語を並べると、英語の数学の文章として読めます。

Isar は、この Mizar の考え方を受け継いでいます。

では、他の言語はどうでしょうか。

Lean 4 ── have（〜が成り立つ）、show（〜を示す）、calc（等式を順に変形する）といった構文を備えており、宣言的スタイルで書けます。 タクティクスタイルと自由に混ぜることもできます。

HOL Light ── miz3 という仕組みがあります。名前が示すとおり、Mizar の記法をほぼそのまま持ち込んだもの です。

Rocq ── C-zar という宣言的スタイルの記法が作られたことがあります。ただし、Rocq で主流なのは、いまもタクティクスタイルです。

なお、Rocq の SSReflect という拡張は、宣言的スタイルではありません。

日本語の書籍『Coq/SSReflect/MathComp による定理証明』 が扱っているのが この書き方 ですが、SSReflect が整えたのは タクティクの並べ方 であって、「仮定する」「よって」といった語を使えるようにしたわけではありません。

つまり、宣言的スタイルで書ける言語のうち、いま実際に広く使われているのは、Isabelle と Lean 4 です。

Mizar は、この方式を最初に示した言語であり、50年の蓄積を持っています。

しかし、Mizar が採用されている領域は、数学の形式化 に限られ、コミュニティも小さいまま です。HOL Light の miz3 も、限られた範囲での利用にとどまっているようです。

読みやすさと、実際に使われているかどうかは、別の話です。

なお、この「宣言的スタイル」については、本記事とは別に、独立した記事を近く公開する予定です。

• なぜこの書き方が生まれたのか
• 証明が長くなるとどれだけ読みやすさに差が出るのか
• AI が証明を書く時代にこの書き方が持つ意味

と言った論点を、より多くのコード例とともに扱う予定です。

さて。

宣言的スタイルを記述することができる２つの定理証明支援系である Isabelle と Lean 4 は、どちらを選べばよいのでしょうか。

宣言的スタイルという観点で見ると、IsabelleとLean 4には、留意すべき相違点があります。

ひとつ目の違いは、その記法が言語の中心にあるかどうかです。

Isabelle では、Isar が証明を書くための標準の言語です。

公式文書は、「Isabelle/Isar は、構造化された証明文書を中心に据えている」 と述べており、タクティク記法 のほうが 模倣として位置づけられています。

Archive of Formal Proofs も、投稿にあたって Isar を推奨しています。

Lean 4 では、そのあたりの事情が異なります。

have、show、calc といった構文は確かに用意されていますが、タクティクモードが実際の作業の中心です。

この差は、実際の書き方に現れます。

Lean 4 で大規模な形式化を行った研究者たちが、次のように書いています。

calc を使った計算の証明は、更新や書き直しの際にはるかに修正しやすいはずだと我々は考えていた。

しかし、我々の証明のほとんどは、代わりにタクティクモードで一段ずつ書かれた。
calc の証明のほうが読みやすいことも確かで、全体としてはそちらのほうが良い書き方に思える。

唯一の欠点は、形式的な証明を作り上げる過程にある。タクティクの状態を操作しながら進めるほうが、楽に感じられるのだ。

• "Virasoro algebra and Sugawara constructions formally in Lean", arXiv:2510.21741, 2025年

Specifically, we expect that calculational proofs arranged to simple calc steps should be significantly easier to fix during updates and refactors, but most of our proofs were written instead step by step in the tactic mode.

Given that calc proofs are also more readable, they seem like an overall better organization of calculational proofs.

Their only downside is the process of constructing a formal proof: making progress by manipulating the tactic state feels easier.

読みやすいと分かっていても、書きやすさに流れてしまう。 彼らはこの緊張を率直に認め、「コミュニティもこの問題を認識しているようだ」と続けています。

ふたつめの違いは、周囲の環境がどちらを後押しするかです。

Isabelle には、Isar で書くことを支えるものが揃っています。

sledgehammer が提案する証明 は、そのまま Isar の中に埋め込むことができます。
AFP は Isar を推奨 しています。

このように、書き手が自然に Isar へ向かう流れが、道具と文化の両面にあります。

Lean 4 でも、calc を書きやすくする取り組みは進んでいます。

タクティクで書いた証明を calc の形に変換する仕組みも作られました。
ただし、これらはまだ広く定着してはいないようです。

第３の差異は、証明の土台そのものです。

Lean 4 は依存型を採用しており、証明そのものがプログラムの項として表現されます。

そのため、宣言的スタイルとタクティクスタイルに加えて、項を直接書くという第３の書き方も存在します。
選択肢が多いぶん、書き方の統一は難しくなります。

Isabelle には、この第３の道がありません。
選択肢が少ないことは制約ですが、書き方が定まりやすいという利点でもあります。

では、どちらを学ぶべきか

目的によります。

数学の形式化に取り組みたいなら、Lean 4 です。
Mathlib という巨大なライブラリ があり、数学者のコミュニティが最も活発です。

ソフトウェアの検証に取り組みたいなら、Isabelle です。
seL4 と AWS の実績があり、AFP には検証の事例が蓄積されています。

そして、「読める証明を書く」という点に価値を見出すなら、Isabelle のほうが環境が整っています。
Isar が標準であり、周囲の道具も文化もそれを支えている からです。

ただし、これは優劣の話ではありません。

Lean 4 で calc を使って美しい証明を書いている人は、数多く います。

どちらの言語でも、宣言的スタイルで書くことはできます。

違いは、その書き方がどれだけ自然に選ばれるか にあります。

コラム: 記号で書く言語は、他にもある ── APLの場合

「数式のようなコード」という点では、APLという言語も知られています。

APLは、計算をそのまま記述するための言語です。定理証明を行う用途は、想定されていません。

証明を検査する仕組みも、論理式を書き表す仕組みも持ちません。

本記事で扱ってきた定理証明支援系とは、目的がまったく異なります。

そのうえで、数式記号をコードに落とし込めるという点で、Isar記法と比較する価値があります。

1960年代にケネス・アイバーソンが設計したこの言語は、**専用の記号を大量に使います。

+/は総和、⍳は連番の生成、⌽は反転。
配列に対する操作を、一文字で表す のです。

実際のコードを見る

１から100までの合計を求める場合。

+/⍳100

これで終わりです。

⍳100が「１から100までの連番を作る」
+/が「その配列を足し合わせる」

を意味します。

２つの記号だけで、計算が完結しています。

Pythonなら、こう書きます。

sum(range(1, 101))

配列の平均値を求める場合は、こうです。

(+/x) ÷ ⍴x

+/xが合計、⍴xが配列の長さ
÷が除算です。

「合計を個数で割る」という平均の定義が、そのまま記号になっています。

そして、APLの簡潔さを示す例として、素数を求める一行がよく引き合いに出されます。

(~R∊R∘.×R)/R←1↓⍳R

この一行が何をしているのかを、順に説明します。**

⍳Rで連番を作り、
1↓で先頭の１を落とす。
R∘.×Rで、その数列同士の掛け算をすべての組み合わせについて計算し、合成数の一覧を作る。

R∊…で元の数列の各要素がその一覧に含まれるかを調べ、
~で否定する。

含まれないものが素数です。

最後の/Rで、その条件に合う要素だけを取り出します。**

説明を読めば理解できます。しかし、説明なしにこの一行から意図を読み取れる人は、多くないでしょう。

IsarとAPLは、書いている対象が違う

Isarが書くのは、論証の筋道です。

「仮定する」「よって」「示す」という語を並べ、なぜその主張が正しいのかを述べます。

APLが書くのは、計算そのものです。
この配列にこの操作を適用せよ、という手順を記号で簡潔に表します。

同じ「数式のよう」でも、比較の軸が違うのです。

なお、Isabelleで先ほどの合計を扱うなら、計算するのではなく、性質として書きます。

lemma "(∑i=1..100. i) = 5050"
  by simp

「１から100までの合計は5050である」という主張を述べ、それを証明しているわけです。
APLは答えを計算し、Isabelleは答えが正しいことを示す。

役割が違います。

APLが有用な場面

第１に、配列全体を一度に扱う計算です。

ループを書かずに、配列に対する操作を直接記述できます。
行列演算、統計処理、金融の計算など、データ全体に同じ操作を適用する仕事に向きます。

第２に、探索的な作業です。

一行で結果が出るので、対話的に試しながら考えを進められます。
書いては消し、書いては消しという作業に適しています。

第３に、思考の道具としての使い方です。

アイバーソンは、この言語を 記法として 設計しました。
1979年のチューリング賞受賞講演の題は「 思考の道具としての記法 」です。
プログラムを書くためではなく、問題を考えるための記法 という発想でした。

APLの弱点

書いた本人でも、数日後には読めないとよく言われます。

記号が密で、変数名も短く、一行に多くの処理が詰まるためです。

先ほどの素数の一行を思い出してください。
結果への最短経路は示されていますが、そこに至る思考の過程は、どこにも書かれていません。

この読みにくさは、本記事で見たタクティク記法の難点と似ています。

• Isar ── 「仮定する」「よって」と、論証の流れを追える
   
• タクティク記法 ── 指示は並ぶが、何を証明しているのかは見えない
   
• APL ── 計算は完結しているが、なぜその計算でよいのかは見えない

簡潔さと読みやすさは、しばしば両立しません。

どちらを取るかは、その記述を後で誰が読むのかによって決まります。

第７部 ── seL4: 何を証明し、何を仮定したのか

何が検証されたのか

seL4 は、OSの中核部分です。

ここでいう「カーネル」は、証明系のカーネル（判定を下す部分）とは別のもので、オペレーティングシステムの中核部分を指します。

規模は次のとおりです。

項目	数値
検証対象	8,700行の C コード + 600行のアセンブラ
証明	20万行の Isabelle スクリプト
抽象仕様の作成	約4人月
Haskell による試作	約2人年
C 実装	約2人月
証明の労力	約20人年

証明の労力のうち約9人年は、証明そのものではなく、道具立てへの投資でした。
形式言語の枠組み、証明の道具、自動化の仕組み、ライブラリの整備です。

設計そのものが、検証のために工夫されていた

seL4 が成功した理由の一つは、検証しやすいように設計されたこと にあります。

普通、OS のカーネルは最初から C言語で書きます。
しかし seL4 の開発チームは、先に Haskell で試作を作りました。

Haskell は関数型のプログラミング言語で、Isabelle の扱う数学に近い性質を持ちます。

そのため、Haskell で書いたものを Isabelle の定義へ自動的に翻訳する道具 をつくることができました。

設計者は Haskell で試作を書き、それが機械的に Isabelle の世界へ運ばれる。
証明の出発点が、こうして用意されました。

手順を整理すると、次のようになります。

1. 抽象仕様 を Isabelle で書く（カーネルが何をすべきか）
    
2. Haskell で試作 を書く（設計の詳細を詰める）
    
3. 試作を Isabelle の定義へ自動翻訳 する
    
4. C言語で実装 する
    
5. 各段階が、一つ上の段階に従っていること を証明する

この積み重ねによって、Cのコードが抽象仕様に従っていること が導かれます。

もし最初から Cだけで書いていたら、この検証は成立しなかったでしょう。

検証を後から付け足すのではなく、検証できる形で設計する という発想が、seL4 の核心にあります。

証明された性質

証明されたのは、機能正当性 と呼ばれる性質です。
実装が、抽象仕様に厳密に従っていることを示しました。

これは極めて強い性質です。

seL4 の公式サイトは、次のように述べています。

機能正当性は非常に強い性質であり、バッファオーバーフロー、メモリリーク、その他 C プログラムを悩ませる誤りの全クラスが存在しないことが、追加の証明なしに導かれる。

さらに、証明はバイナリコードにまで到達しています。

多くの検証プロジェクトが抽象的なモデルの段階で止まるのに対し、seL4 は、仮定を大幅に減らしています。

何を仮定しているのか

しかし、証明がすべてを保証しているわけではありません。

seL4 の公式サイトには、"What the Proofs Assume"（証明が仮定していること）という頁があります。
そこに明記されているのは、次の項目です。

• Cコンパイラの正しさ
• アセンブラのコードの正しさ（レジスタの保存・復元、カーネル退出時の文脈切り替えは証明されていません）
• ハードウェアが仕様どおり動くこと
• キャッシュの整合性と TLB の管理（アセンブラ層で正しく実装されていると仮定し、これらがカーネルの振る舞いに影響しないと仮定しています）
• ブートコード（8,700行のうち 約1,200行。証明は、カーネルが正しくメモリに読み込まれ、整合的な初期状態になった後の動作についてです）
• DMA

重要なのは、これらの仮定が形式論理の中に明示的に書かれていることです。
隠された仮定ではありません。

どこまでが証明され、どこからが仮定なのかが、はっきりしています。

なお、「OSが数学的に正しいと証明された」という言い方は、正確ではありません。

正確には、「明示された仮定のもとで、実装が仕様に従うことが証明された」 です。

それでも、これは他の多くの検証プロジェクトより、はるかに仮定の少ない成果です。

そして、もう一つ重要な限界があります。

証明が保証するのは「実装が仕様に従うこと」であって、「その仕様が正しいこと」ではありません。

仕様そのものに誤りがあれば、その誤った仕様に忠実な実装が出来上がるだけです。

何を仕様として書くかは、人間が決めます。

この論点については、筆者が以前に書いた記事で正面から扱っています。

• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界

そして2025年、AWS がクラウド基盤の中核を検証した

seL4 は2009年の成果です。では、Isabelle はいまも実務で使われているのでしょうか。

答えは、2025年12月に示されました。

AWS が、Nitro Isolation Engine（NIE）を Isabelle/HOL で形式検証したと発表しました。

NIE は、お客様のデータを守りながら AWS の資源を提供するソフトウェアです。

AWS はこれを、 世界初の形式的に検証されたクラウドハイパーバイザー と位置づけています。

規模は、seL4 に匹敵します。

項目	内容
証明の規模	25万行
検証の対象	Graviton-5 プロセッサの仕様、ハイパーコールの Rust コード の機能正当性、セキュリティ特性の仕様
実行時間	市販のノートパソコンで30分（25万行の証明の再検査）

注目すべきは、AWS が Isabelle を選んだ理由です。
公式の解説には、こう書かれています。

表現力、自動化、証明の読みやすさ、スケーラビリティのバランスが、私たちの用途に最も適していたからです。

本記事でここまで述べてきた 特徴が、そのまま選定の理由として挙げられて います。

技術的にも興味深い点があります。

AWS は、分離論理という特化した論理を、Isabelle/HOL の上に構築しました。

分離論理 は、共有された資源を操作するプログラムを検証するために設計された論理 です。

これは、第２部で述べた「Pure の上に論理を載せる」のとは別の層の話です。

Pure の上に載せるのは HOL や ZF といった 土台の論理 でした。

AWS が実現したのは、その HOLの表現力と拡張の仕組みを使って、その上にさらに特化した論理を組み立てること です。

Isabelle は、どちらの層も拡張できます。

土台の論理を差し替えることも、土台の上に特化した論理を積み上げることもできる。

この柔軟さが、実務での大きな検証を支えました。

なお、この解説記事を書いたのは、Isabelle の作者であるローレンス・ポールソン自身 です。

彼はケンブリッジ大学の名誉教授であると同時に、Amazon Scholar でもあります。

• Isabelle/HOL: Nitro Isolation Engine を支える定理証明支援系（AWS 公式ブログ、日本語訳）

seL4 と NIE 以外の適用先

Isabelle が使われたのは、この２つだけではありません。
20年以上にわたって、さまざまな検証と形式化に使われてきました。

ソフトウェアの検証では、次のようなものがあります。

• WebAssembly ── ブラウザなどで動く実行環境の意味論を形式化し、型システムの健全性を証明 しました
   
• CRDT ── 複数の利用者が同時に編集しても矛盾が起きないようにするデータ構造です。分散編集で使われるアルゴリズムの正当性 が証明されました
   
• Cogent 言語 ── 検証のための枠組みが Isabelle の上に作られました
   
• 暗号プロトコル ── ポールソン自身が、抽象的な段階での検証に Isabelle を使ってきました
   
• Ethereum 仮想機械 ── ブロックチェーンの実行環境を形式化し、スマートコントラクトの検証に使う試みがあります

数学の形式化では、Archive of Formal Proofs に大きな成果が収められています。

• ゲーデルの不完全性定理（ポールソンによる形式化）
• ジョルダン曲線定理
• ラムゼーの定理
• 素数定理（2004年）

ソフトウェア検証と数学の形式化の両方で実績がある ことが、Isabelle の特徴です。
多くの処理系は、どちらか一方に偏ります。

第８部 ── Archive of Formal Proofs:査読つきの証明アーカイブ

Isabelle には、もう一つの資産があります。

Archive of Formal Proofs（AFP） は、2004年に始まった、証明の公開アーカイブです。

• Archive of Formal Proofs

特徴は、学術誌と同じように運営されていることです。

• 投稿は査読されます
• ISSN が付与されており、論文として引用できます
• dblp（計算機科学の文献データベース）に索引されています
• 収録されているのは、数学と計算機科学の両方です
• entries は Isabelle の新しい版が出るたびに、その版で動くように更新されます

規模は、次のとおりです（本記事の執筆時点における公式サイトの統計より。この数値は日々更新されています）。

項目	数値
エントリ数	863
著者数	513名
補題の数	約27万9千
行数	約453万行

ISSN は 2150-914x で、dblp にも索引されています。

運用の仕組みにも触れておきます。

AFPに収められた証明は、Isabelleの新しい版が出るたびに、その版で動くように更新されます。

収蔵して終わりではなく、動き続けるアーカイブなのです。

読みやすい形で証明を書けることと、査読を経て公開できることが、ここで結びついています。

数学の証明を形式化して発表したい研究者にとって、この場の存在は大きな意味を持ちます。

第９部 ── Isabelle の弱点と、不得意なこと

Isabelleが苦手とすることも書いておきます。

依存型を使えないことの制約

第４部で述べたとおり、Isabelle は 依存型 を持ちません。

「長さ $n$ のリスト」のような型を直接書けないため、Rocq や Lean 4 なら型で表現できることを、別の方法で表現する必要があります。

自動化と引き換えに、表現力を手放しているわけです。

コード生成の性格が違う

Isabelle にも、コード生成（code generation）という機構があります。

Isabelle で定義した関数を、Haskell、Standard ML、Scala、OCaml のコードとして出力できます。
出力されたコードは、Isabelle の外で普通のプログラムとして使えます。

ただし、Rocq の抽出とは性格が異なります。

Rocq の抽出 は、証明の中から計算の手順だけを取り出す仕組みです。

「条件を満たす値が存在する」ことを、その値を実際に組み立てて示す。

すると、その組み立ての手順がプログラムとして取り出せる、という発想 です。

Isabelle のコード生成は、書いた関数の定義を、対象の言語へ翻訳する仕組みです。
証明の中から取り出すのではありません。

どちらも実用的ですが、同じものではありません。

Rocq は証明が出発点、
Isabelle は関数の定義が出発点です。

なお、このコード生成には、証明を助ける使い道もあります。

たとえば by eval と書くと、その場でコードを生成して実際に計算させ、結果が正しければ証明を完了させます。

大きな数の計算を含む命題では、これが役に立ちます。

開発環境が限られる

Isabelle の開発環境は、Isabelle/jEdit と Isabelle/VSCode に限られます。

そして、この Isabelle/VSCode には注意が要ります。公式のドキュメントに、次の記述があります。

数学記号のための文字符号化や専用フォントの組み込みのために、VSCodium のコードベース自体に重要な変更を加えている。この拡張が、通常の VS Code や、他の言語サーバー方式のエディタで動作する可能性は低い。

つまり、通常の VS Code に、Isabelle/jEdit と同等の証明環境をそのまま導入できるわけではありません。 テキストとして .thy ファイルを開くことはできても、証明の状態を対話的に確認しながら書き進める環境にはなりません。

この点は、次の第１０部にも関わってきます。

第１０部 ── AI エージェント時代の Isabelle

ここからは、Isabelle の機能そのものではなく、この言語がAIの時代にどう使われ始めているかを見ます。

LLM との組み合わせは、活発に研究されている

Isabelle は、大規模言語モデル（LLM）による定理証明の研究対象として、注目を集めてきました。

理由は２つあります。

読みやすい記法（Isar）を持つことと、強力な自動化（sledgehammer）を持つことです。

LLM が証明の骨組みを作り、残った隙間を sledgehammer が埋める、という 分担 が 自然に成立 します。

主な研究の系譜を挙げます。

研究	年	内容
Thor	2022年	sledgehammer の呼び出しが成功するかを予測するモデルを学習させる
Draft, Sketch, Prove	2022年	LLM が自然言語の証明を生成し、Isar の骨組みに変換。隙間を sledgehammer が埋める
Lyra	2023年	Isabelle の実行結果のエラーを LLM に返し、骨組みを修正させる
Baldur	2023年	LLM で誤った証明を修復する
IsabeLLM	2025〜2026年	専用ライブラリで Isabelle を制御し、LLM と sledgehammer を組み合わせる。Isabelle2025 に対応
Isabellm	2026年	コードのすべてが GPT・Gemini・Claude によって実装された。sledgehammer では通らない補題を証明できたと報告

汎用のコーディングAIからは扱いにくい

一方で、Copilot や Cursor のような汎用のコーディング支援ツールから Isabelle を扱うのは、構造的に難しい状況です。

第９部で述べたとおり、通常の VS Code では Isabelle が動きません。

そのため、これらのツールは Isabelle の証明状態を知ることができません。

ファイルをテキストとして読み書きすることはできても、「いま何が証明済みで、何が未証明か」を把握できない のです。

上に挙げた研究が、いずれも専用のライブラリで Isabelle のプロセスを制御している のは、このためです。

Lean 4 が標準的な言語サーバー方式で動き、汎用のエディタから扱えることと比べると、この差は小さくありません。

変わらないこと

それでも、変わらない構図があります。

これらの研究はすべて、LLM が証明を書き、Isabelle が検査するという組み合わせです。
LLM が最終判定を下すのではありません。判定を下すのは、Isabelle のカーネルです。

AI がどれだけ証明を書けるようになっても、何を証明すべきかを決めるのは人間です。
仕様を書くのは人間の仕事であり、そこは自動化されません。

人間には、AIが生成した証明を読んで、それがソフトウェアの設計や数学の定理として妥当かどうかを判断する能力が求められます。

ここで、Isarで綴られた証明の読みやすさが意味を帯びてきます。

AIが提案してくる証明を、何をしているのか読み取りづらいタクティクの羅列としてではなく、論証の流れを追えるIsarの文章として受け取ることができる。

このことは、AI時代にむしろ価値を増すかもしれません。

人間には、AIが生成した証明を読んで、それがソフトウェア設計の目的や意図や、数学の定理として妥当かどうかを判断する能力が求められます。

この論点は、日本語でも議論されています。

Isabelle の開発者たち自身が、タクティク方式 の証明について、次のように述べています。

従来の手法の問題は、機械が検査した証明を見た者が、ある時点で何が証明されているのかを知りようがないことである。目隠しでチェスをするようなものだ。

ポールソン、ニプコウ、ヴェンツェルの共著論文 "From LCF to Isabelle/HOL" の一節です。

同じ趣旨を、より強い言葉で表した一節も知られています。

タクティクによる証明は、暗黙の証明状態を操作する、多少は構造化されたコマンドの並びである。したがって、証明のテキストは機械にだけ適したものである。人間にとっては、コマンドを一段ずつ実行して状態の変化を目で追えるときにのみ、証明が理解できる。このような証明は、コメントのないアセンブリ言語のプログラムのようなものだ。

こちらはニプコウの言葉として、檜山正幸さんの記事に引用されているものです（筆者は原典を特定できていません）。

Isar は、この状況を変えるために作られました。

Isar と、対話環境である PIDE を開発したウェンツェルは、証明支援系の利用が広がらない原因を「難読な証明記述言語と貧弱な利用者向けの環境」だと考え、両方に取り組みました。

そして、LLM の学習データという観点 からも、同じ問題が指摘されています。

タクティクの羅列 は、機械が実行するには十分でも、そこから何かを学ぼうとする者にとっては情報が足りません。

論証の構造が書かれた証明のほうが、学習の材料としても有益ではないか、という見方 です。

これらの議論は、近く執筆予定の記事で詳しく取り扱う予定です。

AIの証明実績

日本語で読める興味深い実験記録があります。

Gemini と ChatGPT に、実際に定理の証明を書かせてみた という記事です。

• Lean,CoqでAIに証明をしてもらう（xiangze さん、2025年） ── 各種の不等式から、ハーン・バナッハの定理、特異点解消定理、ヴェイユ予想まで

結果は、対象の難易度によって分かれました。

大学の学部程度の定理なら、ライブラリの既存の定理を呼び出してあっさり証明が出てきます。
しかし、大学院を超える水準になると様子が変わります。

注目すべきは、LLM自身が述べた限界です。

数学書には「明らかに」と書かれた論理の飛躍があり、その行間を埋めるのは難しい。

そして プログラムの手直しと違って、証明では新しい概念を発明し、部分的な目標として設定する必要がある。証明の全体像が変わってしまうことを見抜いて方針を変えるのは、いまのAIには困難である。

そう述べられています。

ChatGPT 自身が示した現実的な戦略が、次のものです。

LLM を「自律エージェント」ではなく、優秀なジュニア共同研究者として使う。
定義の雛形・文脈の検索・エラーの説明を即座に返してもらい、人間が理論の骨格を与える。これが当面もっとも現実的な戦略です。

記事の著者も、AI が出力した証明が間違っていた場合に修正できるかどうかは、試行錯誤以上に人間の数学的な素養が要る と書いています。

理論の骨格を与えるのは人間 ── ここでも、同じ結論に辿り着いています。

【筆者の見解】

AIが証明を書く時代において、Isabelle を学ぶ価値 は 失われないと筆者は考えます。

証明を読んで判断する人間の能力 はむしろ、これまで以上に重要になるのではないかと考えています。
ただし、これは筆者の見立てであり、統計に基づくものではありません。

そして、ここには まだ答えの出ていない問い があると筆者は考えています。

Isar は、人間のためだけの書き方なのでしょうか。
それとも、LLM にとっても学習しやすい証明の形式 なのでしょうか。

論証の構造が明示された証明は、人間が読みやすいだけでなく、LLM/ AI Agentが学ぶ材料としても優れているかもしれません。

この問いには、まだ答えが出ていません。

なお、AI がどれだけ自律しても、最終的な判断と責任は人間に残る という論点は、定理証明に限った話ではありません。

筆者は、セキュリティの分野を題材に、この問題をより広く論じた記事を書いています。

• AIがネットワークを隔離すると、証拠が消える ── 「推論できる」ことと「実行させてよい」ことの違い
   
• AIに汚染区画の強制隔離の「引き金」を引かせるべきか ── 自律SOCのガバナンスと説明責任

第１２部 ── 本稿のまとめ:Isabelle/HOL の全体像

ここまでお読みいただいた内容を、整理しておきます。

１. 全体の構造:３つの層

Isabelle は、論理を実装するための枠組みです。
この点が、単一の論理に特化した他の定理証明支援系とは異なります。

構造は、次の３つの層が折り重なった形をしています。

【第１層:メタ論理 Isabelle/Pure】

• 役割 ── 「推論とは何か」を書き表すための土台
   
• 中身 ── 自然数や集合といった数学の内容を、一切持ちません
   
• 持っている道具は、３つだけです
  • ⟹ メタ含意 ── 「$A$ ならば $B$」という規則の形を書くための記号
  • ⋀ メタ全称 ── 「どんな $x$ についても」という一般性を書くための記号
  • ≡ メタ等号 ── 「これをこう定義する」という定義を書くための記号

【第２層:対象論理】

• 役割 ── 実際に議論したい数学の世界。Pure の上に載せるもの
   
• 種類
  • Isabelle/HOL ── 高階論理。最も広く使われています
  • Isabelle/ZF ── ツェルメロ=フレンケル集合論
  • Isabelle/FOL ── 一階述語論理
     
• 通常「Isabelle」と言えば、HOL を載せた状態を指します

【第３層:応用ライブラリと特化した論理】

• 役割 ── HOL の上に、さらに特定の目的のための論理を組み立てる
   
• 例 ── AWS が Nitro Isolation Engine の検証のために構築した 分離論理
   
• 注意 ── これは「Pure の上に載せる」のとは別の層です。HOL の表現力を使って、その上に組み立てる 層にあたります。どちらの層でも拡張できることが、Isabelle の柔軟さの源です

２. 二つの記法

Isabelle には、証明を書くための記法が２通りあります。

【タクティクを並べる記法】

• 書き方 ── apply (induction n) のように、処理系への指示を並べます
   
• 利点 ── 短く書けます。試行錯誤に向きます
   
• 難点 ── コードを読んでも、途中で何が証明されているのかが分かりません。処理系を動かし、証明の状態を追う必要があります

【Isar 記法】

• 書き方 ── assume（仮定する）、thus（よって）、show（示す）などを使い、論証の筋道を文章として書きます
   
• 利点 ── 人間が読んで意味を読み取りやすい。数学の答案のように、上から下へ順によみ進める。
   
• AI 時代における意味 ── LLM が生成した証明を人間が確認する際、Isar で書かれていれば、処理系を動かさずに妥当性を判断できます

３. sledgehammer:自動化の仕組み

Isabelle の生産性を支える中核の仕組みです。

【動作の五段階】

1. 人間が、証明したい命題を書き、sledgehammer と入力する
    
2. Isabelle が、標準ライブラリと AFP にある約27万9千の補題から、関連しそうな定理を選び出す
    
3. 選んだ定理とともに、外部の自動証明器へ問題を渡す。Z3、Vampire、E、CVC4 などが並列に走る
    
4. 外部の証明器が「証明できた」と返しても、Isabelle はそれをそのまま受け取らない。返ってきた「使用した定理の一覧」をもとに、Isabelle の内部で証明を組み立て直す
    
5. 最後に、Isabelle のカーネルが検査する

【この仕組みの原則】

sledgehammer は、「証明を発明する」のではありません。「既にある膨大な定理を組み合わせて、隙間を埋める」仕組みです。 したがって、ライブラリが厚いほど強くなります。

４. 実績と、それを支える資産

【二つの大きな実績】

seL4（2009年）

• 汎用 OS カーネルの機能正当性を、世界で初めて形式検証しました
   
• 8,700行の C コードに対し、20万行の証明。約20人年
   
• 検証しやすいよう、まず Haskell で試作を作り、それを Isabelle の定義へ自動翻訳しました

AWS Nitro Isolation Engine（2025年12月）

• 世界初の形式的に検証されたクラウドハイパーバイザーと位置づけられています
   
• 25万行の証明。市販のノートパソコンで30分で検査し直せます
   
• 対象は、Graviton-5 の仕様と、ハイパーコールの Rust コード

【Archive of Formal Proofs】

• Isabelle 専用の証明アーカイブ。査読つきで ISSN を持ち、学術誌のように運営されています
   
• 規模は863エントリ、約453万行
   
• 数学よりもソフトウェア寄り。記事の約半数が、アルゴリズムの解析と検証を扱っています
   
• Lean 4 の Mathlib は約200万行で、数学の体系化が中心です

５. 苦手とすること

依存型を使えないこと ── 「長さ n のリスト」のような型を直接書けません。表現力を最大化する方向ではなく、自動化しやすい単純さを取った設計です。

開発環境が限られること ── 公式に対応しているのは Isabelle/jEdit と、パッチを当てた Isabelle/VSCode だけです。通常の VS Code に、同等の証明環境をそのまま導入することはできません。 そのため、Copilot や Cursor のような汎用のコーディング支援ツールから扱うには、構造的な難しさがあります。

６. AI時代における位置づけ

LLM との相性 ── Isar 記法があるため、LLM が書いた自然言語の証明を、形式的な骨組みへ変換しやすくなっています。

役割分担

1. LLM ── 論証の骨組みを書く
    
2. sledgehammer ── 骨組みに残った sorry の箇所を埋める
    
3. 人間 ── Isar で書かれた証明を読み、妥当性を判断する

そして、本稿の結論です。

AI が証明の候補を書く時代だからこそ、「何を証明すべきか」という仕様を決め、「出てきた証明が妥当か」を読み解く能力が重要になります。 Isabelle/HOL は、そのための有力な選択肢のひとつだと筆者は考えます。

第１３部 ── 発展的な学習のために:　専門書ではこう書かれています

本記事では、専門用語をできるだけ日常の言葉で説明してきました。

しかし、専門書や論文を読む際には、正式な用語を知っている必要があります。

対応表を置いておきます。

用語の対応

本記事での書き方	専門書での用語
論理を載せる枠組み	メタ論理（metalogic）、純粋論理（Pure logic）
枠組みの上に載せる論理	対象論理（object logic）
証明が正しいかを最終判定する部分	カーネル（kernel）
「すべての関数について」と言える論理	高階論理（higher-order logic、HOL）
「すべての数について」までしか言えない論理	一階述語論理（first-order logic）
型の中に値が入る型	依存型（dependent type）
証明の組み立てを処理系に指示する命令	タクティク（tactic）
数学の答案に近い形で証明を書く方式	宣言的スタイル（declarative style）
タクティクを並べていく書き方	タクティクスタイル（procedural style）
仮定から結論を導く推論の形式	自然演繹（natural deduction）
小さな中核だけを信頼する設計	LCF 方式（LCF-style architecture）
実装が仕様に厳密に従うこと	機能正当性（functional correctness）

表現の対応

本記事での書き方	専門書での書き方
どんな推論を認めるかが、処理系のプログラムの中に直接書き込まれている	演繹系がソースコードに固定的に組み込まれている（hardwired as source code）
Isabelle という枠組みの上に、後から載せる形で作られている	Isabelle のインスタンス化として実装されている（implemented as an instantiation）
関数を扱うための、ごく単純な土台	単純型理論（simple type theory）
証明に使えそうな既知の定理を、大量の候補から選び出すこと	前提選択（premise selection）

第１４部 ── 学び方のロードマップ

日本語の情報は、限られている

Isabelle を主題にした日本語の書籍は、筆者の調べた範囲では見当たりません。

Rocq には、『Coq/SSReflect/MathComp による定理証明』（森北出版） という日本語の書籍がありますが、Isabelle にはこれに相当するものがないのが現状です。

一方で、日本語の情報がまったくないわけではありません。

Qiita には、Isabelle を扱った記事が２本あります。

どちらも本記事より踏み込んだ内容で、次に読むものとして最適です。

• Isabelle入門の入門（@myuon_myon さん、2014年） ── Isabelle の特徴を、利用者の視点から、良い点も難点も含めて列挙した記事です。Isar とタクティクの書き方を、同じ定理で並べて示しています。 本記事の第６部と同じ趣旨の比較を、別の例で読めます
   
• IMPのコンパイル結果の正当性証明（@masateruk さん、2017年） ── Concrete Semantics の演習問題を解く実践記録です。自動証明を試して失敗し、補題を追加して進む過程 が、そのまま書かれています。実際の証明作業がどういうものかを知るのに、これ以上の資料はありません

Qiita以外にも、有益な日本語の資料があります。

• Isabelle/HOLの基本（連載）（myuon さん、2017年） ── 公式チュートリアルに沿って、実際に証明を書きながら進む日本語の連載 です。「英語が読みたくない人や雰囲気だけ知りたい人にも優しい解説」を掲げています
   
• Isabelle ゆるリファレンス（apply-scriptスタイル）（Kuniwak さん、2020年） ── 日本語で最も充実した実用資料です。 よく使うコマンドとメソッドを、使い所とともに網羅しています。自動証明の各手法を「解ける範囲」と「帰ってこなさ」で比較した早見表は、実際に使い始めてから何度も参照することになるはずです。書き手は自動テストの専門家で、テストに限界を感じて形式手法へ進んだ という経緯を公開しています
   
• 定理証明システム：Coq・Lean・Isabelle（TANAAKK、2026年） ── ３つの処理系とライブラリの対応を、短くまとめた記事です。Isabelle の論理を切り替えられる構造 についても触れています

また、大学の研究でも使われており、北海学園大学、関西学院大学、電気通信大学などの論文で Isabelle を扱ったものが公開されています。ユークリッド原論の定理証明や、C プログラムの併合システムの検証といった題材です。

日本企業での実務利用

日本の企業が、業務で Isabelle を使った事例も公開されています。

DeNA の SWET グループ（Software Engineer in Test）は、2022年に 社内で Isabelle/Isar の勉強会 を開催し、その資料と練習問題を GitHub で公開しました。

• Isabelle/Isar勉強会を社内で開催しました（鈴木穂高さん、2022年）
   
• DeNA/IsarTutorial（教材と練習問題、解答例）

業務での用途は、仕様と実装のあいだに正当性の関係が成り立つことを証明する ことでした。同グループでは、OCaml で記述した仕様と実装を Isabelle が読める形に変換し、正当性の関係を証明したと報告されています。

興味深いのは、この分野に来た人の経路です。 SWET はテストの専門集団であり、先ほど挙げた「ゆるリファレンス」の書き手も同じグループの所属でした。テストで品質を担保することの限界を感じた人たちが、形式手法へ進んでいる という流れが見えます。

本記事の読者にも、同じ問題意識をお持ちの方がいるかもしれません。

日本語で読めるその他の議論

Isabelle そのものの解説ではありませんが、日本語で読める重要な議論 も紹介しておきます。

• 定理証明支援系についての問題意識（mod_poppo さん、2025年） ── タクティクの羅列は人間が読めるのか という問題意識を、書籍への掲載や LLM の学習データという観点から論じています。結論として、Agda・Mizar・Isabelle/Isar は見る価値がありそうだ、と述べられています
   
• 証明支援系がダメだった理由と、AIでブーストする理由（檜山正幸さん、2023年） ── なぜタクティク方式が主流になったのか、そして Isar と PIDE でウェンツェルが何を変えようとしたのか を論じています。ニプコウの言葉として、タクティク方式の証明を「コメントのないアセンブリ言語のプログラムのようなもの」と評した一節も引用されています

とはいえ、体系的に学ぶには英語の教材が前提になります。 先ほど挙げた「Isabelle入門の入門」も、この状況を「人口が少ないゆえの必然で、情報はあんまりありません」と書いています。2014年の記述ですが、いまも大きくは変わっていません。

英語の定番

• "Concrete Semantics"（Nipkow & Klein）── 無料で公開されています。前半が Isabelle の入門、後半がプログラミング言語の意味論という構成です。最初の一冊としてこれを勧めます
   
• "Programming and Proving in Isabelle/HOL"（公式チュートリアル、prog-prove）── 無料公開。まずこれを読むよう、日本語のブログでも勧められています
   
• "Isabelle/Isar Reference Manual" ── Isar の詳細。慣れてから参照する資料です
   
• Archive of Formal Proofs ── 他人の証明を読む場として。実際の書き方を学べます

順路

1. 公式チュートリアル（prog-prove）を頭から進める
    
2. 手元に Isabelle を導入し、実際に証明を書いてみる。sledgehammer を打ってみることを勧めます。 この体験が、Isabelle の性格を最もよく伝えます
    
3. "Concrete Semantics" で、より本格的な形式化に進む
    
4. AFP のエントリを読み、実際の証明の書き方を学ぶ

おわりに ── 次に読むもの

本記事では、Isabelle/HOL という言語を紹介しました。

設計の中心にあるのは、「特定の論理に縛られない枠組みを先に作る」という考え方でした。

論理学者が新しい論理を考え出す速さに実装が追いつかない、という1980年代の問題意識から生まれた設計です。

依存型を使わないという選択は、表現力を最大化する方向ではなく、自動化しやすい単純さを取るためのものでした。

その結果が sledgehammer であり、seL4 という到達点です。

この言語の面白さを、一文でまとめるなら、こうなります。

Isabelle/HOL は、「証明を人間がすべて書く」のではなく、「人間が論理と仕様を設計し、機械に証明の探索を任せる」という役割分担を、1980年代から一貫して追求してきた
── Pure から HOL、sledgehammer、Isar、そして seL4 と AWS まで、すべてが同じ一本の線の上にあります。

そして、その設計思想は、2025年に AWS がこの言語を選んだ理由としても現れました。

表現力、自動化、証明の読みやすさ、スケーラビリティのバランス。40年前の設計が、いまの選定理由になっているのです。

ここから先へ進む道を、３つ挙げておきます。

形式手法の全体像を知りたい方 は、次の記事へ。Isabelle 以外の言語やツールが、それぞれ何を担っているのかを地図として整理しています。

• Rocq（旧Coq）とLean 4だけでは足りない領域がある

他の定理証明の言語と比べたい方 は、次の記事へ。

• Rocq（旧名 Coq）とは何か ── 証明からプログラムを取り出す仕組み
   
• Lean 4 とは何か ── AI が数学オリンピックに挑む舞台裏

本記事で触れた Isar という書き方に関心を持たれた方 は、近く公開する次の記事をお待ちください。

• 『コードなのに、数学の証明文として読める ── 宣言的スタイルという書き方（Mizar・Isabelle・Lean 4）』

関連記事

• Rocq（旧Coq）とLean 4だけでは足りない領域がある ── 形式手法の地図の上で、他の言語が何を担っているのか
   
• Rocq（旧名 Coq）とは何か
   
• Lean 4 とは何か
   
• Cubical Agda とは何か
   
• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界
   
• if 文もSQLも、実は別々の「論理」だった ── 21の論理体系を５人で議論する対話篇
   
• 論理はひとつではない
   
• Python の型ヒントの限界を超える「篩型」入門 ── 型に条件を書くという発想
   
• 論理プログラミングは終わらなかった ── 第五世代コンピュータから LLM・AI Agent へ
   
• F* とは何か
   
• λProlog とは何か

出典

• Isabelle 公式サイト
• Lawrence C. Paulson, "Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine"（Amazon Science Blog、2026年4月17日。日本語訳は AWS ブログ、2026年7月30日） ── AWS による NIE の検証と、Isabelle を選んだ理由
• Archive of Formal Proofs
• Lawrence C. Paulson, "Isabelle: The Next 700 Theorem Provers"（P. Odifreddi 編 Logic and Computer Science、Academic Press、361〜386頁、1990年） ── Isabelle が生まれた動機と歴史
• Lawrence C. Paulson, "The Foundation of a Generic Theorem Prover"（Journal of Automated Reasoning 第5巻第3号、363〜397頁、1989年） ── Pure の設計
• Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser ほか, "seL4: Formal Verification of an Operating-System Kernel"（Communications of the ACM 第53巻第6号、107〜115頁、2010年。原論文は SOSP 2009、207〜220頁） ── 検証の規模と労力
• "What the Proofs Assume"（seL4 公式） ── 証明が仮定していること
• Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel, "From LCF to Isabelle/HOL"（Formal Aspects of Computing 第31巻、2019年） ── LCF からの系譜
• Mark Adams, "The Common HOL Platform"（PxTP 2015、EPTCS 第186巻、42〜56頁） ── HOL 系の比較と、Isabelle/HOL だけが構造的に異なるという指摘
• Lawrence C. Paulson, "Formalising Mathematics in Simple Type Theory"（Reflections on the Foundations of Mathematics、Synthese Library 第407巻、Springer、437〜453頁、2019年） ── HOL Light から Isabelle/HOL への翻訳経験
• Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson, "Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL"（Experimental Mathematics 第31巻第2号、401〜412頁、2022年） ── 単純型理論と古典論理が自動化を可能にするという指摘
• "Sledgehammer: some history, some tips"（Paulson のブログ） ── 依存型と自動化の関係についてのポールソン自身の見解
• Albert Q. Jiang, Sean Welleck, Jin Peng Zhou ほか, "Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs"（第11回 International Conference on Learning Representations、ICLR 2023） ── LLM と Isabelle の組み合わせ
• Tobias Nipkow, Gerwin Klein, "Concrete Semantics with Isabelle/HOL"（Springer、2014年。） ── 最初の一冊として