【連載２回目】コードなのに、そのまま数学の証明文として読める ── AIが証明を書く時代に注目すべきMizar・Isabelle・Lean 4 の宣言的スタイルの記法

はじめに

本記事は、全２回の連載記事の後編（２本目）です。

前回の記事は、こちらです。

• 【連載初回】コードなのに、そのまま数学の証明文として読める ── AIが証明を書く時代に注目すべきMizar・Isabelle・Lean 4 の宣言的スタイルの記法

前回は、定理証明支援系が持つ２つの証明の書き方のうち、タクティクスタイルを扱いました。

簡単に振り返ります。

定理証明支援系とは、数学の定理や、プログラムの正しさを、コンピュータに検査させる仕組みのことです。

証明を書くための専用の言語と、それを読み取って検査する処理系が、一組になっています。

Isabelle、Lean 4、Rocq（旧名 Coq）、Agda、Mizar などが、そう呼ばれるものです。

その証明の書き方には、２通りありました。

一つは、処理系と対話しながら、一手ずつ進めていく書き方です。

これを、タクティクスタイル（tactic style）、あるいは手続き的スタイル（procedural style）といいます。

「ここで場合分けせよ」「これを簡単にせよ」という短い指示を打ち込むと、処理系が「では、次はこれを証明してください」と応答します。

それを見て、次の指示を考える。

Jupyter Notebook でセルを実行し、出力を見ながら次のセルを書くのに似た作業です。

この書き方には、証明の道筋が分かっていなくても試しながら進められるという大きな利点があります。

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

書き上がったコードには、処理系からの応答が残りません。

指示だけが並んだファイルからは、何を証明しようとしていたのかが読み取れないのです。

もう一つが、論証の筋道を最初から文章として書き切る書き方です。

これを、宣言的スタイル（declarative style）といいます。

初回では、その入口までをご紹介しました。

本記事は、その続きです。

想定読者

• 連載の初回を読まれた方
• Python は書けるが、定理証明支援系は学んだことがないという方
• 「コードなのに、そのまま数学の証明文として読める」という話に関心のある方
• AIが証明を書く時代に、人間が何を読み、何を判断すべきかを考えたい方

論理学や関数型プログラミングの予備知識は、仮定しません。

数学の予備知識も、仮定しません。

専門用語は、登場するたびに日常の言葉で説明します。

初回を読んでいない方のために、必要な内容はこの記事の中でも改めて説明します。

この記事を読む価値

1. 「宣言的」という言葉が、３つの違うものを指していることを説明できるようになる。SQL や React で使われる意味との違いが分かる
    
2. assume、have、thus といった語が、それぞれ論証のどの働きを担っているのかが分かる
    
3. 同じ定理を、６つの言語で書いたコードを並べて読める。Mizar、Isabelle、Lean 4、Agda、HOL Light、Rocq
    
4. 宣言的スタイルが読みやすい理由が、1934年の自然演繹の設計にさかのぼる**ことが分かる
    
5. 30年で10種類以上の実装が作られながら、Wiedijk が2012年に「広く使われている」と評したのは一つだけという事実と、その理由を考える材料が得られる
    
6. 「読みやすい」とは誰にとってか。同じ冗長性が、読み手によって長所にも短所にもなることを知る
    
7. LLM が証明を書く時代に、この書き方が持つ意味について、複数の研究の主張を比べられる

TL;DR

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

• 「宣言的」という言葉は、少なくとも３つの違うものを指している。 SQL や React が宣言するのは「何が欲しいか」、Dafny や TLA+ が宣言するのは「満たすべき性質」、**Mizar や Isabelle の Isar が宣言するのは「論証の構造そのもの」**である
   
• 宣言的スタイルとは、assume（仮定する）、have（〜が成り立つ）、thus（よって）といった語を使い、証明を文章として書く方式である。処理系を動かさなくても、読めば筋道が分かる
   
• 実用的な定理証明言語として、この方式を早期に実装した代表例が Mizar（1973年、ポーランド）である
   
• その読みやすさは、偶然ではない。 1934年にヤシコフスキが設計した自然演繹の形式、すなわち仮定を箱で囲み、その帰結を箱の中に保つという形式を、そのまま言語の構文にしている
   
• 語彙は、処理系が違ってもほぼ共通している。 assume、have、thus、consider、take。Wiedijk は「ほとんどの宣言的なシステムは、本質的に同じ証明言語を持つ」と述べている
   
• Agda は、見た目が似ていても別の系統である。 Mizar や Isabelle が「証明の文書」を書くのに対し、Agda は「証明そのもの」をプログラムの式として書く
   
• 30年にわたって、10種類以上の実装が作られてきた。 HOL、HOL Light、Coq、Isabelle、そして2026年には Lean 4 へも移植された
   
• しかし、広く使われているのは Isabelle の Isar だけである。 miz3 の作者である Wiedijk 自身が、そう書いている
   
• 欠点もある。宣言的スタイルの証明は、タクティクの約２倍の長さになる。 そして、読みやすいと分かっていても、書き手はタクティクへ流れる
   
• 「読みやすい」が誰にとってかで、評価が逆転する。 冗長性は、証明を検査する処理系にとっては長所であり、証明を学習する言語モデルにとっては障害になりうる
   
• 証明の骨格だけを書くなら、極端に短く書ける。 ラグランジュの定理という、群論の基本的な定理の場合、完全な証明が183行に対し、骨格だけなら23行である
   
• そして、1997年には既に「証明の骨格を書き、隙間を自動で埋める」という設計思想が、人間のために提案されていた。 2020年代の LLM による証明生成は、それとよく似た構造を採っている

---

本記事の主題

本記事は、この２つ目の書き方、宣言的スタイルを扱う記事の連載２回目です。

タクティクスタイルで書かれた証明の可読性が低いことは、定理証明支援系を開発した人たち自身が、早くから指摘してきたことです。

その言葉を２つ、紹介します。

１つ目は、Isabelle という定理証明支援系を作った本人の言葉です。

However, existing theorem provers are unsuitable for mathematics. Their formal proofs are unreadable.

筆者による日本語訳:

しかし、既存の定理証明系は数学には不向きである。その形式的な証明は読めない。

出典:Lawrence C. Paulson（ケンブリッジ大学 計算機研究所）, ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician, 2017年〜

書いたのは、ローレンス・ポールソンです。
1986年に Isabelle を公開した人物であり、この文章は、彼自身が主宰する研究計画の説明文の一節です。

ここで「読めない」と言われているのは、タクティクスタイルで書かれた証明のことです。

証明を検査するソフトウェアを作った当人が、そのソフトウェアで書かれた証明は読めないと述べています。

２つ目は、Rocq に宣言的スタイルを導入した研究者の言葉です。

Think of a person reading somebody else's formal proof, or even one of his/her own proof a couple of months after having written it.

筆者による日本語訳:

他人の形式的な証明を読む人、あるいは数か月前に自分で書いた証明を読む人のことを考えてみてほしい。

出典:Pierre Corbineau, "A Declarative Language for the Coq Proof Assistant", TYPES 2007, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年

ここで想定されているのも、タクティクスタイルで書かれた証明です。

この研究者は、その読みにくさを解決するために、Rocq へ宣言的スタイルを導入しました。

プログラムのコードと、同じ問題です。

数か月経てば、書いた本人でも読めなくなる。

本記事は、この問題への一つの答えを扱います。

この記事で扱うこと

本記事では、次のことを扱います。

• 「宣言的」という言葉 が、３つの異なるもの を指していること
   
• assume、have、thus といった語が、それぞれ何を担っているのか
   
• 同じ定理を、６つの言語で書いたコードの比較
   
• この書き方が読みやすい理由が、1934年にさかのぼること
   
• 30年にわたって10種類以上の実装が作られながら、Wiedijk が2012年の論文で「広く使われている」と評したのは Isabelle の Isar だけだという事実
•  
• 大規模言語モデル（LLM）が証明を書く時代に、この書き方が持つ意味

なお、本記事に登場するコードは、すべて論文や公開された資料から引用したものです。
筆者の環境では各言語の処理系を動かせないため、**実機での検証はしていません。

** 出典は、すべてリンクつきで明示します。

---

対話篇:そもそも「処理系」とは何か

本題に入る前に、言葉の整理をします。

この分野には、紛らわしい言葉がいくつもあります。
特に、**「言語」と「処理系」の区別*+* は、最初につまずきやすい箇所です。

この節だけ、対話の形で進めます。

登場するのは、タロウくん（Python は書けるが、この分野は初めて）と、専任講師（数学の複数の分野と技術領域に通じている）です。

---

タロウくん：
先生、質問があります。

Isabelle とか Rocq とか Lean 4 って、Python や Ruby、JavaScript と同じような、プログラミング言語の名前ですよね?

専任講師：
いい質問です。

その理解は、半分正しくて、半分ずれています。

タロウくん:半分、ですか。

専任講師:ええ。まず、Python の話から始めましょう。Python という言葉は、実は２つのものを指しています。

タロウくん:２つ、ですか?

専任講師：
一つは、言語そのもの。

文法の決まりと、それぞれの書き方が何を意味するかという取り決めです。

もう一つは、それを実際に動かすソフトウェア。
こちらは CPython という名前が付いています。

タロウくん：
CPython。
聞いたことはあります。

専任講師：
普段は区別しませんよね。

「Python で書いた」と言えば通じます。

なぜなら、言語と、それを動かすソフトウェアが、ほぼ一対一で対応しているからです。

タロウくん：
確かに、区別する必要を感じたことはないです。

専任講師：
ところが、定理証明支援系 では、そうはいきません。

タロウくん：
と言いますと。

専任講師：
Isabelle を例に取ります。

ここには、３つの層 があります。

まず、Isabelle というソフトウェアそのもの。
証明を読み込んで、正しいかどうかを検査するプログラムです。

タロウくん：
CPython に当たるもの ですね？

専任講師：
そうです。

次に、Isabelle/HOL。

これは、その上に載せる論理の体系です。
何を証明できるのか、どういう推論を認めるのかを決めます。

タロウくん：
・・・それは、Python にはないもの ですね。

専任講師：
ないいですね。
Python では、「どういう推論を認めるか」を選ぶ場面がありませんから。

そして３つ目が、Isar。
その中で、証明を書くための言語です。

タロウくん：
待ってください。

Isabelle と Isar は、別のもの なんですか？

専任講師：
別のものですが、切り離せません。

Isar は Isabelle の一部 です。

Isabelle というソフトウェア の中で、証明を書くときに使う言語の名前 が Isar なのです。

タロウくん：
じゃあ、Isar は Isabelle を拡張する言語ですか？

別の人が後から作って足したような。

専任講師：
そこが、まさに半分正しくて半分ずれている箇所です。

タロウくん：
半分は正しいんですね？

専任講師：
はい。

そういう関係になっている言語も、実際にあります。

HOL Light という定理証明支援系には、miz3 という言語が後から載せられました。

約2,000行のプログラムを追加することで、宣言的スタイルで書けるようになったのです。

これは、まさに「拡張」です。

Rocq も同じです。
C-zar という言語が、後から追加されました。

タロウくん：
じゃあ、Isar も同じでは？

専任講師：
Isar は違います。

Isar は、Isabelle に最初から組み込まれた、標準の書き方 です。

後から足した拡張ではありません。

タロウくん：
同じように見えて、成り立ちが違う んですね。

専任講師：
そのとおりです。

表にすると、こうなります。

処理系	宣言的スタイルの言語	拡張か、組み込みか
Isabelle	Isar	組み込み。Isabelle の標準の書き方
Lean 4	独立した名前は無い	組み込み。have などが言語の一部
HOL Light	miz3	拡張。後から載せた約2,000行
Rocq	C-zar	拡張。後から追加された
Agda	独立した名前は無い	ライブラリで提供される
Mizar	区別しない	処理系と言語が一体。Python に近い

タロウくん：
あ、Mizar だけ、Python と同じなんですね。

専任講師：
よく気づきましたね。

Mizar は、処理系の名前でもあり、言語の名前でもあります。

名前が一つしかありません。

タロウくん：
ところで先生、さっきから 「処理系」 という言葉を使っていますが。

専任講師：
説明していませんでしたね。

処理系 とは、書かれたものを読み取って、実際に動かすソフトウェアのことです。

Python なら、書いたプログラムを実行するソフトウェア。
定理証明支援系なら、書かれた証明を検査するソフトウェアです。

タロウくん：
じゃあ、Isabelle も Rocq も Lean 4 も、ソフトウェアの名前 ということですか。

専任講師：
そのとおりです。

これらは 処理系の名前、つまりソフトウェアの名前 です。

そして、それぞれの処理系の中で、証明を書くための言語があります。

Isabelle における Isar が、その 例 です。

タロウくん：
整理できました。

この記事で扱うのは、３つ目の層、つまり「証明を書くための言語」ということですね。

専任講師：
そのとおりです。

論理の体系そのもの ではなく、証明をどう書き表すか という話です。

第１部 ── 「宣言的」という言葉は、３つの違うものを指している

第１部では、「宣言的」という言葉の意味 を 整理します。

まずはSQL から

次のコードを見てください。

SELECT name FROM users WHERE age > 20

「users というテーブルから、age が20より大きい行の name を取り出す」という意味です。

ここで、書かれていないものに注目してください。

• テーブルを先頭から順に見ていけ、とは書いていません
• 条件に合う行を集めよ、とも書いていません
• どの索引を使え、とも書いていません

書いてあるのは、「何が欲しいか」だけ です。

どうやって取ってくるか は、データベースが決めます。

同じことを Python で書くと、こうなります。

result = []
for user in users:
    if user.age > 20:
        result.append(user.name)

繰り返しの 手順 が、はっきりと書かれています。

SQL では、その手順が消えています。

「宣言的」という言葉 に、聞き覚えのある方もおられるかもしれません。

React で画面を書くとき、「この状態のとき、画面はこう見える」と書きます。
どう書き換えるかは書きません。

Terraform でインフラを書くとき、「サーバは３台であってほしい」と書きます。
いま何台あって、何台足すのかは書きません。

Kubernetes のマニフェストも同じです。「この状態を保ってほしい」と書きます。

これらに共通するのは、「どうやるか」ではなく「どうあってほしいか」を書くという点 です。
SQL も同じでした。

本記事で扱う 宣言的スタイル も、この系譜に連なります。

ただし、宣言している対象が違います。 そこが、本記事の中心にある論点です。

なお、SQL は定理証明支援系ではありません。
証明を検査する機能を持ちません。

それでも SQL から始めたのは、「手順を書かない」という感覚 を、SQLをご存知の読者の皆様はすでにお持ちのはずだからです。

命令的とは何か

「宣言的」の対になる言葉は、「命令的」 です。

命令的 とは、どうやるかをステップごとにコードに書き込むこと です。

numbers = [1, 2, 3, 4, 5]
total = 0
for n in numbers:
    total = total + n
print(total)

このコードには、次の手順 が記述されています。

1. 合計を入れる変数を用意し、0 を入れる
2. 配列の要素を、先頭から一つずつ取り出す
3. 取り出すたびに、変数の中身に足す
4. 全部終わったら、変数の中身を表示する

つまり、「どうやるか」が、すべて書かれている のです。

Web の領域における「宣言的」

JavaScript の配列メソッド

命令的な書き方:

const numbers = [1, 2, 3, 4, 5];
const doubled = [];
for (let i = 0; i < numbers.length; i++) {
  doubled.push(numbers[i] * 2);
}

宣言的な書き方:

const numbers = [1, 2, 3, 4, 5];
const doubled = numbers.map(n => n * 2);

違いは、繰り返しの手順を書くかどうか です。

map を使う書き方には、添字の変数も、繰り返しの条件も、配列への追加も現れません。

コードに書かれているのは、「各要素を２倍したものが欲しい」ということだけです。

Python のリスト内包表記

同じことは Python でも書けます。

命令的:

numbers = [1, 2, 3, 4, 5]
doubled = []
for n in numbers:
    doubled.append(n * 2)

宣言的:

numbers = [1, 2, 3, 4, 5]
doubled = [n * 2 for n in numbers]

React の画面

命令的な書き方
（素の JavaScript で画面を操作する場合）:

const button = document.createElement("button");
button.textContent = "押してください";
button.className = "primary";
document.body.appendChild(button);

// 状態が変わったら、自分で書き換える
button.textContent = "送信中";
button.disabled = true;

要素を作り、文字を入れ、画面に追加し、状態が変わったら自分で書き換える。

*すべての手順 が書かれています。

宣言的な書き方（React）:

function SubmitButton({ isSubmitting }) {
  return (
    <button className="primary" disabled={isSubmitting}>
      {isSubmitting ? "送信中" : "押してください"}
    </button>
  );
}

React では、「この状態のとき、画面はこう見える」とだけ 書きます。

どう書き換えるかは書きません。

状態が変わったとき、画面をどう更新するかは React が決めます。

インフラの構成

命令的な書き方（シェルスクリプト）:

aws ec2 run-instances --image-id ami-xxxxx --count 3

このコマンドは「３台作れ」という命令です。

もし既に２台あったら、１台だけ足したい。
その判断は、自分で書く必要があります。

宣言的な書き方（Terraform）:

resource "aws_instance" "web" {
  count         = 3
  ami           = "ami-xxxxx"
  instance_type = "t3.micro"
}

Terraform では、「３台であってほしい」とだけ 書きます。

いま何台あるかを調べ、足すのか減らすのかを判断するのは、Terraform の仕事です。

Kubernetes のマニフェスト も同じです。

「この状態を保ってほしい」 と書き、その状態へ近づける作業は Kubernetes が行います 。

ここまでに共通しているもの

SQL も、JavaScript の map も、React も、Terraform も、共通しているのは次の一点 です。

「どうやるか」ではなく、「どうあってほしいか」を書く。

領域	書くこと	書かないこと
SQL	欲しいデータの条件	テーブルを見ていく手順
JavaScript の map	各要素をどう変えるか	繰り返しの手順
React	この状態のとき、画面はこう見える	画面をどう書き換えるか
Terraform	あってほしい構成	その構成にする手順

この整理は、複数の技術解説文書で、共通して述べられていることです。

• Declarative vs. Imperative Programming（Toptal）
   
• Declarative Vs. Imperative Programming: 4 Key Differences（Octopus Deploy）

関数型言語における「宣言的」

次は、関数型プログラミング の話です。

関数型プログラミング言語 と呼ばれる一群の言語があります。
Haskell、OCaml、F# などです。

これらの言語では、プログラム全体が宣言的に 書かれます。

Haskell の例:

double :: [Int] -> [Int]
double xs = map (* 2) xs

JavaScript の map と、ほとんど同じに見えます。

実は、順序が逆です。

JavaScript や Python の map は、関数型言語から借りてきた考え方です。

皆様が日々お使いなられているかもしれない上記の書き方は、もともとこの系譜から来ています。

関数型言語が特徴的なのは、次の点です。

変数の値が、途中で変わりません。

先ほどの Python のコードを思い出してください。

total = 0
for n in numbers:
    total = total + n

ここでは、total という 変数の中身を、繰り返し書き換えて います。

関数型言語では、こうしたことをよしとしません。
新しい値を作って返すだけです。

そのため、プログラムは「手順の列」ではなく、「値と値の関係の記述」 になります。

-- 「n の階乗とは、1 から n までを掛け合わせたもの」という記述
factorial n = product [1..n]

つまり、「どう計算するか」ではなく、「何であるか」 をコードに記述していくのです。

関数型言語 の 宣言的な書き方 も、SQL や React と同じ層に属します。

何を計算するか を 宣言しているからです。

満たすべき性質を宣言する言語

もう一つ、「宣言型」についての別の定義 があります。

「このプログラムは、この条件を満たす 」と書く言語です。

**Dafny++ という言語のコードは、次のように書き表します。

method Abs(x: int) returns (y: int)
  ensures y >= 0
{
  ...
}

ensures y >= 0 の部分が、「この関数が返す 値は、必ず $0$ 以上である 」という 宣言 です。

ここで宣言されているのは、計算の手順ではありません。

宣言されているのは、満たすべき条件です。

そして、その条件が本当に満たされるかどうかを、Dafny が検査する のです。

同じ発想の言語が、他にもあります。

• TLA+ ── 並行して動く複数の処理が満たすべき性質を書き、その性質が保たれるかを検査します
   
• F* ── 型の中に条件を書き込める言語です。「この関数は、0より大きい整数を受け取り、0より大きい整数を返す」といったことを、型として表現できます

２つ目のF*については、筆者はすでに記事を書いています。

• F* とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」
   
• Python の型ヒントの限界を超える「篩型」入門

本記事でも、必要な範囲で改めて説明します。

定理証明支援系における「宣言的」

そして、本記事の主題です。

Isabelle や Mizar で 「宣言的スタイル」 と呼ばれるものは、ここまでとは違うものを宣言しています。

宣言 しているのは、論証の構造そのもの です。

assume "P"
have "Q" by ...
thus "R" by ...

「 $P$ を仮定する。 $Q$ が成り立つ。よって $R$ である。」

ここで書かれているのは、計算でも、画面の状態でも、インフラの構成でもありません。

なぜその結論が導かれるのか、という論証の筋道 です。

宣言の対象：３つの階層

以上をまとめます。

「宣言的」という言葉は、少なくとも３つの違うものを指しています。

階層	宣言している対象	例
階層１	何が欲しいか／何を計算するか	SQL、JavaScript の map、Python のリスト内包表記、React、Terraform、Kubernetes、Haskell
階層２	満たすべき性質	Dafny、TLA+、F*
階層３	論証の構造そのもの	Mizar、Isabelle の Isar

階層１ は、多くのプログラマの皆様が、日常的に書いているものです。

階層２ は、「このプログラムは、この条件を満たす」と書くものです。

そして階層３が、本記事の主題です。

同じ「宣言的」という言葉が使われていますが、宣言している対象がまったく異なります。

以上の階層を区別する視座を持っていないと、この後の話が混乱します。

この視座さえ持っていれば、あとは実際のコードを読んでいくだけです。

第２部 ── 論証のための語彙

第２部では、宣言的スタイル で使う *語彙 を、ひとつずつ見ていきます。

その前に、対になる書き方を説明します。

タクティクとは何か

多くの 定理証明支援系 では、証明 を 「指示の列」として 書きます。

この指示を、タクティク と呼びます。

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

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

• 「ここで場合分けせよ」
   
• 「これを簡単にせよ」
   
• 「この定理を使え」

タクティク を使う書き方は、Isabelle に限りません。

Rocq でも、Lean 4 でも、HOL Light でも採用されています。

タクティク のメリットは、証明の中身を一字一句、自分で最初から最後まで一気呵成にまとめて記述する必要がない、ということです。

定理証明支援処理系にプログラマがタクティクで指示を与えると、処理系が「次に何を証明すべきか」を計算して表示してくれるからです。

プログラマは、最初から証明の道筋の全体像を頭の中で描き切れていなくとも、処理系と対話しながら、証明を一歩一歩、試行錯誤しながら模索していける のです

タクティクの難点

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

本連載の初回の記事で、複数の代表的な定理証明支援系言語について、タクティク のコードを並べました。

もう一度、Rocq のタクティク記法のコードを見てください。

Lemma double_div2: forall n, div2 (double n) = n.
intro n.
induction n.
reflexivity.
unfold double in *|-*.
simpl.
rewrite <- plus_n_Sm.
rewrite IHn.
reflexivity.
Qed.

（出典）
Pierre Corbineau（ラドバウド大学ナイメーヘン）, "A Declarative Language for the Coq Proof Assistant", Miculan・Scagnetto・Honsell 編 Types for Proofs and Programs（TYPES 2007）, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年, 72頁

それぞれの命令の意味は、次のとおりです。

intro n（変数を導入せよ）
induction n（n について帰納法を使え）
reflexivity（両辺が同じであることを示せ）
unfold double（double の定義を展開せよ）
simpl（簡単にせよ）
rewrite（書き換えよ）。

一つ一つの意味が分かっても、この９行が全体として何を示しているのかは、人間の目で見て、容易に読み取ることはできません。

まさに、Jupyter Notebook のセルを一つずつ追うのと同じ状況です。

この難点は、開発者たち自身が認めている

Corbineau は、論文の冒頭でこう書いています。

Think of a person reading somebody else's formal proof, or even one of his/her own proof a couple of months after having written it.

Similarly to what happens with source code, this person will have a lot of trouble understanding what is going on with the proof unless he/she has a very good memory or the proof is thoroughly documented.

（筆者による日本語訳）

他人の形式的な証明を読む人、あるいは数か月前に自分で書いた証明を読む人のことを考えてみてほしい。

ソースコードで起きるのと同じように、その人は、非常に良い記憶力を持っているか、その証明が徹底的に文書化されていないかぎり、証明で何が起きているのかを理解するのに大いに苦労するだろう。

（出典）
同上、69〜70頁

続けて、彼はこう述べます。

This illustrates a major inconvenience which still affects many popular proof languages used nowadays: they lack readability.

（筆者による日本語訳）

これは、今日使われている多くの人気ある証明言語に、いまなお影響している大きな不便を示している。

それらは読みやすさを欠いている。

（出典）
同上、70頁

同じ問題を、Isabelle の開発者たちも指摘しています。

The problem with the traditional approach is that anybody looking at a machine-checked proof has no idea of what has been proved at any point.

It is like playing blindfold chess.

（筆者による日本語訳）

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

目隠しでチェスをするようなものだ。

（出典）
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel, "From LCF to Isabelle/HOL", Formal Aspects of Computing 第31巻, 2019年

「目隠しでチェスをするようなもの」。

３人の著者のうち、ポールソンは Isabelle の作者、ニプコウは主要な開発者、ヴェンツェルは Isar の設計者です。

では、宣言的スタイルではどう書くのか

先ほどと同じ定理を、宣言的スタイル で書いたものが、こちらです。

Lemma double_div2: forall n, div2 (double n) = n.
proof.
  let n:nat.
  per induction on n.
  suppose it is 0.
    reconsider thesis as (0=0).
    thus thesis.
  suppose it is (S m) and Hrec:thesis for m.
    have (div2 (double (S m))
          = div2 (S (S (double m)))).
    ~= (S (div2 (double m))).
    thus ~= (S m) by Hrec.
  end induction.
end proof.
Qed.

（出典）
同上、72頁。

これは、C-zar という言語 で書かれています。

Rocq に 後から追加 された、宣言的スタイルのための言語 です。

読んでみてください。

let n:nat（n を自然数とする）
per induction on n（ $n$ について帰納法で進める）
suppose it is 0（それが $0$ の場合を考える）
thus thesis（よって、示すべきことが示された）
suppose it is (S m)（それが $m$ の次の数である場合）
have ...（〜が成り立つ）、thus ~= (S m)（よって、$m$ の次の数に等しい）。

コードを見て、どんな手順で、どんな論証（証明）が展開されているのか、人が眼で見て読み取ることができます。

この点について、当のCorbineau 自身がこう書いています。

The proof consists of a simple induction on the natural number n.

The first case is done by conversion (computation) to 0 = 0 and the second case by computation and by rewriting the induction hypothesis.

Of course, you could have guessed that by simply reading the declarative proof.

（筆者による日本語訳）

**証明は、自然数 n についての単純な帰納法から成る。

第一の場合は 0 = 0 への変換（計算）によって行われ、第二の場合は計算と帰納法の仮定の書き換えによって行われる。

もちろん、宣言的な証明をただ読むだけで、そのことは推測できたであろう。**

（出典）
同上、72〜73頁

「ただ読むだけで、そのことは推測できたであろう」。

これが、宣言的スタイルが目指したもの です。

宣言的スタイルの語彙

では、その語彙を一つずつ見ていきます。

ここでは Isabelle の Isar を例に取りますが、後の部で見るとおり、他の言語でもほぼ同じ語 が使われます。

assume ── 仮定する

「〜であるとする」と、前提を置きます。

assume "P"

数学の証明で「 $P$ であると仮定する」と書くのと、同じことです。

この語を書いた時点から、その仮定が使えるようになります。

have ── 〜が成り立つ

途中で示したい主張を書きます。

have "Q" by ...

by の後ろには、その主張をどう示すかを書きます。

定理の名前を並べたり、簡約を指示したりします。

重要なのは、「 $Q$ が成り立つ」という主張そのものが、コードに書かれていることです。

タクティク なら、この主張は画面に表示されるだけで、コードには残りません。

show ── 示す

いま証明すべき目標を、実際に示します。

show "R" by ...

have との違いは、これが目標そのものだという点です。

have は途中の主張、show は最終的に示すべきものです。

thus ── よって

「直前に示したことを使って、目標を示す」という意味です。

thus "R" by ...

実は、これは省略形です。

Isar では、次の等式が成り立ちます。

from this show   ≡ then show   ≡ thus
from this have   ≡ then have   ≡ hence
from this        ≡ then

出典:カールスルーエ工科大学の Isabelle の講義資料

つまり、thus は then show の省略形であり、then show は from this show の省略形です。

this とは、直前に示した事実を指します。

hence ── ゆえに

thus と同じ構造ですが、こちらは have の省略形です。

「直前に示したことを使って、途中の主張を示す」という意味になります。

obtain ── 存在するものを取り出す

「〜であるような $x$ が存在する」ことが分かっているとき、その $x$ を取り出して名前を付けます。

obtain x where "P x" by ...

数学の証明で「そのような $x$ を一つ取る」と書くのと、同じことです。

next ── 次の場合へ

場合分けをしているとき、次の場合に移ります。

also と finally ── 計算をつなぐ

等式や不等式を、順につないでいく書き方です。

これについては、第５部で詳しく扱います。

Isar には、事実を渡す構文が11種類ある

ここまでに挙げたのは、ごく一部です。

Isabelle の Isar には、「すでに示した事実を、次の段階へ渡す」ための構文が11種類あります。

using / use-in / from / with / then / thus / hence / also / moreover / ultimately / finally

（出典）
"A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL", 2025年

さらに、この論文は次のようにも述べています。

• 証明の文脈を開く仕組みが４種類（subgoal、proof、{}、goal_cases）
• タクティクを適用する方法が５種類（apply、by、proof、qed、タクティクの結合子）
• 事実や項を参照する糖衣構文が６種類（this、that、assms、prems、?thesis、?case）

この数の多さが、後の部で論点になります。

先ほど見たとおり、thus は then show の省略形であり、hence は then have の省略形でした。

11種類のうち、いくつかは同じことの別の書き方です。

**この重なりを「便利さ」と見るか、「冗長さ」と見るか。 **

そこで評価が分かれます。

この論点は、第４部で取り上げます。

第３部 ── なぜ宣言的スタイルは読みやすいのか

ここまで、宣言的スタイルの語彙 を見てきました。

では、なぜこの書き方は 読みやすい のでしょうか。

その答えは、1934年にさかのぼります。

この第３部では、宣言的スタイルへ至る道筋を、順を追って説明 します。

論理学の予備知識は仮定しません。

そもそも「演繹」とは何か

まず、この言葉の解説から始めます。

入口その１: 三段論法

学校で習った三段論法を思い出してください。

人間はみな死ぬ。
ソクラテスは人間である。
ゆえに、ソクラテスは死ぬ。

上の２つを認めるなら、下の一つも認めざるを得ません。

これが演繹（えんえき）です。

演繹の要点は、次の一点にあります。

前提が正しければ、結論も必ず正しい。

推測でも、経験則でもありません。

前提を認めた時点で、結論は決まってしまいます。

ここが、他の推論との違いです。

入口その２: Python の条件分岐

実は、プログラムを書くとき、私たちは日常的にこの演繹を実行しています。

if age > 20:
    print("成人です")

このコードを書くとき、頭の中ではこう考えています。

age が20より大きいならば、この行が実行される。
いま age は25である。
ゆえに、この行は実行される。

形は、先ほどの 三段論法 とまったく同じです。

• 「AならばB」という規則がある
• Aが成り立っている
• ゆえにBが成り立つ

この推論の形には名前があります。

モーダスポネンス（ modus ponens、肯定式）と呼ばれ、論理学で最も基本的な推論規則の一つ です。

つまり、演繹は特別な学問の話ではありません。

プログラマをが毎日実践していること です。

この論点については、筆者が以前に公開した記事でも取り上げています。

• if 文もSQLも、実は別々の「論理」だった

本記事でも、必要な範囲で改めて説明します。

では、それをどう検査させるのか

問題は、ここからです。

この 演繹 を、Isabelle や Lean 4、Rocq といった 定理証明支援系 に 検査させる には、どうすればよいのでしょうか。

「どういう推論を認めるか」 を、あらかじめ厳密に決めておく必要があります。

その決まりの体系を、証明体系と呼びます。

そして、証明体系にはいくつかの流儀 があります。

なぜ「自然」演繹なのか

1934年、ゲルハルト・ゲンツェンという数学者 が、論文の冒頭でこう書きました。

My starting point was this: The formalization of logical deduction, especially as it has been developed by Frege, Russell, and Hilbert, is rather far removed from the forms of deduction used in practice in mathematical proofs.

Considerable formal advantages are achieved in return.

In contrast, I intended first to set up a formal system which comes as close as possible to actual reasoning.

The result was a 'calculus of natural deduction'.

（筆者による日本語訳）

私の出発点はこうであった。

論理的な演繹の形式化、とりわけフレーゲ、ラッセル、ヒルベルトによって発展させられたそれは、数学の証明において実際に使われる演繹の形から、かなりかけ離れている。

その代わりに、相当な形式上の利点が得られてはいる。

これに対して私は、まず、実際の推論にできるだけ近い形式体系を作ろうとした。

その結果が「自然演繹の計算」である。

（出典）
Gerhard Gentzen, "Untersuchungen über das logische Schließen", Mathematische Zeitschrift 第39巻, 176〜210頁および405〜431頁, 1934年。

英訳は "Investigations into Logical Deduction", American Philosophical Quarterly 第1巻, 288〜306頁（1964年）および第2巻, 204〜218頁（1965年）。

上記の引用は英訳からのものであり、筆者の訳は重訳にあたります。

引用元:Stanford Encyclopedia of Philosophy「自然演繹」

「自然」の意味が、ここにあります。

数学者が実際にやっている推論に近い から、「自然」 なのです。

何と比べて「自然」なのか

ゲンツェンが「かけ離れている」と述べた相手は、ヒルベルト流と呼ばれる体系です。

Internet Encyclopedia of Philosophy は、両者の関係をこう整理しています。

The first ND systems were developed independently by Gerhard Gentzen and Stanisław Jaśkowski and presented in papers published in 1934. Both approaches, although different in many respects, provided the realization of the same basic idea: formally correct systematization of traditional means of proving theorems in mathematics, science and ordinary discourse. It was a reaction to the artificiality of formalization of proofs in axiomatic systems.

筆者による日本語訳:

最初の自然演繹の体系は、ゲルハルト・ゲンツェンとスタニスワフ・ヤシコフスキによって独立に開発され、1934年に発表された論文で提示された。両者の手法は多くの点で異なるが、同じ基本的な考えを実現していた。数学、科学、日常の議論において定理を証明する伝統的な手段を、形式的に正しく体系化することである。それは、公理的体系における証明の形式化の不自然さへの反応であった。

出典:Internet Encyclopedia of Philosophy「Natural Deduction」

記述はさらにつづきます。

Hilbert's proof theory offered high standards of precise formulation of this notion, but formal axiomatic proofs were really different than 'real' proofs offered by mathematicians.

The process of actual deduction in axiomatic systems is usually complicated and needs a lot of invention.

Moreover, real proofs are usually lengthy, hard to decipher and far from informal arguments provided by mathematicians.

（筆者による日本語訳）

**ヒルベルトの証明論は、この概念を厳密に定式化する高い水準を提供した。

しかし、形式的な公理による証明は、数学者が実際に書く証明とは、実際には違っていた。

公理的体系における実際の演繹の過程は、たいてい込み入っており、多くの発想を必要とする。

さらに、本物の証明はたいてい長く、解読しがたく、数学者が与える非形式的な議論からかけ離れている。**

（出典）
同上

両者の違いを表にまとめます。

	ヒルベルト流	自然演繹
公理の数	多い	ほとんど無い
推論規則の数	少ない（モーダスポネンスなど）	多い（論理記号ごとに複数（
証明の見た目	長く、解読しがたい	数学者の議論に近い
証明の進め方	公理から始める	仮定を置いて、その帰結を見る

導入規則と除去規則

自然演繹 では、論理記号ごとに規則 が定められています。

ゲンツェン は、こう考えました。

Gentzen (1934) remarked that the introduction rules were like definitions of the logical operators, and that the elimination rules were consequences of their definitions.

（筆者による日本語訳）

ゲンツェン（1934年）は、導入規則は論理演算子の定義のようなものであり、除去規則はその定義から出てくる帰結である、と述べた。

（出典）
Stanford Encyclopedia of Philosophy「自然演繹」

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

「かつ」という記号 を取り上げます。

「かつ」の導入規則

A が成り立ち、B が成り立つならば、「A かつ B」が成り立つ。

「かつ」の除去規則:

「A かつ B」が成り立つならば、A が成り立つ。

この２つ で、「かつ」という記号の意味 が すべて **定まります。

これは、少し不思議な考え方です。

普通、言葉の意味を説明するときは、別の言葉で言い換えます。

「かつ」とは「両方とも成り立つこと」だ、というように。

しかし 自然演繹 では、そうしません。

「かつ」という記号について、次の２つだけを定めます。

【１つ目】

どうすれば、「かつ」を作ることができる。

$A$ が成り立ち、$B$ も成り立っている。

そのときに限り、

「$A$ かつ $B$」と書いてよい。

これが、導入規則 です。

「かつ」を新しく持ち込むための規則なので、そう呼ばれます。

【２つ目】

「かつ」から何が言えるか。

「$A$ かつ $B$」が成り立っている。

ならば、

$A$ が成り立つと言ってよい
$B$ についても同様です。

これが、除去規則 です。

「かつ」を取り除いて、中身を取り出すための規則 です。

この２つで、話は終わりです。

「かつ」が何を意味するのか を、日本語や他の記号で言い換える必要はありません。

作り方と、使い方。この２つが決まれば、その記号の役割はすべて決まっているからです。

プログラミング で言えば、こう考えると近いかもしれません。

ある関数について、

「どんな引数を渡せば呼べるか」

と

「呼んだら何が返ってくるか」

が分かっていれば、その関数 は 使うことができます。

関数の内部実装コードがどう書かれているのかを知らなくても、困ることはありません。

自然演繹の規則 も、それに似ています。

「かつ」の中身を問わず、出し入れの仕方だけを定めているのです。

ゲンツェン流とヤシコフスキ流

さて、ここからが本題です。

1934年、ゲンツェンとヤシコフスキ は、独立に自然演繹 を作りました。

しかし、証明の書き表し方が違いました。

Internet Encyclopedia of Philosophy は、こう述べています。

In addition to providing suitable rules, one must also decide about the form of a proof.

Two basic approaches due to Gentzen and Jaśkowski are based on using trees as a representation of a proof and on using linear sequences of formulas.

筆者による日本語訳:

**適切な規則を与えることに加えて、証明の形についても決めなければならない。

ゲンツェンとヤシコフスキによる２つの基本的な手法は、証明の表現として木を使うものと、論理式の線形の列を使うものである。**

（出典）
同上

この違いは決定的です。

	ゲンツェン流	ヤシコフスキ流
証明の形	木構造	線形の列
仮定の扱い	木の葉に置き、後で解消する	箱で囲む
入れ子	木の枝分かれ	箱の中に箱
向いていること	証明そのものの性質を研究すること	実際に証明を書くこと

「箱」とは何か

表に出てくる 「箱」 という言葉を、説明します。

紙の上に、四角い枠を描くことです。

その枠の中に書かれたことは、枠の外では使えません。

なぜでしょうか。

枠の一行目に、仮定が書かれているからです。

その仮定を認めた場合にだけ、枠の中の話は成り立ちます。

枠の外には、その仮定がありません。

Python で言えば、if 文の中と外の関係に近いものです。

if x > 0:
    y = 100 / x      # ここでは x > 0 が保証されている
    print(y)
# ここへ出ると、x > 0 はもう保証されない

インデントされた範囲の中でだけ、x > 0 という条件が効いています。

その範囲を抜けると、条件は失われます。

ヤシコフスキの「箱」 は、これと同じ働きをします。

箱の一行目に仮定を書き、その仮定が効く範囲を、枠で囲って示すのです。

そして、「箱の中に箱」とは、if 文の中にさらに if 文があるのと同じことです。

if x > 0:
    if y > 0:
        z = x / y    # ここでは x > 0 と y > 0 の両方が効いている
    # ここでは x > 0 だけが効いている

内側の箱では、外側の仮定と内側の仮定の両方が使えます。

内側を抜ければ、内側の仮定は失われます。

この入れ子の構造が、そのまま証明の構造になっているのです。

では、木構造とは

ゲンツェン流のほうも、説明しておきます。

こちらは、証明を木のような図として描きます。

一番上に仮定が並びます。 木でいえば、葉にあたる部分です。

そこから下へ向かって推論が進み、複数の枝が合流していきます。

そして一番下に、結論が来ます。 木でいえば、根や幹にあたる部分です。

紙の上での見た目が、箱とはまったく違います。

箱のほうは、上から下に視線を流して読むことができる一本の列です。
数学の答案と同じ形です。

木のほうは、平面に広がる図です。
一本の列としては読めません。

そして、この記事で扱う宣言的スタイルは、箱のほうを構文にしたものです。

ヤシコフスキの箱

ヤシコフスキの手法 について、改めてみてみます。

Stanford Encyclopedia of Philosophy は、こう説明しています。

Completely independent from Gentzen, Jaśkowski (1934) described two methods.

Of interest to us in this article is the one found in a lengthy footnote, where he describes a pictorial method that he had announced earlier.

The pictorial method involved the drawing of "boxes" around portions of a proof, to indicate that the enclosed formulas are "considered as following only under a supposition".

（筆者による日本語訳）

ゲンツェンとは完全に独立に、ヤシコフスキ（1934年）は２つの手法を述べた。

本稿で関心があるのは、長い脚注の中に見出されるもので、そこで彼は、以前に予告していた図的な手法を述べている。

その図的な手法は、証明の一部の周りに「箱」を描くことを伴い、囲まれた論理式が「ある仮定の下でのみ従うものとみなされる」ことを示す。

出典:Stanford Encyclopedia of Philosophy「自然演繹」

なお、この手法が「長い脚注」の中で述べられたという点は、記しておく価値があります。

続けて、箱の働きが説明されています。

The fundamental notion of making a supposition (= assumption) and seeing where it leads is indicated in Jaśkowski's by the introduction of a box, the first line of which is the supposition and all the consequences of that assumption are retained inside that box. >

Moreover, further suppositions can be made within the previous box by generating a subordinate box.

（筆者による日本語訳）

仮定を置き、それがどこへ導くかを見るという基本的な考え方が、ヤシコフスキにおいては箱の導入によって示される。

箱の最初の行が仮定であり、その仮定から導かれるすべての帰結が、その箱の内側に保たれる。

さらに、前の箱の内側で、下位の箱を作ることによって、さらなる仮定を置くこともできる。

（出典）
同上

そして、重要な制約があります。

Once a box has been constructed, no formula within it can be used to justify any line of the proof outside of the box.

（筆者による日本語訳）

いったん箱が作られると、その内側のどの論理式も、箱の外側の行を正当化するために使うことはできない。

（出典）
同上

箱の中で示したことは、箱の外では使えません。
仮定の下でしか成り立たないからです。

なお、この手法は後に整理されました。

フレデリック・フィッチ が 1952年 に、より現代的な形にまとめたため、「ヤシコフスキ／フィッチ流」と呼ばれます。

現在の論理学 の入門教科書で 最も多く使われているのは、この形式 です。

箱の構造が、そのまま構文になっている

ここで、第２部で見た 宣言型の語彙 を思い出してください。

ヤシコフスキ流の箱	宣言的スタイルの構文
箱を開き、最初の行に仮定を書く	assume
箱の中で、帰結を導いていく	have
箱を閉じ、結論を外へ出す	thus / show
箱の中に箱を作る	proof ブロックの入れ子
箱の中の式は、外では使えない	仮定と変数の有効範囲

一対一で対応しています。

これは偶然ではありません。

miz3 という言語を作った Freek Wiedijk は、論文の中でこう書いています。

The three most common proof systems for first order predicate logic are natural deduction, sequent calculus and Hilbert-style logic.

Of these three, natural deduction corresponds most closely with everyday mathematical reasoning.

The two main proof systems for natural deduction are Jaśkowski/Fitch- and Gentzen-style deduction. Of these, the first is the easiest to use for actual proofs.

（筆者による日本語訳）

**一階述語論理の最も一般的な証明体系は３つある。

自然演繹、シークエント計算、ヒルベルト流の論理である。

このうち、自然演繹が日常の数学の推論に最も近く対応する。
自然演繹の主な証明体系は２つ、ヤシコフスキ／フィッチ流とゲンツェン流である。

このうち、前者が実際の証明に使うのが最も容易である。**

（出典）
Freek Wiedijk（ラドバウド大学ナイメーヘン）, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年

さらに、こうも述べています。

It turns out that the languages of declarative systems are all close to Jaśkowski/Fitch-style natural deduction.

筆者による日本語訳:

宣言的なシステムの言語は、いずれもヤシコフスキ／フィッチ流の自然演繹に近いことが分かる。

出典:同上

【第３部の結論】

宣言的スタイル が読みやすいのは、偶然ではありません。

1934年に、人間が実際に証明を書くために設計された形式を、そのまま言語の構文にしたから です。

仮定を置き、その帰結を導き、結論を出す。

数学の答案で誰もがやっていること が、90年以上前に形式化され、すでに用意されていたのです。

そして、その形式が、いま定理証明支援系の中で動いています。

歴史の符合

スタニスワフ・ヤシコフスキ は、ポーランドの論理学者 です。

そして、宣言的スタイル を最初に示した Mizar も、ポーランド で生まれました。

両者に直接の関係があるかどうかは、筆者は確認できていません。

ただ、ポーランドには20世紀前半から強い論理学の伝統があり、その土壌の上に両方が生まれたことは、記しておく価値があると考えます。

---

第４部 ── 「読みやすい」とは、誰にとってか

本記事は「宣言的スタイルは読みやすい」という主張を軸にしています。

しかし、この「読みやすい」という言葉は、そのままでは曖昧です。

誰が読むのか。何のために読むのか。
それによって、必要なものが変わります。

この第４部では、５人の読み手 を順に見ていきます。

① コードを書いている人間のプログラマ

証明を書いている最中の人にとって、読みやすさは、ほとんど問題になりません。

いま何を証明しようとしているのかは、自分が一番よく知っています。

処理系が「まだ証明されていない箇所」を画面に表示してくれれば、それでこと足ります。

この段階では、タクティクのほうが速く書けます。

② 数か月後の自分

ここから、事情が変わります。

第２部で引いた Corbineau の言葉を、もう一度見てください。

**他人の形式的な証明を読む人、あるいは数か月前に自分で書いた証明を読む人のことを考えてみてほしい。

ソースコードで起きるのと同じように、その人は、非常に良い記憶力を持っているか、その証明が徹底的に文書化されていないかぎり、証明で何が起きているのかを理解するのに大いに苦労するだろう。**

（出典）
Pierre Corbineau, "A Declarative Language for the Coq Proof Assistant", TYPES 2007, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年（筆者による日本語訳）

プログラムのコードと同じです。

数か月経てば、書いた本人でも読めなくなります。

そして、証明の場合はさらに厳しい事情があります。

タクティクの列 には、何を証明していたのかが、どこにも書かれていないから です。

③ 同僚、他のエンジニア

②と同じ問題です。

ただし、書いた本人が近くにいない場合、事態はより深刻になります。 質問する相手がいません。

④ 査読者、数学の共同体

ここで、記事の冒頭に戻ります。

しかし、既存の定理証明系は数学には不向きである。その形式的な証明は読めない。

（出典）
Lawrence C. Paulson, ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician, 2017年〜（筆者による日本語訳）

数学者が新しい証明を受け入れるには、その証明を読んで納得する必要があります。

「処理系が検査したから正しい」では足りません。

なぜそう言えるのかを、人が追えなければなりません。

これが、ポールソンが「数学には不向き」と述べた理由 です。

⑤ 大規模言語モデル

そして 2020年代に、新しい読み手 が現れました。

LLM に証明を書かせる研究が、急速に増えてきたのです。

LLMの学習データとして、既存の証明が使われます。

ここで、問題が起きました。

同じ冗長性が、読み手によって評価が逆転する

Isar の証明は、冗長です。

「仮定する」「〜が成り立つ」「よって」と、中間の主張をすべて書き出します。

タクティクなら書かなくてよいものを、宣言的スタイル（Isar）では、明示的に書くため、冗長になるのです。

この冗長性をどう評価するか？

２つの研究がたがいに正反対の評価結果を与えています。

評価１: 冗長だから理解できる

Isar proofs are hierarchically structured and contain enough redundancy, consisting of explicitly stated assumptions and goals, to be understandable both by humans and machines.

筆者による日本語訳:

Isar の証明は階層的に構造化されており、明示的に述べられた仮定と目標から成る十分な冗長性を含むため、人間にも機械にも理解できる。

（出典）
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年

評価２: 冗長さが問題である

There are at least three problems: the abundance of expert-oriented features, extensive syntactic redundancy, and the substantial demand for proof automation in declarative proofs.

（筆者による日本語訳）

問題は少なくとも３つある。

専門家向けの機能の過多、広範な構文の冗長性、そして宣言的な証明における証明自動化への実質的な要求である。

この３つを、順に説明します。

１つ目: 専門家向けの機能が多すぎる

Isar には、熟練の定理証明エンジニア（プログラマ）向けの機能が数多く用意されています。

これは、便利ではあります。

しかし、それらをすべて学習の対象にしなければならないとすれば、機械学習にとっては負担となります。

２つ目: 同じことを書く方法が、何通りもある

第２部で見たとおり、Isar には、事実を渡す構文だけで11種類あります。

そして thus は then show の省略形、hence は then have の省略形でした。

これは人間にとっては、書きやすい形を選べるという意味で利点となりえます。

しかし機械にとっては、「同じ意味なのに見た目が違うもの」が増えるだけです。
学習の対象が、そのぶん複雑になります。

３つ目: 自動証明への依存が大きい

これが、最も分かりにくい点かもしれません。

宣言的スタイル では、「$A$ である」「よって $B$ である」と主張を並べます。

その $A$ から $B$ への飛躍を埋めるのは、処理系の自動証明の仕組みです。

第２部で見た sledgehammer が、その代表です。

つまり、宣言的スタイルで書かれた証明は、それ単独では成立しません。

強力な自動証明の仕組みが、隣にあることを前提にしています。

そして、その自動証明が失敗すれば、証明は通りません。

モデルが正しい主張を並べたとしても、自動証明が追いつかなければ、失敗と判定されるのです。

言い換えると

この論文が問題にしているのは、次のことです。

Isar は、熟練の定理証明エンジニア（プログラマ）、つまり人間、が書くために設計されました。

しかし、LLMが学ぶ学習データとしては、必ずしも都合がよくないのです。

なぜ、評価が逆転するのか

一方は「冗長だから理解できる」と言い、他方は「冗長さが問題だ」と言っています。

注目していただきたいのは、両方の原文に "machine"（機械）という語が使われている点です。

• ポールソンら: 「人間にも機械にも理解できる」
• XUらの論文: 「機械学習にとって」

この２つの「機械」は、まったく違うものを指しています。

ポールソンらの言う「機械」は、証明を検査する処理系 です。

より正確には、Isabelle の「カーネル」を指しています。

カーネル とは、処理系の中核にある、ごく小さな部分のことです。

定理証明支援系 には、便利な機能が数多く備わっています。
しかし、それらが正しいかどうかを最終的に判定するのは、この小さなカーネルだけです。

なぜ小さく作るのか。

そこだけを注意深く検証すれば、処理系全体が信頼できるからです。

冗長であるほど、確かめるべき情報が明示されます。
仮定も目標も、すべてコードに書かれているから です。

XU らの論文 が想定しているのは、証明を学習するLLM（大規模言語モデル） です。

学習データは冗長であればあるほど、学習すべき構文の種類が増えてしまいます。

第２部で見たとおり、Isar には事実を渡す構文だけで11種類あり、そのうちいくつかは同じことの異なる書き方でした。

同じ意味の書き方が複数ある証明プログラムが学習データとなることは、LLMなどの機械学習・深層学習モデルにとって、学習を行う上で負担となり、障害になりえる のです。

タクティク記法のスタイル と 宣言的スタイル。

両者が持つ特徴 は、読み手が変われば長所にも短所にもなりえるということです。

第４部の結論

本記事で「読みやすい」と述べるとき、それは主に次の読み手を指します。

数か月後の自分、同僚、査読者。

すなわち、書いた本人ではない誰か、あるいは書いたときの記憶を忘れてしまった本人です。

そして、この「冗長性の評価が読み手によって逆転する」という論点が、本記事の最後で再び現れます。

LLM が証明を書く時代に、この書き方がなぜ注目されているのか。

その答えは、いま見た対立と直結しています。

詳細は、第12部で扱います。

この点を押さえたうえで、以降を読み進めてください。

第５部 ── 計算をつなぐ書き方

ここからは、宣言的スタイル の 具体的な仕組み を見ていきます。

まず、等式や不等式を順に変形していく書き方 です。

数学の答案では、こう書く

紙の上で計算を進めるとき、こう書きます。

a = b
  = c
  = d

等号を縦に揃えて、一段ずつ変形していきます。

そして最後に、「よって $a = d$ である」と結論します。

この書き方を、そのまま定理証明支援系の言語の構文にしたものがあります。

Isabelle の also と finally

Isabelle では、次のように書きます。

notepad
begin
  have "a = b" sorry
  also
  have "... = c" sorry
  also
  have "... = d" sorry
  finally
  have "a = d" .
end

（出典）
Isabelle の公式資料

読み方を説明します。

• have "a = b" ── まず、$a = b$ であることを示します
• also ── 「さらに」。等式の連鎖を続けます
• have "... = c" ── ここが要点です
• finally ── 連鎖を締めくくります

... という記法

have "... = c" の ... に注目してください。

これは、省略記号ではありません。Isabelle の構文の一部です。

... は、直前の文の右辺を指します。

つまり、have "a = b" の直後に have "... = c" と書けば、それは have "b = c" と書いたことと同じ意味になります。

この記法があるため、b を繰り返し書く必要がありません。

紙の上で、等号を縦に揃えて左辺を省略するのと同じこと です。

finally が何をするか

finally の後には、連鎖の結果が使えるようになります。

上の例では、a = b、b = c、c = d の３つを繋いで、a = d という事実が得られます。

この事実が、finally の直後の証明に注ぎ込まれます。

最後の . は、「もう証明することは無い」という意味です。

a = d は既に手元にあるので、それをそのまま使えばよいのです。

事実を集める moreover と ultimately

似た仕組みが、もう一組あります。

等式の連鎖ではなく、複数の事実を集めて一度に使いたいとき に使います。

proof -
  have "statement1" <proof>
  moreover have "statement2" <proof>
  moreover have "statement3" <proof>
  ultimately show ?thesis <proof>
qed

出典:"Formalizing IMO Problems and Solutions in Isabelle/HOL", 2020年

moreover（さらに）で事実を積み重ね、ultimately（結局）でそれらをまとめて使います。

数学の証明で「以上より」と書くのと、同じ働き です。

【重要】これらは、言語に組み込まれた構文ではない

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

Isabelle の公式資料には、also と finally について、次の趣旨の記述があります。

これらは、利用者の側で定義された 仕組みである。

標準のライブラリに含まれてはいるが、言語そのものに組み込まれた構文ではない。

つまり、Isabelle/Isar は「特定の証明言語」ではなく、「証明を書くための 言語を作るための 枠組み」 でもあるということ です。

必要ならば、自分で新しい書き方を定義できるのです。

第６部 ── Lean 4 の calc

Isabelle の also / finally に相当する仕組みが、Lean 4 にも あります。

calc という名前です。

書き方

Lean 4 では、次のように書きます。

calc a = b := by ...
     _ = c := by ...
     _ = d := by ...

_（アンダースコア）が、Isabelle の ... に相当します。 直前の右辺を指します。

そして、この連鎖全体が a = d という事実になります。

Isabelle との違い

両者を並べてみます。

意味	Isabelle	Lean 4
連鎖を始める	have "a = b"	calc a = b := ...
続ける	also have "... = c"	_ = c := ...
直前の右辺を指す	...	_
締めくくる	finally	（不要。連鎖全体が一つの式）

Lean 4 の calc は、連鎖全体が一つのまとまりです。
始まりと終わりを示す語が要りません。

Isabelle の also / finally は、独立した文をつないでいく形です。

calc で使える関係は、拡張できる

Lean の公式の文書には、次の趣旨の記述があります。

calc は、等式の推移性 のような基本的な原理によって合成されることを意図した、中間の結果をつなぐための便利な記法である。

そして、calc で使える 二項関係の述語の集合 は、利用者が自由に拡張できる。

つまり、= だけでなく、≤ や <、あるいはエンジニアが自分で定義した関係でも使えます。

次のような連鎖が書けるということです。

calc a ≤ b := by ...
     _ < c := by ...
     _ ≤ d := by ...

結果として a < d が得られます。

Lean 4 の have と show

Lean 4 には、Isabelle と 同じ名前 の語もあります。

have（〜が成り立つ）と show（示す）です。

ただし、内部の扱いが違います。

Lean の公式論文から、再び該当部分を引用してみましょう。

have H : p, from s, t という記法は、内部的には項 (λ(H : p), t) s になる。

同様に、show p, from t は、t に期待される型 p を注釈するだけである。

この引用は、少し難しいと思います。順に説明します。

まず、Isabelle の場合

Isabelle で have "Q" と書くと、何が起きるでしょうか。

処理系が持っている「仕様可能な事実の一覧」に、$Q$ が書き加えられます。

Python で言えば、こういう感覚です。

facts = []
facts.append("Q が成り立つ")   # have "Q" にあたる
facts.append("R が成り立つ")   # have "R" にあたる

have は、一覧に追加する命令です。

証明が終われば、この一覧は役目を果たし終わります。

have 自体は、どこにも残りません。

次に、Lean 4 の場合

Lean 4 では、まったく違うことが起きます。

have は、命令ではありません。
関数を作って、それを呼ぶという形に、書き換えられます。

Python で書くと、こうです。

def use_it(H):        # H という名前で、事実を受け取る関数
    return ...        # その事実を使って、続きを行う

use_it(証明)          # 実際に事実を渡して、呼び出す

「$Q$ が成り立つ」という事実に H という名前を付け、その名前を使う関数を作り、そこに事実を渡す。

引用文にある (λ(H : p), t) s は、この形です。

• λ(H : p), t ── 「$H$ という名前で $p$ という事実を受け取り、$t$ を行う関数」
• s ── その関数に渡される、実際の証明
• 全体 ── 関数を作って、すぐに呼び出している

λ は関数を作る記号で、Python の lambda と同じものです。

何が違うのか

Isabelle では、have は「一覧に追加する命令」でした。
証明が終われば消えます。

Lean 4 では、have は「プログラムの一部」になります。**
証明そのものが、実行できるプログラムとして残るのです。

なぜ、そんなことができるのか。

第７部で詳しく扱いますが、簡単に触れておきます。

Lean 4 では、「命題」と「型」が対応し、「証明」と「その型を持つプログラム」が対応します。

「$P$ ならば $Q$」という命題は、「$P$ を受け取って $Q$ を返す関数」の型に対応する。

そして、その命題を証明することは、実際にそういう関数を書くことにあたります。

だから、have が関数の呼び出しに書き換えられるのです。

見た目は同じでも、内部が違う

have "Q" と書く。

見た目は、Isabelle も Lean 4 も同じです。

しかし、Isabelle ではそれが命令として処理され、Lean 4 ではプログラムの一部になります。

この違いが、第７部で重要になります。

Lean 4 には、Mizar に触発された構文もある

先ほどの公式論文には、次の記述もあります。

Lean には、Mizar と Isar に触発された別の構文もある。

ラムダ抽象に対する assume H : p, t と take x : A, t である。

assume と take は、まさに Mizar と Isar の語です。

Lean 4 は、宣言的スタイルの語彙を取り込んでいます。

第７部 ── Agda の等式推論は、別の系統である

Agda という言語にも、calc に似た書き方があります。

しかし、これは別の系統に属します。

その理由を説明します。

Agda の等式推論

Agda では、次のように書きます。

begin
  a
    ≡⟨ step1 ⟩
  b
    ≡⟨ step2 ⟩
  c
∎

begin で始め、≡⟨ ⟩ で一段ずつ変形し、∎（証明終わりの記号）で締めます。

見た目は、Lean 4 の calc によく似ています。

しかし、書いているものが違う

Freek Wiedijk という研究者が、証明の書き方を３つに分類しています。

この分類を借りると、Agda の位置づけがはっきりします。

１つ目: タクティクスタイル

処理系に「こうせよ」と指示を出していく書き方です。

指示を一つ出すたびに、処理系が「では次はこれを証明してください」と返してきます。
その繰り返しで、証明すべきことがなくなれば完了です。

本記事で、これまで見てきた書き方です。

この書き方を採る処理系:
HOL4、HOL Light、ProofPower、Coq、Matita、PVS、B method、Metamath、そして初期の Isabelle

２つ目: 宣言的スタイル

「仮定する」「よって」「示す」と、論証を文章として書いていく書き方です。

そして Wiedijk は、これをさらに２つに分けています。

同じ宣言的スタイルでありながら、「何を書いているのか」が違う のです。

２つ目のＡ: 証明を、文章として書く

数学の教科書に載っている証明を、思い浮かべてください。

「n が偶数であると仮定する。すると n = 2k となる整数 k が存在する。よって n² = 4k² であり、これは4で割り切れる。」

このような文章を、処理系が読める形にしたものを書きます。

「仮定する」「存在する」「よって」といった語を並べ、主張を順に書き下ろしていくのです。

注目すべきは、各段階の間にある細かい推論を、自分で書かなくてよいという点 です。

上の例で言えば、「$n = 2k$ から $n^2 = 4k^2$ が出る」という 部分の計算を、エンジニアは自ら書く必要はありません。

「$n = 2k$ である」と書き、次に「$n^2$ = 4$k^2$ である」と書けば、その間は処理系が自動で埋めてくれます。

エンジニアが書くのは、論証の要点だけ です。

この書き方を採る処理系:
Mizar、Isabelle（その証明言語である Isar を使う場合）

２つ目のＢ: 証明そのものを、部品から組み立てる

こちらは、まったく違います。

文章を書くのではありません。
証明という「もの」を、部品を組み合わせて作り上げます。

プログラムを書く作業に近い、と言ったほうが正確です。

この書き方を採る処理系:
Twelf、Agda、Epigram

ＡとＢの違いを、コードで見てください

言葉だけでは伝わりにくいので、同じ主張を両方の書き方で書いてみます。

証明したい命題
「$n$ が偶数ならば、$n$ の$2$乗は$4$で割り切れる」

まず、$Ａ$の書き方です。
Isabelle の Isar で書きます。

theorem "even n ⟹ 4 dvd n^2"
proof -
  assume "even n"
  then obtain k where "n = 2 * k" ..
  then have "n^2 = 4 * k^2" by simp
  then show "4 dvd n^2" by simp
qed

上から読んでみてください。

• assume "even n" ── 「$n$ は偶数であると仮定する」
• then obtain k where "n = 2 * k" ── 「すると、$n = 2k$ となる $k$ が取れる」
• then have "n^2 = 4 * k^2" ── 「すると、$n$ の$2$乗は $4 k^2$ である」
• then show "4 dvd n^2" ── 「よって、$n$ の$2$乗は$4$で割り切れる」

数学の答案そのものです。

そして注目していただきたいのは、by simp の部分です。

「$n = 2k$ から $n^2$ = 4$k^2$ が出る」++という計算を、エンジニアは自ら記述しません。**

「そうなる」とだけ書いて、あとは simp という自動処理に任せています。

次に、$Ｂ$ の書き方です。
Agda の形式で書きます。

even-sq : (n : ℕ) → Even n → Divides 4 (n * n)
even-sq n evn =
  let (k , eq) = evn
      step1 = cong (λ x → x * x) eq
      step2 = trans step1 (assoc-lemma k)
  in divides-intro (k * k) step2

まったく違う見た目になりました。

• let (k , eq) = evn ── 「偶数であるという証拠から、$k$ と等式を取り出す」
• step1 = cong (λ x → x * x) eq ── 「その等式の両辺を$2$乗する、という操作を適用して、新しい等式を作る」
• step2 = trans step1 (assoc-lemma k) ── 「作った等式と、別の補題を繋いで、さらに新しい等式を作る」
• in divides-intro (k * k) step2 ── 「作った等式を材料に、割り切れることの証拠を組み立てる」

上記の Agda のコード は、$Ａ$ との違いを示すために筆者が構文に基づいて書いたものです。
実機での検証はしていません。

何が違うのか

$Ａ$ では、「$n^2$ = 4$k^2$ である」と、主張を書きました。

$Ｂ$ では、cong (λ x → x * x) eq と書いています。

これは、「eq という等式に、$2$乗する操作 を適用せよ 」という意味です。

主張ではなく、新しいものを作る手順 を、人間の定理証明エンジニアがコードに記述するのです。

そして、その結果に step1 という名前を付け、次の材料にしています。

変数に値を代入し、それを使って次の計算をする。
これは、プログラムを書く作業そのものです。

$Ａ$ では、細かい計算は by simp に任せていました。

$Ｂ$ では、++cong や trans といった部品を、人間の定理証明エンジニアが、自分で選んで組み合わせる必要** があります。 自動で埋めてくれる仕組みは、ここにはありません。

この違いが、両者の違いです。

表にまとめます

	Ａ: 文章として書く	Ｂ: 部品から組み立てる
何を書いているか	論証の筋道	証明という「もの」そのもの
段階の間の細かい推論	処理系が自動で埋める	自分で組み立てる
現れる語彙	assume、have、thus	λ、let ... in、関数の定義
近い作業	数学の答案を書く	プログラムを書く
採用する処理系	Mizar、Isabelle（Isar）	Twelf、Agda、Epigram

３つ目: 処理系に丸ごと任せるスタイル

「これが成り立つ」という主張だけを並べて書き、その証明は処理系が自分で探します。

人間の定理証明エンジニアは、証明の道筋を書きません。

何を示してほしいかだけを書き、あとは処理系に任せます。

この書き方を採る処理系:
ACL2、Theorema

（出典）:F
reek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年

Ａとの違いは、何か

ここで、疑問を持たれた方がいるかもしれません。

「Ａも、主張を並べて書く方式ではなかったか」

そのとおりです。
見た目は、よく似ています。

違いは、隙間の大きさです。

$Ａ$ では、隙間を小さく刻みます。

「$A$ である」「よって $B$ である」「よって $C$ である」と、細かい段階に分けて書きます。

各段階のあいだは、ごく短い距離です。
だから、処理系の自動証明が埋められます。

３つ目のスタイルでは、隙間が大きいままです。

「この補題が成り立つ」とだけ書いて、そこへ至る道筋は書きません。

処理系が、その大きな隙間を自力で埋めます。

連載１回目の話とつながります

連載１回目で、have による分解を扱いました。

うまくいかない箇所があれば、その行をより細かい have に分解する。

「$A$ から $D$ が導出される」を一度に示せなければ、途中に $B$ と $C$ を書き足す。

そうすれば、短い区間をそれぞれ埋めればよくなります。

$Ａ$ は、その「刻む」作業を人間が行う方式です。

３つ目のスタイルは、人間が自ら細かく刻まむことなく、処理系に委ねる方式です。

だから、自動証明の能力が前提になります

３つ目のスタイルが成り立つのは、処理系の自動証明が非常に強力な場合だけです。

ACL2 は、その一例です。

帰納法 を自動で見つけ出す仕組みを持ち、人間が指示しなくても証明を組み立てられる場面が多くあります。

しかし、隙間が大きすぎれば失敗します。

そのため、この方式でも「補題の並べ方」は人間が考えます。
どういう順序で、どの粒度の補題を置けば、処理系が埋められるか。

証明の道筋は書かないが、補題の配置は考える。
それが、この方式の作業です。

３つを、隙間の大きさで並べると

スタイル	人間が書くもの	処理系が埋める隙間
タクティクスタイル	一手ずつの指示	ほぼ無い（人間が全部指示する）
Ａ:文章として書く	細かく刻んだ主張	小さい
３つ目:丸ごと任せる	補題の主張だけ	大きい

人間が書く量が減るほど、処理系が埋める隙間は大きくなります。

そして、隙間が大きいほど、処理系の自動証明の能力が問われます。

Agda は、２つ目のＢに属する

ここまでの説明を経てようやく、Agda の位置が見えてきました。

Agda は、Mizar や Isabelle と同じく、宣言的スタイル に属します。
タクティク を並べる書き方ではありません。

しかし、その中でも別の枝に分かれます。

Mizar と Isabelle が「証明を文章として書く」のに対し、
Agda は「証明そのものを部品から組み立てる」のです。

だから、先ほど見た Agda のコードには、assume も thus も現れませんでした。

代わりに現れたのは、λ や let ... in といった、プログラムを書くための語彙 でした。

そして、これは Agda の欠点ではありません。

Agda では、証明を書くこととプログラムを書くことが、同じ作業 だからです。

前に触れた カリー・ハワード同型対応 が、ここでも威力を発揮します。

対話篇:Ｂは、手続き型に近いのではないか

ここで、疑問を持たれた方がいらっしゃるかもしれません。

その疑問を、タロウくんに代弁してもらいます。

タロウくん:
先生、少し混乱しています。

$Ｂ$ の書き方は 「宣言的スタイル」 に分類されるんですよね？

専任講師:
そうです。

タロウくん:
でも、さっきの Agda のコードを見ると、step1 を作って、それを使って step2 を作って……と、手順を書いている ように見えます。

専任講師:
はい。

タロウくん:
それって、タクティクスタイル と同じで、手続き型 なのでは？

専任講師:**
とてもいい疑問です。

その混乱は私の説明の仕方にも原因があります。
「手順」という言葉を使ってしまいましたから。

タロウくん:
違うんですか。

専任講師:
違います。

ただし、その違いは注意して見ないと分かりません。

まず、タクティクスタイル が何をしているかを、思い出してください。

タロウくん:
「場合分けせよ」とか「簡単にせよ」とか、指示を出していました。

専任講師:
そうですね。

その指示を出すと、何が起きましたか？

タロウくん:
画面に表示されている目標が、書き換わりました。

専任講師:
そこが要点です。

タクティク は、処理系が持っている状態を変化させます。

いま何を証明すべきか、という 状態が、命令のたびに書き換わっていく。

タロウくん:
はい。

専任講師:
だから、命令を出す順序が変われば、結果も変わります。

同じ命令でも、その時点の状態が違えば、違う結果になる。

タロウくん：
・・・なるほど。

専任講師:
では、Ａの Isar を見てください。

have "n^2 = 4 * k^2" と書きました。

これは、処理系に何かを命令していますか？

タロウくん:
いえ・・・
「$n$ の $2$ 乗は $4 k^2$ である」と、言っているだけです。

専任講師:
そのとおりです。

主張を述べているだけで、状態を書き換えていません。

タロウくん:
では、Ｂはどうなんですか。

step1 = cong (λ x → x * x) eq は、明らかに何かをしているように見えますが。

専任講師:
よく見てください。

これは、eq という既にあるものから、step1 という新しいものを作っています。

タロウくん:
はい。

専任講師:
では、eq はどうなりましたか？

タロウくん:
そのままです。 変わっていません。

専任講師:
そこが決定的です。

タクティクなら、命令を出した時点で元の状態が書き換わります。

Ｂでは、元のものはそのまま残り、新しいものが増えるだけ です。

タロウくん:
あ。Python で言うと・・・

total = total + n のように変数の中身を書き換えるのが タクティクスタイル で、
doubled = [n * 2 for n in numbers] のように新しい変数を作るのが Ｂ、ということですか？

専任講師:
まさにそのとおりです。

よく気づきましたね。

タロウくん:
でも、それだと 「宣言的」 と呼ぶ理由が、まだ分かりません。

新しい変数を作るのも、手順といえば手順ですよね？

専任講師:
では、こう考えてください。

step1 = cong (λ x → x * x) eq という行を、日本語にするとどうなりますか。

タロウくん:
「step1 は、eq の両辺を2乗したものを、cong で作ったものです」
・・・あ。

専任講師:
気づかれましたね。

タロウくん:
「〜せよ」ではなく、「〜である」と言っています。

専任講師:
そこが、宣言的と呼ばれる理由です。

この行は、step１ とは何であるかを定義 しています。
命令ではなく、定義 です。

タロウくん:
Ａの have "n^2 = 4 * k^2" も、「$n^2$ は 4$k^2$ である」と言っていました。

専任講師:
同じことです。

ＡもＢも、「これが成り立つ」「これはこういうものだ」 と述べているだけ です。

処理系に命令を出していません。

タロウくん:
だから、両方とも宣言的スタイルなんですね？

専任講師:
そのとおりです。

そして、ＡとＢの違いは、述べている対象が違うだけです。

Ａは、論証の筋道を述べ、
Ｂは、証明という「もの」の構造を述べている。

タロウくん:
整理できました。

「命令か、定義か」 が、手続き型と宣言的スタイルを分ける境目 なんですね。

専任講師:
それが、この分類の本質です。

この対話で見たとおり、$Ｂ$ は手続き型ではありません。

各行が「〜せよ」ではなく「〜である」を述べているという点で、$Ａ$ と同じ性質を持っています。

「証明の対象」とは何か

Agda が属する (2b) では、「証明の対象を 構文として書き表す 」とあります。

証明の対象とは何でしょうか。

カリー・ハワード対応 と呼ばれる考え方があります。

簡単に言えば、次のとおりです。

• 命題は、型に対応する。
• 証明は、その型を持つ項に対応する。

「項」 というのは、プログラムの式のことだと思ってください。

具体例で説明します。

「A ならば B」という命題を考えます。

これは、「A を受け取って B を返す関数」の型 に対応します。

そして、その命題の 証明 は、実際にそういう関数を書き、型検査を通すこと にあたります。

つまり、証明を書くこととプログラムを書くことが、同じ作業 になります。

なお、ここで必要なのは 「型検査を通ること」であって、「実行して動くこと」ではありません。

関数が宣言どおりの型を持つと処理系が確認できれば、その時点で証明は完了します。

この論点については、筆者が以前に公開した記事でも取り上げています。

• Cubical Agda とは何か
• Rocq（旧名 Coq）とは何か

Mizar 系と Agda 系の違い

この対応を踏まえると、両者の違い が見えてきます。

	Mizar・Isabelle（自然言語型）	Agda（証明対象型）
書いているもの	証明の文書	証明の対象そのもの
語彙	assume、have、thus	λ、let ... in、関数の定義
段階の間の隙間	処理系が自動で埋める	書き手が項として書く
証明の実体	文書。処理系が読み取って検査する	項そのもの

Mizar や Isabelle では、「仮定する」「よって」と書きます。

これは、論証を文章として書いているのであり、その文章から証明の対象を組み立てるのは処理系の仕事 です。

Agda では、人間の定理証明エンジニアが、証明の対象そのものを書きます。
ラムダ式や関数の定義として。

そのため、Agda のコードには assume も thus も現れません。

なぜ、見た目が似るのか

では、なぜ Agda の 等式推論は calc に似て見えるのでしょうか。

答えは、Agda の 等式推論 が「ライブラリで提供された仕組み」だからです。

言語に組み込まれた構文ではありません。

begin、≡⟨ ⟩、∎ は、いずれも標準ライブラリで定義された演算子です。

そして、それらを組み合わせた結果は、やはり 項 になります。

つまり、Agda の 等式推論 は「読みやすく書くための工夫」であって、系統としては (2b) のままです。

Lean 4 は、両方にまたがる

ここで、Lean 4 の位置づけが問題になります。

Lean 4 は、Agda と同じく依存型という仕組みを採用しています。

依存型とは、型の中に値を書き込める仕組みのことです。

Python の 型ヒント で List[int] と書けば「整数のリスト」を表せますが、「長さが３のリスト」は表せません。

依存型のある言語では、「長さが３のリスト」という方を定義することができます。

この仕組みがあるため、「証明」を「プログラムの式」として表現できます。

そして Lean 4 では、証明が式として表現されます。

しかし同時に、assume、have、show、take という Mizar 系の語彙も持っています。

したがって、Wiedijk の二分類には収まらないのです。

そこで、この記事では、次の３分類を導入します。

系統	書いているもの	処理系
証明の文書として書く	論証を文章として書く。段階の間の自明な推論は処理系が埋める	Mizar、Isabelle（Isar）、HOL Light（miz3）、Rocq（C-zar）
証明の対象として書く	証明そのものを項として書く	Twelf、Agda、Epigram
両方にまたがる	Mizar 系の語彙も持ち、項としても書ける	Lean 4

---

第８部 ── 同じ定理を、６つの言語で書く

ここまで、宣言的スタイルの仕組み を見てきました。

この部では、実際のコードを並べます。

なぜ、この定理を選んだのか

６つの言語のコードを並べるにあたり、比較に使う定理を一つ選ぶ必要がありました。

ところで、数学の証明とはどういうものかを、数学を専門としない方に示すとき、必ず使われる定理が２つあります。

• 素数が無限にあること（ユークリッドの証明）
  &mbsp;
• $\sqrt{2}$ が無理数であること

本記事では、後者を選びました。

理由は３つあります。

（理由１） ６つの言語すべての実際のコードが無料公開されているから

Freek Wiedijk が編纂した資料があります。

書誌情報
Freek Wiedijk 編, "The Seventeen Provers of the World", Lecture Notes in Artificial Intelligence 第3600巻, Springer, 2006年。序文はダナ・スコット（カーネギーメロン大学 名誉教授）。

$\sqrt{2}$ が無理数であることの証明を、１７個の処理系で書き比べたものです。

（理由２） 同じ人物が編纂した資料であり、比較の条件が揃っているから

各処理系の執筆者は、同じ依頼を、同じ条件で受け取っています。

ばらばらの出典から集めたコードを並べるのとは、比較の質が違います。

（理由３） 各処理系の作者本人が書いたコードだから

• Mizar のコードを書いたのは、Mizar の設計者である Andrzej Trybulec
• Isabelle/Isar のコードを書いたのは、Isar の設計者である Markus Wenzel と Isabelle の作者である Lawrence Paulson
• Agda のコードを書いたのは、Thierry Coquand

編者の Wiedijk は、自分では一つも書きませんでした。

その理由を、彼はこう述べています。

I did not want to write any of the formalizations myself, as I wanted the formalizations to be 'native' to the system.

I am a Coq/Mizar user, so my formalizations would have been too 'Coq-like' or 'Mizar-like' to do justice to the other systems.

（筆者による日本語訳）

**私は形式化を自分で書きたくなかった。

形式化がその処理系にとって「土着のもの」であってほしかったからである。

私は Coq と Mizar の利用者なので、私が書いた形式化は、他の処理系に対して公平を欠くほど「Coq らしい」か「Mizar らしい」ものになってしまっただろう。**

出典:同資料、8頁

それぞれの処理系を最もよく知る人物が、その処理系にとって自然な書き方で書いています。

なお、Wiedijk も２つの定理で迷った

同じ資料に、次の記述があります。

There are two canonical proofs that are always used to show non-mathematicians what mathematical proof is: The proof that there are infinitely many prime numbers.

The proof of the irrationality of the square root of two.

From those two I selected the second, because it involves the real numbers.

（筆者による日本語訳）

**数学の証明とはどういうものかを、数学者でない人に示すために必ず使われる、標準的な証明が２つある。

素数が無限にあることの証明と、２の平方根が無理数であることの証明である。

この２つのうち、私は後者を選んだ。実数が関わるからである。**

出典
同資料、9頁

実数を扱うには、それを形式化する作業が必要 です。

どの処理系がその作業を済ませているのか、そしてそれがどう仕上がっているのかが見える、というのが Wiedijk の選定理由でした。

素数の無限性のコードを見たい方へ

素数が無限にあることの証明も、Mizar と Isar の両方で書かれた資料が存在します。

• Markus Wenzel, Freek Wiedijk, "A Comparison of Mizar and Isar", Journal of Automated Reasoning 第29巻第3〜4号, 389〜411頁, 2002年
• 論文の頁:https://link.springer.com/article/10.1023/A:1021935419355

ただし、この論文は購読制です。

ご自身でコードをご覧になりたい方は、Springer の購読、または所属機関を通じた入手が必要になります。

証明したい命題

さて、証明する内容を確認します。

「$\sqrt{2}$ は無理数である」 ── つまり、$\sqrt{2}$ は分数で表せない、ということです。

証明の筋道は、次のとおりです。

1. $\sqrt{2}$ が分数で表せると仮定する
2. その分数を、これ以上約分できない形にする
3. すると、分子も分母も偶数であることが導かれる
4. これは「約分できない」という前提と矛盾する
5. よって、$\sqrt{2}$ は分数で表せない

上記の２から３に至る道筋を補足説明させていただきます。

1. その分数を、これ以上約分できない形にする

どんな分数でも、約分を繰り返せば、それ以上約分できない形になります。

たとえば $6/4$ は $3/2$ に、$10/8$ は $5/4$ になります。

これ以上約分できないということは、分子と分母が共通の約数を持たないということです。

特に、両方が偶数になることはありません。

両方が偶数なら、2で割れてしまうからです。

1. すると、分子も分母も偶数であることが導かれる

ここが、この証明の山場です。

$\sqrt{2} = a/b$ と書けたとします。
両辺を2乗すると $2 = a^2/b^2$、つまり $a^2 = 2b^2$ です。

$a^2$ は 2$b^2$ に等しいので、$a^2$ は偶数です。

そして、2乗して偶数になる数は、それ自身も偶数です。
奇数を2乗しても奇数にしかならないからです。よって、a は偶数です。

$a$ が偶数なら、$a = 2c$ と書けます。

これを $a^2 = 2b^2$ に代入すると、$4c^2 = 2b^2$、すなわち $b^2 = 2c^2$ となります。

同じ理屈で、$b^2$ が偶数なので、b も偶数です。

つまり、a も b も偶数だと分かりました。

1. これは「約分できない」という前提と矛盾する

しかし、２番目で「これ以上約分できない形にした」はずでした。

a も b も偶数なら、まだ2で割れます。 約分できてしまいます。

矛盾です。

1. よって、$\sqrt{2}$ は分数で表せない

矛盾が生じたということは、出発点の仮定が誤っていたということです。

つまり、「$\sqrt{2}$ が分数で表せる」という仮定が誤りでした。

したがって、$\sqrt{2}$ は分数では表せません。これが、無理数であるということです。

以上が、以下の「２」から「３」に至る道筋です。

（再掲）

1. $\sqrt{2}$ が分数で表せると仮定する
2. その分数を、これ以上約分できない形にする
3. すると、分子も分母も偶数であることが導かれる
4. これは「約分できない」という前提と矛盾する
5. よって、$\sqrt{2}$ は分数で表せない

上記の「１」から「５」に至るこの筋道が、各言語のコードにどう表れるかを見てください。

① Mizar

出典
Freek Wiedijk 編, "The Seventeen Provers of the World", Lecture Notes in Artificial Intelligence 第3600巻, Springer, 2006年, 27〜28頁

このコードを書いたのは、Mizar の設計者である Andrzej Trybulec 本人です。

定理の記述

sqrt 2 is irrational

証明の本体

theorem
sqrt 2 is irrational
proof
  assume sqrt 2 is rational;
  then consider i being Integer, n being Nat such that
W1: n<>0 and
W2: sqrt 2=i/n and
W3: for i1 being Integer, n1 being Nat st n1<>0 & sqrt 2=i1/n1 holds n<=n1
    by RAT_1:25;
A5: i=sqrt 2*n by W1,XCMPLX_1:88,W2;
C:  sqrt 2>=0 & n>0 by W1,NAT_1:19,SQUARE_1:93;
    then i>=0 by A5,REAL_2:121;
    then reconsider m = i as Nat by INT_1:16;
A6: m*m = n*n*(sqrt 2*sqrt 2) by A5
    .= n*n*(sqrt 2)^2 by SQUARE_1:def 3
    .= 2*(n*n) by SQUARE_1:def 4;
    then 2 divides m*m by NAT_1:def 3;
    then 2 divides m by INT_2:44,NEWTON:98;
    then consider m1 being Nat such that
W4: m=2*m1 by NAT_1:def 3;
    m1*m1*2*2 = m1*(m1*2)*2
    .= 2*(n*n) by W4,A6,XCMPLX_1:4;
    then 2*(m1*m1) = n*n by XCMPLX_1:5;
    then 2 divides n*n by NAT_1:def 3;
    then 2 divides n by INT_2:44,NEWTON:98;
    then consider n1 being Nat such that
W5: n=2*n1 by NAT_1:def 3;
A10: m1/n1 = sqrt 2 by W4,W5,XCMPLX_1:92,W2;
A11: n1>0 by W5,C,REAL_2:123;
    then 2*n1>1*n1 by REAL_2:199;
    hence contradiction by A10,W5,A11,W3;
end;

注目していただきたい語

• assume ── 「$\sqrt{2}$ は有理数であると仮定する」
• then consider ... such that ── 「そのような整数 i と自然数 n を取る」
• then ── 「すると」
• .= ── 等式の連鎖。Isabelle の also に相当します
• by ── その主張の根拠となる定理の名前
• hence contradiction ── 「よって矛盾する」

W1、W2、A5、A6 といった記号は、プログラマが主張に付けた通し番号です。
任意に決められます。i、n、m などの変数名も同じです。

RAT_1:25、XCMPLX_1:88 といった記号は、ライブラリに登録された定理の名前です。
他の文字列に変えると動きません。

theorem、proof、assume、consider、then、hence、by、end は予約語です。

英語の数学の文章として読める形になっています。

by RAT_1:25 のような記号は、ライブラリに登録された定理の名前です。
RAT_1 という論文の25番目の定理、という意味です。

【重要】Trybulec 自身の注記

同じ資料に、Trybulec本人 が次のように書いています。

The actual proof in Mizar would now be as follows:

sqrt 2 is irrational by IRRAT_1:1, INT_2:44;

The presented proof is an adjusted version of the proof that the square root of any prime number is irrational (IRRAT_1:1).

So, this is what the proof would have looked like if Freek Wiedijk had not submitted the IRRAT_1 article to the MML in 1999.

（筆者による日本語訳）

Mizar における実際の証明は、いまなら次のようになる。

sqrt 2 is irrational by IRRAT_1:1, INT_2:44;

**ここに示した証明は、任意の素数の平方根が無理数であることの証明（IRRAT_1:1）を調整した版である。

つまり、Freek Wiedijk が1999年に IRRAT_1 の記事を MML に投稿していなかったなら、証明はこのようになっていただろう、というものである。**

出典:
同資料、30頁

この注記は重要です。

ライブラリに定理が蓄積されていれば、証明は一行で済みます。

「２は素数である」という定理（INT_2:44）と、「素数の平方根は無理数である」という定理（IRRAT_1:1）。

この２つを呼び出すだけです。

MML とは、Mizar Mathematical Library の略です。

Mizarの証明を蓄積したライブラリ で、1989年から 積み上げられているものです。

② Isabelle/Isar

出典:同資料、49〜52頁

このコードを書いたのは、Isar の設計者である Markus Wenzel と、Isabelle の作者である Lawrence Paulson です。

定理の記述

sqrt (real (2::nat)) ∉ ℚ

証明の本体

theorem sqrt-prime-irrational: p ∈ prime =⇒ sqrt (real p) ∉ ℚ
proof
  assume p-prime: p ∈ prime
  then have p: 1 < p by (simp add: prime-def)
  assume sqrt (real p) ∈ ℚ
  then obtain m n where
    n: n ≠ 0 and sqrt-rat: |sqrt (real p)| = real m / real n
    and gcd: gcd (m, n) = 1 ..
  have eq: m² = p * n²
  proof −
    from n and sqrt-rat have real m = |sqrt (real p)| * real n by simp
    then have real (m²) = (sqrt (real p))² * real (n²)
      by (auto simp add: power2-eq-square)
    also have (sqrt (real p))² = real p by simp
    also have ... * real (n²) = real (p * n²) by simp
    finally show ?thesis ..
  qed
  have p dvd m ∧ p dvd n
  proof
    from eq have p dvd m² ..
    with p-prime show p dvd m by (rule prime-dvd-power-two)
    then obtain k where m = p * k ..
    with eq have p * n² = p² * k² by (auto simp add: power2-eq-square mult-ac)
    with p have n² = p * k² by (simp add: power2-eq-square)
    then have p dvd n² ..
    with p-prime show p dvd n by (rule prime-dvd-power-two)
  qed
  then have p dvd gcd (m, n) ..
  with gcd have p dvd 1 by simp
  then have p ≤ 1 by (simp add: dvd-imp-le)
  with p show False by simp
qed

corollary sqrt (real (2::nat)) ∉ ℚ
  by (rule sqrt-prime-irrational) (rule two-is-prime)

注目していただきたい語

• assume ── 「p は素数であると仮定する」
• then have ── 「すると、〜が成り立つ」
• obtain ... where ── 「そのような m と n を取る」
• also と finally ── 第５部で見た等式の連鎖です
• ... ── 直前の右辺を指す記法
• show ?thesis ── 「示すべきことを示す」
• proof と qed ── 証明の始まりと終わり

sqrt-prime-irrational という定理の名前、
p-prime、sqrt-rat、gcd、eq といった仮定への名前、
そして m、n、k、p という変数名は、いずれもプログラマが任意に付けたものです。

prime-def、power2-eq-square、prime-dvd-power-two、two-is-prime は、ライブラリに登録された定理の名前です。
他の文字列に変えると動きません。

theorem、proof、assume、have、show、obtain、also、finally、qed は予約語です。

?thesis は「いま示すべきこと」、... は「直前の右辺」を指す、予約された記法です。
simp、auto、rule はタクティクの名前です。

第２部と第５部で見た語が、実際に使われています。

なお、この証明は「任意の素数の平方根は無理数である」という、より一般的な命題を証明しています。

最後の２行で、それを「２の平方根」の場合に当てはめています。

【補足】Isar には、別の書き方もある

同じ資料には、同じ定理を 「線形の前向き推論」 で書いた版も掲載されています。

Wenzel 自身が、次のように書いています。

Here is an alternative version of the main proof, using mostly linear forward-reasoning. >

While this results in less top-down structure, it is probably closer to proofs seen in mathematics.

（筆者による日本語訳）

**主要な証明の代替版がここにある。ほとんど線形の前向き推論を使ったものである。

これは上から下への構造は減るが、おそらく数学で見られる証明により近い。**

出典
同資料、51頁

同じ Isar でも、書き方に幅があります。

③ Agda

出典:
同資料、58〜61頁

このコードを書いたのは、Thierry Coquand です。

定理の記述

prime p → noether A (multiple p) → isNotSquare p

定義の例

noether (A ∈ Set, R ∈ rel A) ∈ Type
noether A R ≡
  (P ∈ pred A) → (x ∈ A) → ((y ∈ A) → (R y x → P y) → P x) → (x ∈ A) → P x

isNotSquare ∈ pred A
isNotSquare ≡ λ p → (x, y ∈ A) → ¬ ((p · square x) == square y)

主定理

theorem (p ∈ A) ∈ prime p → noether A (multiple p) → isNotSquare p
theorem p ≡
  λ h1 h2 →
    let rem ∈ (x ∈ A) → ¬ (Square p x)
        rem ≡ infiniteDescent A (multiple p) (Square p) h2 (lemma5 h1)
    in λ x y h3 → rem x (Witness y h3)

注目していただきたいのは、ここに現れる語です。

λ（ラムダ抽象）、let ... in、≡（定義）、Witness。

assume も thus も、どこにもありません。

第７部で述べたとおり、Agda は「証明の対象そのもの」を 項 として書きます。
そのため、関数型プログラミングの語彙が並びます。

Coquand 自身が、同じ資料でこう答えています。

It feels like programming in a functional language with dependent types.

The construction of the proof/program can be done interactively with place-holders/meta-variables.

（筆者による日本語訳）

**依存型を持つ関数型言語でプログラムを書いているように感じられる。

証明とプログラムの構築は、プレースホルダーやメタ変数を使って対話的に行える。**

出典
同資料、62頁

「証明を書いている」ではなく、「プログラムを書いている」と述べています。

④ Lean 4

Lean 4 のコードは、上記の資料には含まれていません。
2006年の資料であり、Lean 4 はまだ存在しなかったからです。

そこで、現在の Mathlib（ Lean 4 の数学ライブラリ ）から引きます。

出典:
Mathlib.Data.Real.Irrational

定義

def Irrational (x : ℝ) := x ∉ Set.range ((↑) : ℚ → ℝ)

定理

theorem irrational_sqrt_two : Irrational (√2) := by
  simpa using Nat.prime_two.irrational_sqrt

一行です。

この一行の意味（説明の出典:read-lean）:

**「２は素数である」という定理と、「素数の平方根は無理数である」という定理を利用している。

定理 irrational_sqrt_two は引数を持たないことに注意されたい。

それはちょうど一つのことを述べている。√2 は無理数である、と。**

【重要】Mizar と Lean 4 の一行は、同じ構図である

先ほど見た Trybulec の注記を、思い出してください。

Mizar:   sqrt 2 is irrational by IRRAT_1:1, INT_2:44;

Lean 4:  theorem irrational_sqrt_two : Irrational (√2) := by
           simpa using Nat.prime_two.irrational_sqrt

どちらも、「ライブラリに既にある定理を２つ呼び出すだけ」です。

• 「２は素数である」（Mizar の INT_2:44、Lean 4 の Nat.prime_two）
• 「素数の平方根は無理数である」（Mizar の IRRAT_1:1、Lean 4 の irrational_sqrt）

処理系が違っても、ライブラリに収蔵された定理が豊富になれば、証明は一行になります。

これは、宣言的スタイル か タクティク かという問題とは、別の話です。

過去に証明された定理が、ライブラリに蓄積されているかどうかの問題です。

Lean 4 で、一から書いた場合

では、ライブラリに頼らず書くとどうなるでしょうか。

出典:My First Lean 4 Proof: the Irrationality of $\sqrt{2}$, 2026年3月

import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Tactic

-- 補題:n の２乗が偶数ならば、n も偶数である
lemma even_of_even_sq {n : ℕ} (h : 2 ∣ n ^ 2) : 2 ∣ n := by
  exact (Nat.Prime.dvd_of_dvd_pow Nat.prime_two h)

-- 主定理:2 * m² = n² を満たす互いに素な m, n は存在しない
theorem sqrt2_irrat : ¬ ∃ m n : ℕ, 2 * m ^ 2 = n ^ 2 ∧ Nat.Coprime m n := by
  rintro ⟨m, n, hmn, hcop⟩
  have h2n : 2 ∣ n ^ 2 := ⟨m ^ 2, by linarith⟩
  have hn : 2 ∣ n := even_of_even_sq h2n
  obtain ⟨k, rfl⟩ := hn
  have h2m : 2 ∣ m ^ 2 := by
    have : 2 * m ^ 2 = 4 * k ^ 2 := by ring_nf at hmn ⊢; linarith
    exact ⟨k ^ 2, by linarith⟩
  have hm : 2 ∣ m := even_of_even_sq h2m
  exact Nat.not_coprime_of_dvd_of_dvd (by norm_num) hm ⟨k, rfl⟩ hcop

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

have が４回、obtain が１回、現れています。

これらは、Isabelle の Isar と同じ語です。

つまり、Lean 4 の タクティクモード の中に、宣言的スタイルの語彙 が混ざっています。

第７部で述べた「 Lean 4 は両方にまたがる 」という 位置づけを体現する実例のひとつ です。

⑤ HOL Light の miz3

miz3 のコードは、上記の資料には含まれていません。

miz3 が作られたのは2012年、資料は2006年だからです。

そこで、miz3 の論文から引きます。

出典
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年, 12〜13頁

定理は、スマリヤンの「ドリンカーの原理」 です。

「酒場には、その人が飲んでいるならば全員が飲んでいる、という人が必ずいる」 という、一見すると奇妙な主張 です。

let DRINKER = thm `;
  let P be A->bool;
  thus ?x. P x ==> !y. P y [22]
  proof
    (?x. ~P x) \/ ~(?x. ~P x) [1];
    cases by 1;
    suppose ?x. ~P x [2];
      consider x such that ~P x [3] by 2;
      take x;
      assume P x [4];
      F [5] by 3,4;
      thus !y. P y [6] by 5;
    end;
    suppose ~(?x. ~P x) [10];
      consider a being A such that T;
      take a;
      assume P a [11];
      let y be A;
      P y \/ ~P y [12];
      cases by 12;
      suppose P y [13];
        thus P y by 13;
      suppose ~P y [14];
        ?x. ~P x [15] by 14;
        F [16] by 10,15;
        thus P y [17] by 16;
      end;
    end;
  end`;;

注目していただきたい語

thus、cases by、suppose、consider ... such that、take、assume、let ... be。

Mizar の語彙と、ほとんど同じです。

それもそのはずで、miz3 は Mizar の言語を HOL Light の上に載せたものです。

miz3 の「3」は、Wiedijk が開発した ３番目の Mizar モードであること を指します。

ここで、角括弧に囲まれた数字について説明します。

[1]、[2]、[3] といった数字は、プログラマが各行に付けた通し番号です。

後の行から「あの行で示したことを使う」と指し示すために付けます。

実際の使われ方を見てください。

(?x. ~P x) \/ ~(?x. ~P x) [1];
cases by 1;

１行目で「飲んでいない人が存在するか、存在しないかのどちらかである」と述べ、[1] という番号を付けています。

２行目の cases by 1 は、「１番で述べたことを根拠に、場合分けせよ」という意味です。

もう一つ、見てください。

consider x such that ~P x [3] by 2;
assume P x [4];
F [5] by 3,4;

F [5] by 3,4 は、「３番と４番を根拠に、矛盾が導かれる。これを５番とする」という意味です。

F は矛盾を表す記号です。

この番号は、プログラマが任意に決められます。

通し番号である必要すらありません。
上のコードでも、[6] の次が [10] になっており、間が飛んでいます。

大切なのは、番号を付けた行と、それを参照する行とで、数字が一致していることだけです。

Python で変数に名前を付けるのと、同じことだと考えてください。 total でも sum_value でも動きますが、使うときは同じ名前で呼ばなければなりません。

そして、この番号こそが、宣言的スタイル の要点の一つです。

「どの主張を根拠にして、次の主張を導いたのか」が、コードに明示されています。

タクティクスタイルでは、この情報がどこにも残りませんでした。
処理系が内部で持っている状態から、自動的に使われるだけだったからです。

⑥ Rocq の C-zar

C-zar のコードは、第２部で既に見ました。

もう一度、掲げます。

出典
Pierre Corbineau, "A Declarative Language for the Coq Proof Assistant", TYPES 2007, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年, 72頁

Lemma double_div2: forall n, div2 (double n) = n.
proof.
  let n:nat.
  per induction on n.
  suppose it is 0.
    reconsider thesis as (0=0).
    thus thesis.
  suppose it is (S m) and Hrec:thesis for m.
    have (div2 (double (S m))
          = div2 (S (S (double m)))).
    ~= (S (div2 (double m))).
    thus ~= (S m) by Hrec.
  end induction.
end proof.
Qed.

注目していただきたい語

let ... be、per induction on、suppose it is、have、thus、reconsider ... as、~=。

~= は、Isabelle の also に相当する等式の連鎖です。

【注意】miz3 と C-zar だけ、定理が違う

上記のとおり、miz3 と C-zar については、$\sqrt{2}$ の無理性のコードを入手できませんでした。

そのため、それぞれの論文に掲載されている実例を、そのまま使っています。

比較の条件が揃っていない点は、お断りしておきます。

ただし、C-zar については、同じ定理を タクティクスタイル で書いた版も同じ論文に掲載されており、第２部で並べて示しました。

同じ処理系での書き分けを見るという点では、むしろ好都合です。

語彙の対応表

６つの言語の語彙を、対応させます。

働き	Mizar	Isabelle（Isar）	Lean 4	miz3	C-zar	Agda
仮定する	assume	assume	assume	assume	assume	──
中間の主張	（文を書く）	have	have	（文を書く）	have	──
目標を示す	thus	show	show	thus	thus	──
変数を固定する	let	fix	intro	let	let	──
存在するものを取る	consider	obtain	obtain	consider	consider	──
存在の証人を示す	take	show	exists	take	take	──
計算を繋ぐ	.=	also / finally	calc	.=	~=	≡⟨ ⟩
場合分け	per cases	next	cases	cases / suppose	per cases	──
証明の開始	proof	proof	by / :=	proof	proof	──
証明の終了	end	qed	（不要）	end	end proof	──

Agda の欄が空いているのは、第７部で述べたとおり、系統が違うからです。

残る５つの言語では、語彙が驚くほど共通しています。

なぜ、こんなにも似ているのか

Wiedijk が、その理由を述べています。

Most declarative systems have essentially the same proof language.

In other words, declarative interactive theorem provers have proof languages that are much more similar to each other than the languages of procedural systems are.

（筆者による日本語訳）

ほとんどの宣言的なシステムは、本質的に同じ証明言語を持つ。

言い換えれば、宣言的な対話型定理証明系の証明言語は、手続き的なシステムの言語どうしよりも、はるかに互いに似ている。

出典
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年

そして、その理由も述べています。

It turns out that the languages of declarative systems are all close to Jaśkowski/Fitch-style natural deduction.

（筆者による日本語訳）

宣言的なシステムの言語は、いずれもヤシコフスキ／フィッチ流の自然演繹に近いことが分かる。

出典
同上

第３部で見たとおりです。

なお、引用に出てくるシークエント計算も、ゲンツェン が考案した証明体系です。

自然演繹とは別の流儀 で、証明そのものの性質を調べる研究に向いています。
本記事では立ち入りません。

多くの宣言的な証明言語が、1934年のヤシコフスキ／フィッチ流の自然演繹に近い構造を持っています。

だから似ているのです。

ただし、すべての処理系がこの系譜に属するわけではありません。

第７部で見るとおり、Agda のように、証明を項として表現する別系統 もあります。

第９部 ── 30年の移植史

ここまで、宣言的スタイルの仕組みと、６つの言語のコード例 を見てきました。

この部からは、別の話をします。

この書き方は、どれだけ広まったのでしょうか。

最初の実装:Mizar

実用的な定理証明言語として、宣言的スタイルを早期に実装した代表例が Mizar です。

ポーランド で、Andrzej Trybulec によって設計されました。

なお、「最初」と言い切らないのには理由があります。

第３部で見たとおり、論証を「仮定を置き、帰結を導く」形で書き表す考え方そのものは、1934年のヤシコフスキにさかのぼります。

そして本記事の後半で見るとおり、Agda のように別の系統に属する処理系もあります。

Mizar が果たしたのは、その考え方を、実際に動く定理証明支援系として実装したこと です。

1973年に始まりました。

Mizar の公式サイトには、その思想が最初に発表されたのは1973年11月14日、ワルシャワ大学の図書館情報学・科学情報研究所での研究会であったと記されています。

出典
Mizar Home Page

いま（2026年）からおよそ50年以上前のことです。

なお、一部の資料は開始年を 1974年としています。

Mizar の特徴は、記法が人間の書く数学の文章に極めて近いこと でした。

第８部で見たコードを思い出してください。

assume、consider ... such that、hence contradiction。

英語の数学の文章として読める形になっていました。

なお、Mizar そのものについては、本記事では、宣言的スタイルの起点として のみ取り上げます。

この言語が持つ50年の歴史と、そこに蓄積された数学については、近日中に単独の記事を公開する予定です。

そして、移植が始まった

Mizar の読みやすさは、他の処理系 の開発者たちの目に留まりました。

「この書き方を、自分の処理系にも載せられないか。」

その試みが、30年にわたって繰り返されることになります。

移植の一覧

年	実装	載せた先	作者
1973年頃	Mizar	（言語そのもの）	Andrzej Trybulec
1996年	Mizar Mode for HOL	HOL	John Harrison
1997年	DECLARE	高階論理（独立した処理系）	Don Syme
1999年	Isar	Isabelle	Markus Wenzel
2001年	Mizar-light	HOL Light	Freek Wiedijk
2004年	MMode	Coq	Mariusz Giero, Freek Wiedijk
2007年	C-zar	Coq	Pierre Corbineau
2012年	miz3	HOL Light	Freek Wiedijk
時期不明	PhoX の宣言版	PhoX	Christophe Raffalli
2026年	Lisar	Lean 4	AI が書いた概念実証

出典:
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年、および各実装の論文

30年にわたって、10種類以上の実装が作られてきました。

わずか41行で実装できる

この一覧の中で、特に注目していただきたいものがあります。

2001年の Mizar-light です。

Wiedijk がこれについて、次の趣旨を述べています。

Mizar の証明言語を HOL の上に実装した。
それは わずか41行の ML から成り、手続き的スタイルと宣言的スタイルが実際にはどれほど近いかを示している。

41行です。

宣言的スタイルを載せるのに、特別な仕組みは要りません。

なお、この記述は Wiedijk の Mizar-light の論文（TPHOLs 2001）に由来しますが、筆者はその原典を確認できていません。 二次的な資料からの引用であることを、お断りしておきます。

どの処理系にも載せられる

miz3 の論文で、Wiedijk はこう述べています。

This possibility of transforming proofs in this way does not depend on anything specific to HOL Light.

Any procedural system that has goals and tactics can have a miz3-like layer on top of it, and proofs can be converted to it in exactly the same way.

（筆者による日本語訳）

このように証明を変換できる可能性は、HOL Light 固有のものに依存しない。

目標とタクティクを持つ手続き的なシステムであれば、どれでもその上に miz3 のような層を載せることができ、証明はまったく同じやり方でそれに変換できる。

出典
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年

技術的には、どの処理系にも宣言的スタイルを載せることが可能と考えられます。

2026年、Lean 4 へ

最も新しい移植は、2026年のものです。

Lisar という名前のライブラリが、Isabelle の Isar を Lean 4 に持ち込みました。

ここで、正確に述べておきます。

Lean 4 そのものに Isar という言語があるわけではありません。

Lisar は、Lean 4 の上で Isar 型の書き方を実現するライブラリです。

冒頭の対話篇で扱った「言語と処理系の区別」を、思い出してください。

miz3 が HOL Light に、C-zar が Rocq に載せられたのと同じ関係です。

出典:nomeata/lean-lisar

Lisar is a Lean 4 library that brings the high-level shape of Isabelle/Isar to Lean, enabling declarative, human-readable proof text.

It is implemented purely with Lean's metaprogramming facilities — no compiler patches, no forks, just a library you import.

（筆者による日本語訳）

Lisar は、Isabelle/Isar の高水準の形を Lean にもたらす Lean 4 のライブラリである。

宣言的で人間が読める証明のテキストを実現する。

Lean のメタプログラミングの機能だけで実装されており、コンパイラへのパッチもフォークも要らず、import するだけの普通のライブラリである。

出典:
同上

calc、also、moreover の連鎖も実装されています。

そして、このリポジトリには重要な但し書きがあります。

これはAI が書いた概念実証であり、維持されるライブラリではない、と明記されています。

この点については、第12部 で改めて扱います。

---

第１０部 ── 定着したものと、しなかったもの

30年で10種類以上。

では、そのうち、いくつが広く使われているでしょうか。

答え:一つだけ

miz3 の論文に、次の一節があります。

There already are various declarative proof languages which have been grafted on top of a procedural system.

Currently Isabelle/Isar is the only one that knows widespread use.

（筆者による日本語訳）

手続き的なシステムの上に接ぎ木された宣言的な証明言語は、すでにいくつも存在する。

現在、広く使われていると言えるのは Isabelle/Isar だけである。

出典:
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年

この一文の重みは、書き手が誰かを知ると変わります。

Wiedijk は、Mizar-light と miz3 の作者です。
つまり、自分が作ったものも含めて、広くは使われていないと認めているわけです。

もう一人の証言

C-zar を作った Corbineau も、同じことを書いています。

The new declarative language is now widely distributed, though not yet widely used, and we hope that this paper will help new users to discover our language.

（筆者による日本語訳）

この新しい宣言的言語は、いまや広く配布されているが、まだ広くは使われていない。

本論文が、新しい利用者に我々の言語を見つけてもらう助けになることを願っている。

出典
Pierre Corbineau, "A Declarative Language for the Coq Proof Assistant", TYPES 2007, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年

なお、C-zar は Coq の公式リリース（バージョン8.1）に含まれました。

配布はされていたのです。
それでも、使われませんでした。

２人の作者が、４年の間隔をおいて、同じことを述べています。

miz3 の作者自身による位置づけ

Wiedijk は、miz3 についてもこう書いています。

The miz3 interface is both a prototype (in the sense that it has no real users yet) as well as a quite usable system (in the sense that it is a quite usable proof language for the quite usable HOL Light system).

（筆者による日本語訳）

miz3 のインタフェースは、試作品であると同時に（まだ実際の利用者がいないという意味で）、かなり使えるシステムでもある（かなり使える HOL Light システムのための、かなり使える証明言語であるという意味で）。

出典:
Freek Wiedijk, 同上

「まだ実際の利用者がいない」。

開発には、約2,000行の OCaml と、３人月がかかりました。

ちなみに、HOL Light本体は、約30,000行です。

なぜ、Isar だけが定着したのか

筆者は、決定的な理由を示す資料を見つけられませんでした。

ただし、いくつかの違いは指摘できます。

第１に、Isar は Isabelle の標準の書き方として位置づけられました。

対話篇で見たとおり、miz3 と C-zar は後から載せた拡張です。
利用者は、それを選んで導入する必要があります。

Isar は、Isabelle を使えば最初からそこにあります。

第２に、Isar には強力な自動化が組み合わされました。

Isabelle には sledgehammer という仕組みがあり、証明の細部を自動で探してくれます。
宣言的スタイルで骨格を書き、細部は自動化に任せる、という分担が成立 します。

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

• 依存型を使わないIsabelle/HOL とは何か

本記事でも、必要な範囲で触れます。

第３に、Archive of Formal Proofs が Isar を推奨しました。

Archive of Formal Proofs は、Isabelle の証明を収める査読つきのアーカイブです。

その投稿の案内には、apply スタイルよりも構造化された Isar の証明を好むが、義務とはしないという趣旨の記述 があります。

長く保守されるアーカイブが、その書き方を推奨した。 これは大きいでしょう。

それでも、タクティクが選ばれる理由

ここまで、宣言的スタイルの利点 を述べてきました。

その一方で、なぜ、多くの書き手がタクティクを選び続けるのか。

その理由を、利点する側の立場から考えてみたいと思います。

① 証明が長くなる

Wiedijk が、実験の結果を述べています。

We experimented quite a bit by comparing procedural proofs to their declarative counterparts, and our impression is that declarative proofs are generally about twice as long as corresponding procedural ones.

（筆者による日本語訳）

我々は手続き的な証明とその宣言的な対応物を比較する実験をかなり行ったが、我々の印象では、宣言的な証明は一般に、対応する手続き的な証明の約２倍の長さになる。

出典:
Freek Wiedijk, 同上

実例を見てください。

「$1$ から $n$ までの和は $\dfrac{n(n+1)}{2}$ である」という定理です。

HOL Light のタクティクスタイル:

let ARITHMETIC_SUM = prove
 (`!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2`,
  INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;

３行です。

同じ定理を miz3 の宣言的スタイル で書くと、13行になります。

Wiedijk 自身の評価:

This proof is thirteen lines instead of the three that we got with the traditional proof style. I.e., this proof is quite a bit longer, but not unreasonably so.

（筆者による日本語訳）

この証明は、伝統的な証明スタイルで得た３行ではなく、13行である。
つまり、この証明はかなり長いが、法外というほどではない。

出典:
同上

② 中間の主張を、すべて自分で書かなければならない

Wiedijk は、手続き的スタイルの利点 も明記しています。

The advantage of the procedural style is that one does not need to write all intermediate statements: these are generated automatically.

Also, procedural systems tend to have much stronger automation, with often many different decision procedures that without human help can perform proofs in specific domains.

（筆者による日本語訳）

手続き的スタイルの利点は、中間のすべての主張を書く必要がないことである。
それらは自動的に生成される。

また、手続き的なシステムは、はるかに強力な自動化を持つ傾向があり、人の助けなしに特定の領域の証明を実行できる決定手続きを多く備えていることが多い。

出典:
同上

タクティク を打つと、次に何を証明すべきかを、処理系が計算して画面に表示してくれます。

宣言的スタイル では、それを人間が、自分で考えて（ひらめいて）書かなければなりません。

③ 道筋が見えていない段階では、書き始められない

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

タクティクなら、試しながら探せます。
一つ打ってみて、何が残るかを見る。場合分けの形を確かめる。

宣言的スタイルで書くには、「何を仮定し、何を示すのか」を先に決めておく必要 があります。

④ 読みやすいと分かっていても、書き手はタクティクへ流れる

この点を、そのまま書き記した研究があります。

Lean 4 で大規模な形式化を行った研究者たちの報告です。

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.

（筆者による日本語訳）

とりわけ、単純な calc の段階に整理された計算の証明は、更新や書き直しの際にはるかに修正しやすいはずだと我々は考えている。

しかし、我々の証明のほとんどは、代わりにタクティクモードで一段ずつ書かれた。

calc の証明のほうが読みやすいことも確かで、全体としてはそちらのほうが、計算の証明のより良い組み立て方に思える。

唯一の欠点は、形式的な証明を作り上げる過程にある。
タクティクの状態を操作しながら進めるほうが、楽に感じられるのだ。

出典:
Virasoro 代数と Sugawara 構成の Lean 4 による形式化についての論文, arXiv:2510.21741, 2025年

「読みやすいと分かっていても、書きやすさに流れてしまう。」

この研究者たちは、その緊張関係を認めたうえで、コミュニティもこの問題を認識しているようだと続けています。

⑤ 学習の負担

宣言的スタイル には、独自の語彙があります。

assume、have、show、thus、hence、obtain、also、finally、moreover、ultimately。

第２部で見たとおり、Isabelle には事実を渡す構文だけで11種類あります。

これらを覚え、使い分ける必要があります。

実務での使い分け

では、書き手はどうしているのか。

素数定理 という、数論の重要な定理を形式化した研究者たちが、次のように報告しています。

We found Isar extremely useful in structuring complex proofs, while for filling in low-level inferences we typically relied on tactic applications.

（筆者による日本語訳）

Isar は複雑な証明を構造化するのに極めて有用であることが分かった。
一方、低水準の推論を埋めるには、典型的にはタクティクの適用に頼った。

出典:
"A formally verified proof of the prime number theorem"

大きな構造は宣言的スタイル、細部はタクティク。

これが、実務での使い分けです。

そして、多くの書き手が採っている方法は、次のものです。

タクティクで探し、宣言的スタイルで残す。

探索の段階ではタクティクが向き、保守の段階では宣言的スタイルが向いているようです。

第１１部 ── 長い証明での差

前の部で、「宣言的スタイルは約２倍の長さになる」という数値を見ました。

しかし、それは短い証明での話です。

証明が長くなると、何が変わるのでしょうか。

ラグランジュの定理での比較

Wiedijk は、群論のラグランジュの定理を、複数の方法で形式化して比較しました。

ラグランジュの定理とは、「群の部分群の大きさは、必ずもとの群の大きさを割り切る」という定理です。

用語を説明します。

群とは、要素どうしを組み合わせる演算が定められた集合のことです。整数の足し算、あるいは図形の回転などが、その例にあたります。

部分群とは、その一部を取り出したもので、それ自体も群になっているものです。

そして「大きさ」とは、要素の個数のことです。

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

ある群の要素が12個あるとき、その部分群の要素の個数は、1、2、3、4、6、12 のいずれかにしかなりません。

5個や7個の部分群は、存在しないのです。

抽象代数学の基本的な結果とされています。

行数の比較が、次のとおりです。

形式化の方法	行数
伝統的な HOL Light（John Harrison による）	214行
Mizar の形式的証明の素描	25行
Mizar	153行
miz3 の形式的証明の素描	23行
miz3	183行
miz3（Harrison の証明から自動変換）	1,317行
miz3（Harrison の証明を手で追って書いたもの）	198行

出典
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年, 22頁

Wiedijk 自身の評価:

It is clear that the two hand-written miz3 formalizations are of a similar size to the HOL Light and Mizar formalizations, which shows that using miz3 did not lead to much larger proof texts.

（筆者による日本語訳）

手で書かれた２つの miz3 の形式化は、HOL Light と Mizar の形式化と同程度の大きさである。

これは miz3 を使っても、証明のテキストがそれほど大きくならなかったことを示している。**

出典:
同上

この表から読み取れること

３点あります。

① 長い証明では、行数の差が縮まる

短い証明では、３行が13行になりました。約４倍です。

しかし、ラグランジュの定理では、214行が183行から198行になっています。
むしろ短くなっているか、ほぼ同じです。

証明が長くなるほど、宣言的スタイルの不利は小さくなります。

② 自動変換すると、6倍以上に膨らむ

注目していただきたいのが、1,317行という数字です。

これは、Harrison が書いたタクティクスタイルの証明を、機械的に miz3 へ変換したものです。

同じ証明を、人が手で書き直すと198行でした。

約6.7倍の差があります。

Wiedijk 自身が、その理由を述べています。

この証明には等式についての推論が多く含まれており、変換器がその型を最適化していないためだ、と。

機械が変換したものと、人が書いたものは、別物になります。

③ 骨格だけなら、23行

最も注目していただきたいのが、この数字です。

完全な証明が183行に対して、その８分の１以下です。

形式的証明の素描とは何か

「形式的証明の素描」（formal proof sketch） と呼ばれるものがあります。

証明の骨格だけを書き、細部の正当化を省いたもの です。

実際のコードを見てください。

now let a be A; assume a IN G; let b be A; assume b IN G;
  assume i(a)**b IN H;
  b***H = a**i(a)**b***H; .= a***(i(a)**b***H); thus .= a***H;
!a b. a IN G /\ b IN G /\ ~(a***H = b***H) ==> a***H INTER b***H = {}
proof let a be A; assume a IN G; let b be A; assume b IN G;
  now assume (a***H INTER b***H = {});
    consider g1 g2 such that g1 IN H /\ g2 IN H /\ a**g1 = b**g2;
    g1**i(g2) = i(a)**b;
    i(a)**b IN H;
    thus a***H = b***H;
  end;
qed;
!a. a IN G ==> a IN a***H proof let a be A; assume a IN G; a**e = a; qed;
{a***H | a IN G} PARTITIONS G;
!a b. a IN G /\ b IN G ==> CARD (a***H) = CARD (b***H)
proof let a be A; assume a IN G; let b be A; assume b IN G;
  consider f such that !g. g IN H ==> f(a**g) = b**g;
  bijection f (a***H) (b***H);
qed;
set INDEX = CARD {a***H | a IN G};
set N = CARD G; set n = CARD H; set j = INDEX; N = j*n;
thus CARD H divides CARD G;

出典:
同上、21頁

証明の筋道が、すべて書かれています。

「$a$ を $G$ の要素とする」
「$a \times H$ と $b \times H$ が交わらないと仮定する」
「そのような $g_1$ と $g_2$ を取る」「よって a×H = b×H である」。

書かれていないのは、各段階の正当化だけです。
どの定理を使ってその段階が正しいと言えるのか、という部分です。

なぜ、骨格だけ書けるのか

この書き方が可能なのは、処理系が「正当化が足りない」場合にエラーではなく警告を出すから です。

C-zar の論文に、次の記述があります。

If a justification fails, the proof assistant issues a warning Warning: insufficient justification. rather than an error.

This allows the user to write proofs from the outside in by filling the gaps, rather than linearly from start to end.

（筆者による日本語訳）

**もし正当化が失敗した場合、証明支援系はエラーではなく警告を出す。

「警告:正当化が不十分である」と。これによって利用者は、最初から順に書くのではなく、外側から内側へ、隙間を埋めていく形で証明を書ける。**

出典:
Pierre Corbineau, "A Declarative Language for the Coq Proof Assistant", TYPES 2007, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年, 74頁

同じ論文には、CoqIDE という環境では、その警告が橙色の背景で強調されるとも書かれています。
どこにまだ作業が必要なのかが、一目で分かるということです。

この部の結論

短い証明では、宣言的スタイルは割に合わないように見えます。 ３行が13行になるのですから。

しかし、証明が長くなるほど、その差は縮まります。
214行が183行になるように。

そして、骨格だけを書くなら、わずか23行です。

この「骨格だけ書く」という使い方が、次の話につながります。

第１２部 ── AI が証明を書く時代の、宣言的スタイル

2022年以降、大規模言語モデル（LLM）に証明を書かせる研究が、急速に増えました。

この部では、そこで 宣言的スタイル が果たしている役割を見ます。

まず、言葉を区別する

LLM が出力するものについて、区別が要ります。

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

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

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

この区別を持たないと、以降の話が曖昧になります。

骨格を書いて、隙間を埋める

LLM に証明を書かせる研究 で、最も広く使われている手法があります。

次の３段階です。

1. LLM が、自然言語で証明の下書きを書く
2. その下書きを、宣言的スタイルの骨格へ変換する
3. 残った隙間を、自動証明の仕組みが埋める

この手法を最初に示したのが、2023年のICLRに採択された以下の論文です。

出典: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）

題名がそのまま手法を表しています。
「下書きし、素描し、証明する」

【重要】この手法は、1997年に提案されていた

同じ論文の付録に、次の記述があります。

Interactive theorem provers such as Isabelle and Mizar use a declarative proof style (Syme, 1997), in which a proof is interleaved with conjectures and their corresponding proofs.

Syme (1997) stated that the list of conjectures in a declarative proof should be analogous to a proof sketch found in a mathematical textbook and sufficiently convincing for the reader.

（筆者による日本語訳）

Isabelle や Mizar のような対話型定理証明系は、宣言的な証明スタイル（Syme, 1997）を使う。

そこでは証明が、予想とそれに対応する証明とで織り合わされる。

Syme（1997）は、宣言的な証明における予想の一覧は、数学の教科書に見られる証明の素描と類似したものであるべきで、読者を十分に納得させるものであるべきだと述べた。

出典:
同上、付録A

続けて、こうあります。

In practice, ITP users often prove a theorem by writing down a list of conjectures (a "formal sketch"), then attempt to find a proof of each conjecture (fill a "gap") with an automated system.

（筆者による日本語訳）

実際には、対話型定理証明系の利用者は、予想の一覧（「形式的な素描」）を書き下ろし、次に各予想の証明を自動のシステムで見つける（「隙間を埋める」）ことによって、定理を証明することが多い。

出典:
同上

LLM に証明を書かせる2022年の研究が、その手法の根拠として1997年の論文を引用しています。

「骨格を書いて、隙間を自動で埋める」という手法は、LLM のために考案されたものではありませんでした。

1997年に、人間が証明を書くための手法として提案されていたのです。

そして、その手法は、LLMにとっても適している手法だったのです。

1997年の Declare

その1997年の仕事を見てみます。

Don Syme という研究者が、Declare という定理証明支援系* を作りました。

書誌情報:

• Don Syme, "DECLARE: A prototype declarative proof system for higher order logic", Technical Report 416, University of Cambridge Computer Laboratory, 1997年
   
• Don Syme, "Three Tactic Theorem Proving", Bertot・Dowek・Théry・Hirschowitz・Paulin 編 Theorem Proving in Higher Order Logics（TPHOLs 1999）, Lecture Notes in Computer Science 第1690巻, Springer, 203〜220頁, 1999年

論文の題名に注目してください。

"Three Tactic Theorem Proving" ── **「３つのタクティクによる定理証明」**です。

要旨には、こうあります。

We take a somewhat radical approach to proof description: proofs are not described with tactics but by using just three expressive outlining constructs.

The language is "declarative" because each step specifies its logical consequences, i.e. the constants and formulae that are introduced, independently of the justification of that step.

（筆者による日本語訳）

我々は証明の記述に、いくぶん急進的な手法を採る。

証明はタクティクによってではなく、わずか３つの表現力のあるアウトラインの構成子だけを使って記述される。>

この言語が「宣言的」であるのは、各段階が、その段階の正当化とは独立に、論理的な帰結、すなわち導入される定数と論理式を明示するからである。**

出典:
Don Syme, "Three Tactic Theorem Proving", 同上

わずか３つの構成子。

そして、細部は自動証明の仕組みに任せる。

The style is also heavily "inferential", because Declare relies on an automated prover to eliminate much of the detail normally made explicit in tactic proofs.

（筆者による日本語訳）

このスタイルはまた、大いに「推論的」でもある。

というのも、Declare は、タクティクによる証明では通常明示される詳細の多くを取り除くために、自動証明器に依存するからである。

出典:
同上

なお、Don Syme はこの後、定理証明の分野を離れます。

1998年にマイクロソフトへ移り、C# のジェネリクスを設計し、そして F# という関数型プログラミング言語を作りました。

F# の書籍の著者紹介には、こうあります。

Don Syme is a principal researcher at Microsoft Research and is the main designer of F#.

He received a Ph.D. from the University of Cambridge Computer Laboratory in 1999.

（筆者による日本語訳）

ドン・サイムはマイクロソフト研究所の主任研究員であり、F# の主たる設計者である。
1999年にケンブリッジ大学計算機研究所で博士号を取得した。

出典:
Expert F# 4.0（Apress）の著者紹介

【注意】F# と F* は、まったく別の言語です。

• F#（エフシャープ）── Don Syme が設計した、.NET 上の関数型プログラミング言語
   
• F*（エフスター）── マイクロソフト研究所と INRIA が開発した、検証のための言語

後者については、筆者が以前に記事を書いています。

• F* とは何か

1999年という年

もう一つ、記しておきたいことがあります。

1999年の TPHOLs という国際会議の論文集に、宣言的スタイル の論文が３本、連続して掲載されています。

著者	論文	頁
Markus Wenzel	"Isar — A Generic Interpretative Approach to Readable Formal Proof Documents"	167〜184頁
Vincent Zammit	"On the Implementation of an Extensible Declarative Proof Language"	185〜202頁
Don Syme	"Three Tactic Theorem Proving"	203〜220頁

出典:
Lecture Notes in Computer Science 第1690巻, Springer, 1999年

Isar が発表されたのも、この会議 です。

そして、Wenzel は Isar の論文の中で、Syme の Declare をこう評価しています。

Several attempts have been undertaken to transfer ideas of Mizar into the established tradition of tactical theorem proving, while trying to avoid its well-known shortcomings. The DECLARE system has been probably the most elaborate, so far. Our approach, which is called Intelligible semi-automated reasoning (Isar), can be best understood in that tradition, too.

筆者による日本語訳:

Mizar のアイデアを、タクティクによる定理証明の確立された伝統へ移すという試みが、これまで何度か行われてきた。

その周知の欠点を避けようとしながらである。DECLARE が、これまでで最も精緻なものであろう。

私たちの手法、Intelligible semi-automated reasoning（Isar）と呼ばれるものも、その伝統の中で最もよく理解される。

出典:
Markus Wenzel, "Isar — A Generic Interpretative Approach to Readable Formal Proof Documents", TPHOLs'99, Lecture Notes in Computer Science 第1690巻, Springer, 167〜184頁, 1999年

Isar の名前は、"Intelligible semi-automated reasoning"（理解できる半自動の推論）の頭字語 です。

なお、Isabelle の公式サイトにも、Mizar との関係が明記されています。

Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings: it is based on a few basic principles only, it is quite independent of the underlying logic, and integrates a broad range of automated proof methods.

（筆者による日本語訳）

既存の宣言的な定理証明システム（Mizar など）と比較して、Isar はいくつかの欠点を避けている。それはごく少数の基本原理のみに基づいており、下にある論理からかなり独立しており、幅広い自動証明の手法を統合している。

出典:
Isabelle 公式サイト「Isar」

2025年、同じ問題が再び論じられる

さて、ここからが本題です。

2025年、Isar を機械学習のために再設計する研究 が発表されました。

その論文が指摘する問題を、もう一度見てください。

There are at least three problems: the abundance of expert-oriented features, extensive syntactic redundancy, and the substantial demand for proof automation in declarative proofs.

筆者による日本語訳:

問題は少なくとも３つある。
専門家向けの機能の過多、広範な構文の冗長性、そして宣言的な証明における証明自動化への実質的な要求である。

出典:"A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL", 2025年

この研究が提案する新しい言語の名前は、MiniLang（最小の言語） です。

そして、この研究の動機は、機械学習にあります。 LLM が学習しやすい形式を作る、ということです。

【この記事の見せ場】1997年と2025年で、同じ設計が目指されている

ここで、３つを並べてみてください。

	Declare（1997〜1999年）	Isar（1999年〜）	MiniLang（2025年）
構文の数	３つの構成子	多数（事実を渡す構文だけで11種類）	削減を目指す
設計の動機	証明を読みやすくする	証明を読みやすくする	機械学習のために
自動化への依存	強い（細部は自動証明器へ）	強い（sledgehammer）	設計として組み込む

Syme が1997年に採った「構文を極限まで減らす」という設計を、
MiniLang が2025年に、別の動機から再発見 しています。

そして、Isar はその中間にあります。

Wenzel は Syme の Declare を「これまでで最も精緻なもの」と評価しながら、より多くの構文を持つ言語を作りました。

その冗長性を、ポールソンらは 「人間にも機械にも理解可能にするもの」 と呼び、MiniLang の論文は「問題」と呼んでいます。

第４部で見たとおりです。

自然言語に近づける試み

もう一つ、別の方向の試みがあります。

Isabelle/Naproche という系統です。

これは、自然言語により近い入力を受け付ける証明支援系です。

ForTheL という言語で書かれ、素数の無限性の証明などがチュートリアル に含まれています。

Wiedijk 自身が、宣言的スタイルの限界 について、次のように書いています。

Actually, the Mizar and Isar languages, as well as the language described in this paper, are not very much like natural language.

The ForTheL language for the SAD system is much better in this respect.

筆者による日本語訳

実のところ、Mizar と Isar の言語、そして本論文で述べる言語は、自然言語にそれほど似てはいない。

SAD システムの ForTheL 言語のほうが、この点でははるかに優れている。

出典:
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年

「宣言的スタイルは読みやすい」と述べてきましたが、それは「タクティクと比べれば」という話です。

自然言語そのものと比べれば、まだ隔たりがあります。

Naproche とは何か

Naproche は、Natural Proof Checking の略です。

直訳すれば、「自然な証明の検査」 となります。

開発したのは、ドイツのボン大学の数学研究所 です。

そして、この処理系は Isabelle に 同梱 されています。

Isabelle を導入すれば、Naproche も一緒に入ります。

拡張子が .ftl または .ftl.tex のファイルを Isabelle/jEdit で開けば、自動的に Naproche による検査が始まります。

入力に使う言語が、ForTheL です。

Formula Theory Language の略で、日常の数学の文章に近い形で読めることを目指しています。

公式の資料 には、次の記述があります。

The Naproche system (for Natural Proof Checking) checks the logical correctness of texts written in an input language ForTheL (for Formula Theory Language) which ideally reads like common mathematical language.

Proofs and proof structures should resemble the style of undergraduate textbooks.

（筆者による日本語訳）

**Naproche（Natural Proof Checking の略）は、ForTheL（Formula Theory Language の略）という入力言語で書かれた文章の、論理的な正しさを検査する。

ForTheL は、理想的には日常の数学の言語のように読めることを目指している。

証明とその構造は、学部生向けの教科書のスタイルに似たものであるべきである。**

出典:
Peter Koepke, Mateusz Marcol, Patrick Schäfer（ボン大学 数学研究所）, "Formalizing Sets and Numbers, and some of Wiedijk's '100 Theorems' in Naproche", 2023年9月1日, 3頁

実際のコードを見てください

ユークリッドによる素数無限性の証明 を、ForTheL で書いたものです。

証明する定理:「素数は無限に存在する」

Signature. P is the collection of prime natural numbers.

Theorem (Euclid). P is infinite.

Proof by contradiction. Assume that P is finite. Take a natural number r
such that {1, ... , r} and P are equinumerous. Take a bijection p between
{1, ... , r} and P. p is a sequence of length r and P = {p1, ... , pr}.

(1) pi is a nonzero natural number for every i ∈ dom(p).

Consider n = p1 ··· pr + 1. p1 ··· pr is nonzero and n is nontrivial.
Take a prime divisor q of n.

(2) q ∉ {p1, ... , pr}.

Proof by contradiction. Take a natural number i such that 1 ≤ i ≤ r and
q = pi. q is a divisor of n. i ∈ dom(p). pi is a divisor of p1 ··· pr (by
Factorproperty, 1). Thus q divides 1. Contradiction. qed.

出典:同上、37〜38頁。このコードを書いたのは、Peter Koepke です。

このコードの読み方

まず、気づいていただきたいことがあります。

上のコードは、そのまま英語の文章として読むことができます。

日本語にすると、こうなります。

定義:P を、素数である自然数を集めたものとする。

定理（ユークリッド）:P は無限である。

背理法による証明。P が有限であると仮定する。{1, ... , r} と P が同じ個数になるような自然数 r を取る。{1, ... , r} と P のあいだの全単射 p を取る。p は長さ r の列であり、P = {p1, ... , pr} である。

(1) dom(p) のすべての i について、pi は0でない自然数である。

n = p1 × ... × pr + 1 と置く。p1 × ... × pr は0ではなく、n は0でも1でもない。n の素因数 q を取る。

(2) q は {p1, ... , pr} に属さない。

背理法による証明。1 ≤ i ≤ r かつ q = pi となる自然数 i を取る。q は n の約数である。i は dom(p) に属する。pi は p1 × ... × pr の約数である（因数の性質と (1) による）。よって q は 1 を割り切る。矛盾。証明終わり。

訳文に出てくる語を、２つ説明します。

全単射とは、２つの集合のあいだで、要素を一対一に対応させる写像のことです。「同じ個数である」ことを示すために使われます。

背理法とは、示したいことの逆を仮定し、そこから矛盾を導く手法です。矛盾が出れば、その仮定が誤りだったと分かります。

証明の筋道は、次のとおりです。

素数が有限個しかないと仮定します。 すると、それらをすべて並べられます。

次に、それらをすべて掛け合わせて、$1$ を足します。 これを $n$ とします。

$n$ には素因数があるはずです。 ところが、その素因数は、最初に並べた素数のどれとも違います。

なぜなら、最初に並べたどの素数も、$n$ を割ると$1$余るからです。

これは、「素数をすべて並べた」という仮定と矛盾します。

よって、素数は無限に存在します。

名前の区別

P、r、p、n、q、i は、プログラマが任意に付けた名前です。
別の名前でも動きます。

Signature、Theorem、Proof、Assume、Take、Consider、Thus、Contradiction、qed は、ForTheL の予約語です。

Factorproperty は、この文書の中で先に定義された公理の名前です。

Isar や Mizar と比べてください

第８部で見た Mizar のコードを思い出してください。

assume sqrt 2 is rational;
then consider i being Integer, n being Nat such that
W1: n<>0 and

Mizar も英語に近い形でしたが、W1: のような通し番号や、being という独特の語法がありました。

ForTheL では、そうした記号がほとんど現れません。

Take a natural number r such that ...（〜であるような自然数 r を取る）
Assume that P is finite.（P が有限であると仮定する）

これらは、数学の教科書に出てくる英語の文章そのものです。

そして、この違いは見た目だけではありません。

同じ資料は、ForTheL のファイルが LaTeX の方言としても書けること を述べています。

つまり、同じファイルを、証明の検査にかけることも、組版して PDF の論文として出力することもできます。

先ほど示したコードも、実は組版されたPDFから取ったもの です。

ただし、限界もあります

同じ資料には、正直な記述もあります。

約3000行のこの文書を検査するのに、「中程度の性能をもつ一般向けのノートパソコンで約30分」かかったとされています。

さらに、検査が失敗することもあると書かれています。

外部の自動証明器が制限時間内に答えを見つけられない場合があるためです。

その場合は、制限時間を延ばすか、証明の段階をさらに細かく書き足す必要があります。

読みやすさを追求すると、機械が埋めるべき隙間が大きくなります。

その隙間を埋める作業に、時間がかかるのです。

ここにも、本記事で繰り返し見てきた緊張関係があります。

2026年、AI が移植を書いた

そして、最後の話です。

第９部で触れた Lisar について、詳しく見ます。

何が作られたのか

Lisar は、Isabelle の Isar を Lean 4 に持ち込むライブラリです。

具体的に、次のものが実装されています。

第１に、Isar の語彙が、そのまま Lean 4 で使える ようになりました。

fix（変数を固定する）、assume（仮定する）、have（〜が成り立つ）、show（示す）、thus（よって）、hence（ゆえに）、obtain（存在するものを取り出す）、also と finally（等式の連鎖）、moreover と ultimately（事実を集める）、note、presume、case、next。

本記事の第２部と第５部で見た語が、ほぼすべて揃っています。

第２に、proof … qed というブロックの構文が作られました。

Lean 4 では、証明を書くとき by と書いて タクティクモード に入ります。

Lisar では、その代わりに proof と書くと、Isar の書き方 でその証明を書けます。

第３に、専用の表示画面が作られました。

本記事の冒頭で、Lean 4 の Infoview を紹介しました。

⊢ の前に文脈、後に示すべきことが表示される画面です。

Lisar は、その代わりに Isar 専用の表示 を出します。

fix（固定した変数）、facts（手元にある事実）、this（直前に示したこと）、?thesis（いま示すべきこと）が、それぞれ区別されて並びます。

第４に、Isar の設計の核心が再現されました。

これが最も重要な点です。

Isar では、have で示した事実は、目標の文脈に自動では入りません。
使いたければ、from や then で明示的に引き渡す必要があります。

この仕組みを、Lisar は忠実に再現しています。 リポジトリの説明には、次のようにあります。

This is the central design choice of Isar — and the central design choice of Lisar.

筆者による日本語訳:

これは Isar の中心にある設計上の選択であり、Lisar の中心にある設計上の選択でもある。

出典:nomeata/lean-lisar

第５に、動く例が７つ用意されました。

そのうち２つは、本記事で扱った定理です。

• $\sqrt{2}$ が無理数であること（LisarExamples/Sqrt2Irrational.lean）
• ドリンカーの原理（LisarExamples/Drinker.lean）

いずれも、Isabelle の例を Lean 4 へ移植したものです。

第６に、テストも書かれました。

通常の機能テストに加え、実際に Lean のサーバを起動して、表示画面が正しく出るかを確かめる試験まで含まれています。

実際のコード

リポジトリに掲載されている、最初の例です。

import Lisar

example : ∀ n : Nat, 0 ≤ n → n + 0 = n := proof
  fix n
  assume hpos : 0 ≤ n
  have hzero : n + 0 = n := Nat.add_zero n
  thus ?thesis := hzero
qed

出典:
同上

証明しているのは、「すべての自然数 $n$ について、$n$ が$0$以上ならば、$n$ に$0$を足しても $n$ のままである」という主張です。

読んでみてください。

• fix n ── 「n を固定する」
• assume hpos : 0 ≤ n ── 「n は0以上であると仮定する。それを hpos と呼ぶ」
• have hzero : n + 0 = n := Nat.add_zero n ── 「n + 0 = n が成り立つ。根拠は Nat.add_zero という定理である」
• thus ?thesis := hzero ── 「よって、示すべきことが hzero によって示された」

これは Lean 4 のコードです。
しかし、Isabelle の Isar とほとんど同じ形をしています。

fix、assume、have、thus、?thesis、proof、qed は、Lisar が用意した語です。
n、hpos、hzero は、プログラマが任意に付けた名前です。
Nat.add_zero は、Lean のライブラリにある定理の名前です。

なぜ、これが驚くべきことか

Lisar は、Lean 4 のコンパイラを一切改造していません。

リポジトリには、次のようにあります。

It is implemented entirely with Lean's metaprogramming facilities: no compiler patch, no fork, just an ordinary library you can import.

（筆者による日本語訳）

これは Lean のメタプログラミングの機能だけで実装されている。
コンパイラへのパッチもなく、フォークもなく、import するだけの普通のライブラリである。

出典:
同上

つまり、Lean 4 という言語が持つ拡張の仕組みだけで、別の言語の書き方を丸ごと持ち込めたということ です。

第９部で見た Mizar-light が41行だったことを、思い出してください。

宣言的スタイルを載せるのに、処理系の内部を書き換える必要はありません。

そして、これを書いたのは AI でした

このリポジトリには、次の但し書きがあります。

This repository is an AI-authored proof of concept.

（筆者による日本語訳）

このリポジトリは、AI が書いた概念実証である。

出典:
同上

リポジトリには INITIAL_PROMPT.md というファイルが置かれています。

AIに与えた最初の指示が、記録として残されている のです。

そして、次の記述が続きます。

It is not a maintained library.
Adapting Isar's philosophy to Lean's idioms — deciding which Isar mechanisms have natural Lean analogues, which should be reshaped, and which should be left out — is a real design problem that needs sustained human judgement, not a code-generation pass.

The leaves of this implementation reflect a single AI session's choices; many of them deserve to be revisited with a clearer view of how Lean users actually want to write proofs.

（筆者による日本語訳）

**これは、維持されるライブラリではない。

Isar の哲学を Lean の流儀へ適応させること、すなわち、どの Isar の機構に自然な Lean の対応物があり、どれを作り直すべきで、どれを省くべきかを決めることは、持続的な人間の判断を要する本物の設計問題であって、コード生成を一度走らせて済むものではない。

この実装の末端は、たった一度の AI との対話における選択を反映したものである。

その多くは、Lean の利用者が実際にどう証明を書きたいのかを、より明確に見据えたうえで、あらためて考え直されるべきものである。**

出典:
同上

何ができて、何ができなかったのか

この但し書きは、AIが何をできて、何をできなかったのかを、正確に示しています。

できたこと ── 動くものを作ることです。30種類を超える構文を実装し、専用の表示画面を作り、テストを書き、７つの例を動かしました。

できなかったこと ── 設計の判断です。

Isar には多くの機構があります。 そのうち、Lean 4 に自然に馴染むものはどれか。作り直すべきものはどれか。省くべきものはどれか。

この判断は、「Lean の利用者が実際にどう証明を書きたいのか」を知らなければできません。

そして、それは一度のコード生成では得られないものです。

リポジトリは、こう締めくくられています。

If structured proofs in Lean appeal to you and you'd like to take this further, the project is an open invitation.

（筆者による日本語訳）

Lean で構造化された証明を書くことに関心があり、これをさらに進めたいと思われるなら、この計画は開かれた招待状である。

出典:
同上

動くものは AI が作った。しかし、それを本物にするのは人間の仕事として残されている。

読める証明が必要な、もう一つの理由

ここまで、宣言的スタイル の読みやすさについて論じてきました。

その理由は「人間が論証を追えるから」でした。

しかし、もう一つの理由があります。

Wiedijk の論文の冒頭に、脚注として次の記述があります。

There is only one serious possibility for mathematics verified with the best interactive theorem provers to still have problems.

The definitions and statements might not mean what the person who wrote them thinks they mean.

Although it then still is certain that the mathematics contains no errors at all, it is the 'wrong' mathematics.

（筆者による日本語訳）

最良の対話型定理証明系で検証された数学に、なお問題がありうる可能性は、ただ一つである。

定義や主張が、それを書いた人が思っている意味とは違うかもしれない、ということである。

その場合でも、数学に誤りが一切ないことは確かである。しかしそれは「間違った」数学なのである。

出典:
Freek Wiedijk, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年, 脚注1

処理系が保証するのは、書かれた主張に対しての正しさです。

その主張そのものが、証明したかったことと違っていたら、検査を通っても意味がありません。

そして、それを確かめられるのは人間だけです。

assume "even n" と書かれていれば、「$n$ は偶数である」という仮定を置いたことが読み取れます。

タクティクの列には、その情報がありませんでした。

つまり、読める証明が必要なのは、論証を追うためだけではありません。

「そもそも、何を証明しようとしているのか」を確かめるためでもあります。

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

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

そして、AIが形式化を担うようになると、この問題はより深刻になります。
その話は、続編の記事で扱います。

この部の結論

LLM が証明の候補を書く時代になりました。

しかし、その手法とよく似た設計思想が、1997年には既に提案されていました。
骨格を書いて、隙間を自動で埋める。

当時それは、人間が証明を書くための工夫でした。
それが、LLM にも適していたのです。

そして、宣言的スタイルの冗長性 は、読み手によって評価が分かれています。

• 証明を検査する処理系にとっては、確かめるべき情報が明示されているという長所です。
   
• 証明を学習する言語モデルにとっては、学習すべき構文の種類が増えるという短所になりえます。

どちらを重く見るかは、まだ決着していません。

発展的な学習のために ── 専門書ではこう書かれています

本記事では、専門用語をできるだけ日常の言葉で説明してきました。

しかし、専門書や論文を読む際には、正式な用語を知っている必要があります。

対応表を置いておきます。

用語の対応

本記事での書き方	専門書での用語
数学の答案に近い形で、論証を文章として書く方式	宣言的スタイル（declarative style）
タクティクを並べていく書き方	手続き的スタイル（procedural style）
補題の主張だけを並べ、処理系に証明させる方式	誘導自動化スタイル（guided automated style）
証明の組み立てを処理系に指示する命令	タクティク（tactic）
数学者が実際にやっている推論に近い形式体系	自然演繹（natural deduction）
仮定を箱で囲み、その帰結を箱の中に保つ形式	ヤシコフスキ／フィッチ流の自然演繹（Jaśkowski/Fitch-style natural deduction）
木構造で証明を表す形式	ゲンツェン流の自然演繹（Gentzen-style natural deduction）
公理を多く持ち、推論規則が少ない体系	ヒルベルト流（Hilbert-style logic）
論理記号の意味を定める規則	導入規則（introduction rule）と除去規則（elimination rule）
骨格だけを書き、細部の正当化を省いた証明	形式的証明の素描（formal proof sketch）
いま証明すべき主張	命題（thesis／goal）
証明に使えそうな定理を、大量の候補から選び出すこと	前提選択（premise selection）
証明が正しいかを最終判定する部分	カーネル（kernel）
証明そのものを、プログラムの項として書く方式	証明対象型の宣言的スタイル（proof object declarative style）
証明を文章として書く方式	自然言語型の宣言的スタイル（natural language declarative style）
証明と項が対応するという考え方	カリー・ハワード対応（Curry-Howard correspondence）
数学の自然言語を形式化した言語	制御された自然言語（controlled natural language）、数学の俗語（mathematical vernacular）
等式を順に変形していく書き方	計算的推論（calculational reasoning）
型の中に値が入る型	依存型（dependent type）

表現の対応

本記事での書き方	専門書での書き方
各段階が、その正当化とは独立に、何が成り立つのかを述べている	each step specifies its logical consequences, independently of the justification
中間の主張を、すべて自分で書く	中間の statement を明示的に記述する
隙間を埋める	gap を fill する／unjustified step を justify する
証明の骨格	proof skeleton／proof outline
処理系を動かさなくても読める	stand-alone である

---

実際に試すには

本記事を読んで、宣言的スタイルを実際に書いてみたいと思われた方へ。

６つの言語のうち、最も容易に試せるのは Lean 4 です。

理由:ブラウザだけで動かせるからです。

Lean 4 をブラウザで試す

公式の実行環境があります。

• https://live.lean-lang.org/

Mathlib という数学ライブラリを読み込んだ状態で始めるなら、次の URL です。

• https://live.lean-lang.org/?from=mathlib

導入の作業は要りません。 ブラウザで開けば、その場でコードを書いて動かせます。

公式のリポジトリにも、想定される用途が記されています。

Doodling around with Lean before installing it as a newcomer.

筆者による日本語訳:

Lean を導入する前に、新参者が試しに触ってみる。

出典:leanprover-community/lean4web

ただし、同じリポジトリには次の注意もあります。

Currently, serious Lean code development and larger projects are considered out-of-scope.

筆者による日本語訳:

現在のところ、本格的な Lean のコード開発や、より大きな計画は対象外と考えている。

出典:同上

あくまで「試すため」の環境です。

本記事で見た have や calc を、実際に書いてみてください。

各言語の難易度

言語	試す難易度	導線
Lean 4	最も容易	ブラウザで動く実行環境がある
Isabelle	中	導入が必要
Agda	中	導入が必要
Rocq（C-zar）	中〜難	導入が必要。C-zar が現在の Rocq で使えるかは、筆者は確認できていません
Mizar	難	導入が必要
HOL Light（miz3）	最も難しい	miz3 は別途の導入が必要

日本語の学習資料

Lean 4 には、日本語の資料が揃っています。

• lean-ja ── 日本語のコミュニティサイト
• Theorem Proving in Lean 4 日本語訳

Isabelle については、筆者が前記事で日本語資料を集約しています。

• 依存型を使わないIsabelle/HOL とは何か

Mizar については、信州大学が日本語の資料を公開しています。

• Mizar:チュートリアル、ライブラリ検索、各種リソース

Mizar 講義録が、日本語で公開されています。

---

日本語で読める議論

本記事の主題について、日本語で書かれた議論があります。

筆者が調べた範囲では、宣言的スタイルを複数の言語にわたって比較した日本語の記事は見当たりませんでした。 しかし、個別の論点については、すでに論じられています。

檜山正幸さんの記事

• 証明検証系Mizarのジレンマと証明系の村（2016年12月）

この記事には、次の記述があります。

しかしMizarの場合は、言語自体は（証明記述言語の範疇では）癖がなくまっとうで、書くにも読むにも楽なものです。むしろ癖が凄く難読なのは、他の証明系のタクティク言語です。Mizarはもっと世に広まってよいものだと思います。

出典:
同記事

そして、Isar の名前について、興味深い推測が述べられています。

Isabelleの高水準証明記述言語はIsarといいます。公式には "Intelligible semi-automated reasoning" のアクロニムだということですが、おそらくはMizarへのリスペクトが込められているんじゃないかと思います。実際、Isar（の設計者のウェンツェル）はMizarにかなり影響を受けています。

出典:
同記事

名前の由来について、筆者はウェンツェル自身による記述を確認できていません。

しかし、Mizar からの影響については、第12部で引いたとおり、ウェンツェル自身が論文で認めています。

檜山さんは、Isabelle カテゴリで Isar と Mizar の詳細な比較も記録されています。

• 檜山正幸のキマイラ飼育記 メモ編:Isabelle カテゴリ

myuon さんの記事

• Isabelle入門の入門（2014年）

Isar とタクティクの対比が、実例つきで書かれています。

逆に、Isarでの証明では、仮定やすでにわかっている命題からゴールの形になるように証明を書きます。上の方法と違い、証明は必ず一方通行ではなく、例えばex'の証明中では仮定b("2 ≤ Suc n")は2回別の場所で使われています。Mizarみたいな感じです（Mizar使ったことないけど）。

出典:
同記事

• Isabelle/HOLの基本（連載）（2017年）

公式のチュートリアルに沿って、実際に証明を書きながら進む連載です。 第４章で Isar を扱っています。

タクティクの読みにくさをめぐる議論

• 定理証明支援系についての問題意識（mod_poppo さん、2025年）

タクティクの羅列を示して「証明がどのように進んだのかわかりますか」と読者に問いかけ、書籍への掲載や LLM の学習データという観点から論じています。

結論として、Agda・Mizar・Isabelle/Isar は見る価値がありそうだ、と述べられています。

• 証明支援系がダメだった理由と、AIでブーストする理由（檜山正幸さん、2023年）

なぜタクティク方式が主流になったのか、そして Isar と PIDE でウェンツェルが何を変えようとしたのかを論じています。

---

おわりに

本記事で見てきたことを、一文でまとめるなら、こうなります。

宣言的スタイルとは、1934年に人間が証明を書くために設計された形式を、そのまま言語の構文にしたものである。

ヤシコフスキが考えた「箱」の構造が、assume、have、thus という語になりました。

仮定を置き、その帰結を導き、結論を出す。数学の答案で誰もがやっていることが、90年以上前に形式化されていました。

その読みやすさは、30年にわたって10種類以上の処理系へ移植されるだけの価値がありました。

HOL、HOL Light、Coq、Isabelle、そして Lean 4。

しかし、Wiedijk が2012年の論文で「広く使われている」と評したのは、Isabelle の Isar だけでした。

なお、2026年現在について同じ結論が成り立つかどうかは、本記事では利用統計まで調査していません。

読みやすさと、実際に使われることは、別の話でした。

そして2026年、Lean 4 への移植を書いたのは、AI でした。

ただし、そのリポジトリには但し書きがあります。

動くものは作ることができたれ。しかし、何を残し何を捨てるかという設計の判断は、人間の仕事として残っている。

LLM が証明の候補を書く時代に、宣言的スタイルが持つ意味は、まだ決着していません。

冗長性は、証明を検査する処理系にとっては長所であり、証明を学習する言語モデルにとっては障害になりえます。

ただ、一つ確かなことがあります。

LLM が書いた証明の候補を、人間が読んで判断する場面は、これから増えます。

そのとき、指示の列が並んでいるだけのコードと、論証の筋道が文章として書かれたコードでは、判断のしやすさが違います。

1934年に人間のために設計された形式が、いま、別の意味を持ち始めているのです。

---

関連記事

• 依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
   
• Rocq（旧Coq）とLean 4だけでは足りない領域がある ── 形式手法の地図
   
• Rocq（旧名 Coq）とは何か
   
• Cubical Agda とは何か
   
• Lean 4 とは何か
   
• λProlog とは何か
   
• F* とは何か
   
• 形式証明は「仕様が人間の意図を反映しているか」は保証しない
   
• AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう
   
• Python の型ヒントの限界を超える「篩型」入門
   
• 定理証明・形式検証はいまから学ぶ価値があるか

---

出典

宣言的スタイルの分類と、その現況

• Freek Wiedijk（ラドバウド大学ナイメーヘン）, "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", Logical Methods in Computer Science 第8巻第1号:30, 2012年。DOI: 10.2168/LMCS-8(1:30)2012

６言語のコード

• Freek Wiedijk 編, "The Seventeen Provers of the World", Lecture Notes in Artificial Intelligence 第3600巻, Springer, 2006年。序文はダナ・スコット
• Mathlib.Data.Real.Irrational（Lean 4）
• My First Lean 4 Proof: the Irrationality of $\sqrt{2}$, 2026年

C-zar

• Pierre Corbineau（ラドバウド大学ナイメーヘン）, "A Declarative Language for the Coq Proof Assistant", Miculan・Scagnetto・Honsell 編 Types for Proofs and Programs（TYPES 2007）, Lecture Notes in Computer Science 第4941巻, Springer, 69〜84頁, 2008年

Isar

• Markus Wenzel, "Isar — A Generic Interpretative Approach to Readable Formal Proof Documents", TPHOLs'99, Lecture Notes in Computer Science 第1690巻, Springer, 167〜184頁, 1999年
• Isabelle 公式サイト「Isar」

Declare

• Don Syme, "Three Tactic Theorem Proving", TPHOLs 1999, Lecture Notes in Computer Science 第1690巻, Springer, 203〜220頁, 1999年
• Don Syme, "DECLARE: A prototype declarative proof system for higher order logic", Technical Report 416, University of Cambridge Computer Laboratory, 1997年

自然演繹

• Stanford Encyclopedia of Philosophy「Natural Deduction Systems in Logic」
• Internet Encyclopedia of Philosophy「Natural Deduction」
• Gerhard Gentzen, "Untersuchungen über das logische Schließen", Mathematische Zeitschrift 第39巻, 176〜210頁および405〜431頁, 1934年

冗長性をめぐる議論

• 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年
• "A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL", 2025年

AI と定理証明

• Albert Q. Jiang, Sean Welleck, Jin Peng Zhou ほか, "Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs", ICLR 2023
• nomeata/lean-lisar（2026年）
• Virasoro 代数と Sugawara 構成の Lean 4 による形式化, arXiv:2510.21741, 2025年

その他

• Lawrence C. Paulson, ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician, ケンブリッジ大学, 2017年〜
• Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel, "From LCF to Isabelle/HOL", Formal Aspects of Computing 第31巻, 2019年
• "A formally verified proof of the prime number theorem"
• "Formalizing IMO Problems and Solutions in Isabelle/HOL", 2020年
• leanprover-community/lean4web