0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@etale_cohomology(Etale Cohomology)

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

0
Posted at

Executive Summary

忙しくて本文をお読みになれない方のために、まず最初に本稿の内容を要約してお伝えいたします。
本文だけをお読みになる方は、このEzecutive Summary を読み飛ばしていただいて差し支えございません。

本稿の問い

数学者が自然言語で書いた証明 を、Lean 4 や Isabelle などの 定理証明支援系のコード に置き換え、証明に論理の飛躍がないかを機械で検証する営みを、形式化 と呼びます。

本稿の問いは、「どの数学の定理が、どの定理証明支援系で形式化されたのか」を、どこで調べられ、どう読めばよいのか 、という点にあります。

本稿で取り上げる一覧とアーカイブ

名前 どんなものか 本稿で取り上げる理由
Freek Wiedijk「Formalizing 100 Theorems」 有名な100の定理ごとに、どの定理証明支援系で形式化されたかを並べた一覧 定理証明支援系どうしを比べる物差しとして、研究者のあいだで長く使われてきたため
「1000+ theorems」プロジェクト Wikipedia に収録されている名前が付いた定理の形式化の進捗度合いを追える一覧 100より広い範囲を扱い、Lean 版では定理ごとに Lean のコードが表示されるため
Isabelle の Archive of Formal Proofs（AFP） Isabelle で形式化された成果の、査読付きの公開アーカイブ 有名な定理の一覧ではないが、証明の全文を読める巨大な実例の宝庫であり、宣言的スタイルの実例が多いため
『The Seventeen Provers of the World』 √2 の無理性を扱った1つの定理に絞り、17個の定理証明支援系による形式化を比較して文献。なお、序章では、素数定理、四色定理、ジョルダン曲線定理の大規模な形式化も紹介されている 同じ定理を中心題材として、各システムでどのように形式化されるかを直接比べられ、タクティクと宣言的スタイルの違いを学ぶのに役立つため（Otter/Ivy は √2 の無理性そのものではなく、中心となる補題を証明しています）

なお、上記の4つの一覧（・アーカイブ）うち3つは、数学の定理のみ を扱います。
Archive of Formal Proofs は、計算機科学の成果 も含みます。

資料 扱う範囲
Formalizing 100 Theorems 数学の定理100件のみ
1000+ theorems Wikipedia に採録されている名前が付された数学の定理
The Seventeen Provers of the World 数学の定理1件（√2 の無理性）
Archive of Formal Proofs 計算機科学と数学の両方

繰り返しとなりますが、Archive of Formal Proofs には、プログラムの検証や、プログラミング言語の意味論といった計算機科学の成果も多く含まれています。（詳しくは第4章でご説明します）

本稿の結論

  • 「どの定理が、どの定理証明支援系で形式化されたか」 を調べる 出発点 は、Freek Wiedijk の「Formalizing 100 Theorems」 です。
    2026年9月23日に確認した時点で、100の定理はすべて、少なくとも1つの定理証明支援系で形式化されています
     
  • 一覧で示されている事実は、「形式化された」か「まだ形式化されていない」かです。
    なお、「まだ形式化されていない」は、その数学定理が「正しくない」ということを意味するものではありません
     
  • 一覧の多くは、形式化がタクティクで書かれたのか、宣言的スタイルで書かれたのか を、列として 示していません。両者を見分けるためには、定理証明支援系の性格を知ったうえで、コードを読んで確かめる必要があります
     
  • 定理証明支援系の性格は、大まかに分かれます。
    HOL Light と Rocq はタクティクが中心、
    Isabelle はタクティクと宣言的スタイル（Isar）の両方、
    Mizar は宣言的スタイル です。
    Lean の mathlib では、定理の55.1%が term mode、44.9%が tactic mode で証明されています
     
  • 同じ定理を複数の言語で書いた実例を並べて読むことが、書き方を学ぶ近道です。
    その格好の教材となりうるのが、『The Seventeen Provers of the World』です

Executive Summary で使う用語の簡単な説明

用語 簡単な説明 詳しい説明
形式化 自然言語で書かれた数学の証明を、定理証明支援系のコードに置き換え、機械で検証すること 第1章
定理証明支援系 証明を1ステップずつ機械で検査するソフトウェア。Lean、Isabelle、Rocq（旧 Coq）、HOL Light、Mizar など がある 第1章
タクティク 「帰納法を使え」「この等式で書き換えよ」のように、証明の手順を命令として積み重ねる書き方 第5章
宣言的スタイル 「$A$ が成り立つ。したがって $B$ が成り立つ」のように、証明の筋道そのものを書き下す書き方。Isabelle では Isar と呼ばれる 第5章

本稿の位置づけ

定理証明言語を学び始めた方が、数学の定理の形式化の過去の実績を調べ、そこから証明の書き方を学ぶための、道案内の記事です。

本稿の主目的は、形式化の実績の一覧を「検索のための表」として終わらせず、実際の証明のコードを読み、書き方の違いを学ぶ入口として使う方法を示すことです。

本稿の位置づけ.png

想定読者

  • 定理証明言語（Lean 4、Isabelle、Rocq など）を学び始めて半年以内の方
     
  • 特定の定理証明言語のコードとして、証明の正しさを検証するためのコードをどう記述するかを知りたい方
     
  • 定理証明支援系別に、形式化の実績を比較し、違いを知りたい方

前提とする知識

  • いずれかの定理証明言語で、簡単な定理を1つ証明したことがある程度の経験

前提としない知識

  • 特定の定理証明支援系の詳しい知識
     
  • 形式化の研究の歴史

本稿の用語と訳語について

本稿では、専門用語の日本語の訳語を、日本の研究者や実務家のあいだで確立された訳語があるものに限って用います。

確立された訳語を確認できなかった専門用語は、英語のまま記します。

たとえば、Lean の証明の書き方を表す tactic mode と term mode は、日本語の訳語を確認できなかったため、英語のまま記します。

本稿から得られること

  1. 数学の定理の形式化の過去の実績を集めた一覧の所在と、その読み方 が分かります
     
  2. 一覧を読むことで、定理証明支援系ごとの実績 を比べられます
     
  3. 形式化がタクティクで書かれたのか、宣言的スタイルで書かれたのかを見分ける手がかり が得られます
     
  4. 同じ定理を複数の定理証明言語で書いた実例から、コードの書き方の違い を学べます

第1章　形式化とは何か

タロウくん：
先生、最近「数学の定理を形式化した」というニュースをよく見かけます。
形式化とは、何をすることなのでしょうか。

専任講師：
数学者が英語や日本語で書いた証明を、定理証明支援系のコードに置き換えることです。

置き換えたコードは、定理証明支援系が1ステップずつ検査します。

検査が最後まで通れば、その定理証明支援系の論理・公理系のもとで、その証明が正しいものとして受理されたことになります。

平たく言えば、証明に論理の飛躍がないと機械が認めた、ということです。

ただし、この受理は、採用した公理や定義、そして検査器の実装が正しいことを前提にしています。

本稿で「定理が形式化された」と言うときは、ある形式化された定理の記述とその証明が、その定理証明支援系で受理されたことを指します。

自然言語で書かれた元の定理と同じ内容になっているか、採用した公理や定義が意図に合っているかは、別に人間が確かめる必要があります。この点は、第7章で詳しく扱います。

タロウくん：
人間が読んで確かめるのと、何が違うのですか？

専任講師：
人間が書く証明には、「明らかに」「同様にして」といった省略があります。

定理証明支援系は、人間向けの「明らかに」だけでは済ませられず、機械が検査できる形で必要な情報を与える必要があります。

実際には、ライブラリやタクティク、自動証明などが、その一部を肩代わりします。

自然言語で「明らかに」と一言で述べられる部分のすべてを、定理証明エンジニアが、定理証明支援系の低レベルなコードに展開するのではありません。

そのため、人間の目では見落としていた小さな誤りが、形式化の途中で見つかることがあります。

たとえば、1974年、2002年、2005年の3本の論文の結果を Isabelle/HOL で形式化した研究では、2005年の論文に小さな誤りが見つかり、その論文の著者の助言で簡単に直せたと報告されています。

出典：
A. Koutsoukou-Argyraki, W. Li, L. C. Paulson, "Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL", Experimental Mathematics, 31(2), pp. 401–412, 2022. doi: 10.1080/10586458.2021.1980465。arXiv:2101.05257
https://arxiv.org/pdf/2101.05257

タロウくん：
形式化された定理の一覧を見れば、どの定理がどの定理証明支援系で検証されたか、分かるのですね。

専任講師：
そうです。

次の章から、その一覧を順に見ていきましょう。

第2章　Freek Wiedijk「Formalizing 100 Theorems」

2-1　どんな一覧か

「Formalizing 100 Theorems」 は、オランダのラドバウド大学の Freek Wiedijk が作った一覧です。

有名な数学の定理 100個について、どの定理証明支援系で形式化されたかを、定理ごとに収録した一覧 です。

出典：
F. Wiedijk, "Formalizing 100 Theorems", Radboud University Nijmegen
https://www.cs.ru.nl/~freek/100/

2-2　取り上げる理由

この一覧は、定理証明支援系どうしを比べる物差しとして、研究者のあいだで長く使われてきました。

Metamath の公式ページは、この一覧が、良くも悪くも、他の人々によって定理証明支援系を評価するために使われている、と書いています。

出典：
Metamath「Metamath 100」
https://us.metamath.org/mm_100.html

定理証明支援系を学び始めた方にとっては、「有名な定理が、どの言語で形式化済みか」を一目で見渡せる、最初の地図 になります。

2-3　読み方

一覧は、次の決まりで書かれています。

表示 意味
斜体の定理 まだ形式化されていない定理（2026年9月23日に確認した時点では、100の定理すべてが形式化済みのため、斜体の定理はありません）
斜体の形式化 構成的な証明による形式化
下線の定理 難しい証明の定理
各定理の下の並び その定理を形式化した定理証明支援系と、形式化した人の名前。定理の記述（statement）へのリンクが付く

各定理 の下の並びは、年代順ではなく、定理証明支援系の一覧の順 に並んでいます。

たとえば、第1番の「√2 の無理性」の下には、HOL Light、Isabelle、Lean、Rocq、Metamath、Mizar、ACL2、ProofPower、PVS、Imandra、Megalodon、Naproche、NuPRL の形式化が並んでいます。

タロウくん：
「構成的な証明」 とは何ですか？

専任講師：
存在を示すときに、実際にその物を作ってみせる証明のこと です。

背理法で「存在しないと仮定すると矛盾する」とだけ示す証明とは 区別 されます。

*定理証明支援系には、構成的な証明を重んじるものがある ので、一覧でも区別している のです。

2-4　言語ごとの付録

この一覧には、言語ごとの付録があります。

Rocq（旧Coq）版 の付録では、Rocq で形式化された定理の記述を見られます。
表示を切り替えると、形式化に使われた公理や、どの版の Rocq で 動作を確かめたかという 再現性の情報 まで見られます。

出典：
「Formalizing 100 theorems in Rocq」
https://madiot.fr/rocq100/

Lean 版 には、まだ Lean で形式化されていない定理だけを集めたページもあります。

出典：
Lean community「Missing theorems from Freek Wiedijk's list of 100 theorems」
https://leanprover-community.github.io/100-missing.html

第3章　「1000+ theorems」プロジェクト

3-1　どんな一覧か

「1000+ theorems」 は、Freek Wiedijk が始めたプロジェクトです。

出典：
「Formalized theorems - 1000+ theorems」（プロジェクトのページ。Wikipedia の「List of theorems」に載っている定理の形式化を追うことを掲げている）
https://1000-plus.github.io/

Wikipedia の「List of theorems」に載っている名前付きの定理 について、形式化の進み具合を追っています。

出典：
Wikipedia「List of theorems」
https://en.wikipedia.org/wiki/List_of_theorems

「Formalizing 100 Theorems」の範囲を、1000を超える定理に広げたもの です。

「1000+ theorems」について参照した文章（出典）：

3-2　取り上げる理由

理由は2つ あります。

1つ目 は、有名な100の定理より広い範囲の定理を調べられることです。

2つ目 は、Lean 版 の一覧では、定理ごとに mathlib の Lean のコード（定理の記述）が表示 されることです。
数学書に載っている定理が、Lean ではどう書かれるのかを、そのまま見比べることができます。

Lean 版 の一覧のページによれば、2026年9月23日に確認した時点で、238件の定理が Lean で形式化 されていると記載されています。

3-3　読み方

一覧は表の形 をしており、各行 が1つの定理、列 が MSC の分類番号、定理の名前、Isabelle、HOL Light、Rocq、Lean、Metamath、Mizar です。

形式化がある欄には、その形式化の場所へのリンクと、形式化した人の名前が付されています。

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

言葉 意味
定理の記述（statement） 何を仮定し、何を示すのかを書いた部分
証明（proof） その記述を、どう導くのかを書いた部分
  • Lean 版の一覧には、Lean のコードが収録されています。
  • ただし、収録されているのは定理の記述（theorem から始まる、何を仮定し何を示すかを書いた部分）だけです。
  • 証明の部分（by 以降のタクティクなど）は収録されていません。ただし、各定理には docs（mathlib の文書）と source（GitHub 上のソースコード。コミットと行番号を指定したリンク）のリンクが付いており、source をたどると証明の本体を読むことができます。

たとえば、ピタゴラスの定理にあたる定理 は、次のように書かれています。

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
    {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) :
    dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔
    angle p₁ p₂ p₃ = Real.pi / 2

出典：
Lean community「1000+ theorems in Lean」に表示されている mathlib の定理の記述（読みやすさのため、改行の位置を変えた）
https://leanprover-community.github.io/1000.html

タロウくん：
数学書の「直角三角形では、斜辺の2乗は他の2辺の2乗の和に等しい」が、ずいぶん長くなりますね。

専任講師：
そうです。

数学書では暗黙の前提になっている「どんな空間の話か」「距離や角度はどう定義されているか」を、すべて明示しているから です。

[InnerProductSpace ℝ V] は、「内積を持つ実ベクトル空間の上の話である」という前提を書いたもの です。

また、数学書では「直角ならば」と一方向に書くことが多いのですが、この定理は ↔ で、「直角であることと、2乗の和の等式が成り立つことは同値である」と、両方向を述べています。

数学書の定理と、形式化された定理の記述を見比べると、数学書が何を省略しているかが分かります。

すでに述べましたが、一覧には、定理の記述だけが表示され、証明は表示されません。
証明を読みたいときは、定理の名前から mathlib の文書をたどる必要があります。

第4章　Isabelle の Archive of Formal Proofs（AFP）

4-1　どんなものか

Archive of Formal Proofs（AFP） は、Isabelle で機械的に検査された、証明ライブラリ、例題、大規模な研究成果の集まり です。

AFP に収録される成果は、数学の定理の形式化に限られません。
計算機科学と数学の両方 の成果が採録されています。

実際に収録されている成果には、命題論理のコンパクト性定理 のような 論理学 や 数学の成果 だけでなく、以下が含まれます。

  • プログラムの情報流の安全性を証明するための並行分離論理の形式化
  • インタプリタの最適化の形式化

上記のような、プログラムの検証やプログラミング言語に関する成果も多く 含まれています。

出典：
"From LCF to Isabelle/HOL"（AFP が計算機科学と数学の両方を扱うこと）
https://arxiv.org/pdf/1907.02836

AFP は、学術誌の形で運営されており、投稿は査読されます。
dblp に索引付けされ、ISSN（2150-914x）を持っています。

また、AFP の成果は、対応する Isabelle のリリースでのビルドと保守を前提に公開されています。
対応の状況や使い方は、導入のときに AFP の公式のページで確かめてください。

収録された成果は、すべて BSD形式のライセンスか GNU LGPL で公開されており、自由にダウンロードし、使い、変更し、再配布できます。

Archive of Formal Proofs について参照した文章（出典）：

4-2　取り上げる理由

AFP は、有名な定理の一覧ではありません。
それでも 取り上げる理由は2つ あります。

1つ目 は、証明の全文を読めることです。

第2章で取り上げた 「Formalizing 100 Theorems」 と、第3章で取り上げた 「1000+ theorems」 は、主に「どの定理が形式化されたか」を示す一覧でした。証明の中身は一覧そのものには収録されておらず、各定理に付いたリンクから、mathlib のソースコードなどへ進んで読む必要がありました。

それに対して、AFP は、1つ1つの成果が、証明の全文を含む形で公開 されています。

2つ目 は、宣言的スタイルの実例 が多いことです。

Isabelle の宣言的スタイルである Isar で書かれた証明を大量に読んで、コードの書き方を学ぶ学習素材として活用することができます。

2019年の論文（下記参照）によれば、AFP は2004年に始まり、その時点で322人の著者による480の成果を収録し、約225万行の *Isar の文書で13万4千の定理と補題を証明していました。

出典：
L. C. Paulson, T. Nipkow, M. Wenzel, "From LCF to Isabelle/HOL", Formal Aspects of Computing, 31, pp. 675–698, 2019. doi: 10.1007/s00165-019-00492-1。arXiv:1907.02836
https://arxiv.org/pdf/1907.02836

ここで、「Isar の文書」 とは、Isabelle の理論ファイル全体を指す言い方です。

Isabelle は、宣言的な Isar の証明と、タクティクを並べた証明を、同じファイルの中で混ぜて書くことができます。

そのため、この行数がすべて宣言的スタイルの証明というわけではありません。

4-3　読み方と使い方

AFP のトップページには、収録された成果が、収録された日付の新しい順に並んでいます。

AFP の成果は、自分の Isabelle の証明の中から読み込んで使うこともできます。

AFP のヘルプのページによれば、Isabelle2021-1 以降では、ダウンロードした AFP を isabelle components -u で Isabelle に登録すると、自分の理論ファイルから imports "ABC.Some_ABC_Theory" の形で AFP の成果を参照できます。

AFP は、成果を論文などで引用するときの推奨の書式も示しています。

出典：
Archive of Formal Proofs「Help」
https://www.isa-afp.org/help

第5章　『The Seventeen Provers of the World』

5-1　どんなものか

『The Seventeen Provers of the World』 は、Freek Wiedijk がまとめた 本 です。

17個の定理証明支援系による形式化を比較するための題材を、 √2 の無理性を扱う1つの定理 に絞ったものです。

√2 の無理性を扱う1つの定理 を、17個の定理証明支援系で形式化した結果を比較することができます。

また、それぞれの定理証明支援系の開発者や利用者（定理証明エンジニア、形式証明の研究者など）が、それぞれの定理証明支援系における一般的な書き方で形式化しています。（他の定理証明支援系にそろえた書き方ではありません）

さらに、Freek Wiedijk がすべての定理証明支援系について、同じ質問（どの論理にもとづくか、どのように実装されているか、どのように使うかなど）を投げかけ、各担当者がその質問に答えています。

そのため、コードの書き方の違いと、その背景にある設計の違いを、同じ条件で比較するための恰好の資料として利用可能です。

17の定理証明支援系は、次のとおりです。
『The Seventeen Provers of the World』に掲載されている順に並べます。

  • HOL
  • Mizar
  • PVS
  • Coq
  • Otter/Ivy
  • Isabelle/Isar
  • Alfa/Agda
  • ACL2
  • PhoX
  • IMPS
  • Metamath
  • Theorema
  • Lego
  • Nuprl
  • Ωmega
  • B method
  • Minlog

HOL の節には、HOL Light、HOL4、ProofPower の3つの版の形式化が載っています。Coq は、現在は Rocq に名前が変わっています。

題材を1つに絞っているのは、書き方の違いだけを比べるためです。なお、序章では、当時完成したばかりの大規模な形式化として、Isabelle による素数定理、Coq による四色定理、HOL Light によるジョルダン曲線定理も紹介しています。

原稿は2005年にまとめられ、書籍版は2006年に Springer から刊行されました。

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Radboud University Nijmegen, 2005（書籍版は Lecture Notes in Computer Science 3600, Springer, 2006）
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

5-2　取り上げる理由

本稿の目的の1つは、タクティクで書かれたのか、宣言的スタイルで書かれたのかを見分けられるようになること です。

第2章で取り上げた 「Formalizing 100 Theorems」 と 第3章で取り上げた 「1000+ theorems」 、第4章で取り上げた Archive of Formal Proofs は、タクティクで書かれたのか、宣言的スタイルで書かれたのかが見分けられるようには書かれていません。

『The Seventeen Provers of the World』は、同じ定理を17個の定理証明支援系で形式化した実例を並べているため、書き方の違い（タクティクで書かれたのか、宣言的スタイルで書かれたのか）を同じ条件で比較できる、まとまった資料 です。

ただし、約20年前の資料なので、17個の定理証明支援系それぞれの書き方の細部は、現在とは異なります。

🔬 上級者向けコラム：17個の言語について

17個の定理証明支援系の特徴を、上級者向けに解説します。

以下では、『The Seventeen Provers of the World』に掲載されている順に、1番から17番までの番号を付けて解説します。

1番の HOL から8番の ACL2 までは、同書の中で、それぞれの定理証明支援系の開発者や利用者が答えた、共通の質問（論理、実装の方式、使い方など）への回答にもとづいて書きます。

9番の PhoX から17番の Minlog までは、筆者が同書の該当の節を確かめられなかったため、序章の比較表、目次に掲載されている形式化の担当者、序文、ほかの節の中の言及にもとづいて書きます。

比較表について、Wiedijk 自身が、「強力な自動証明」「大きなライブラリ」などの項目はかなり主観的だ、と断っています。

比較表の2つの項目には、名前が付いています。

「小さな証明の核（証明オブジェクト）」は de Bruijn 基準、「計算を自動で証明できる」は Poincaré 原理とも呼ばれます。de Bruijn 基準は、小さな核そのものを指すというより、小さく単純な検査器で最終の結果を確かめられるようにする設計上の考え方を指します。

1. HOL（HOL Light、HOL4、ProofPower）

John Harrison の回答によれば、HOL Light の論理は、無限公理、外延性公理、選択公理を持つ古典的な高階論理で、多相的な型変数を持つ単純型付きラムダ計算にもとづきます。

興味深いのは、HOL Light の核の公理化は、トポスの内部論理の通常の定義に近く、その意味で直観主義的な性格を持つ、という指摘です。ヒルベルトの ε の形で選択公理を加えた時点で、論理が古典的になります。

実装は LCF 方式で、定理を抽象型として扱い、定理は少数の基本推論規則を適用することでしか作れません。論理の核は、補助の関数を含めても、注釈と空行を除いて433行の OCaml のコードです。

2. Mizar

Andrzej Trybulec の回答によれば、Mizar は古典論理と Jaśkowski の自然演繹にもとづき、それ自体は特定の集合論とは独立した形式体系です。ただし、ライブラリの Mizar Mathematical Library は、Tarski–Grothendieck 集合論にもとづきます。

作業は、文書を ASCII で書いて検証器に丸ごと処理させる「lazy interaction」で進めます。証明の計画から始め、検証器が報告する隙間を埋めていく段階的な詳細化が、最善の書き方とされています。

比較表で、宣言的スタイルのシステムでありながら、型と依存型に丸が付いている点も特徴です。

3. PVS

John Rushby の回答によれば、PVS は古典的な高階論理にもとづき、主に Common Lisp で書かれています。

述語で絞り込んだ部分型（predicate subtypes）と依存型を持ち、型検査と定理証明が密接に統合されています。述語による部分型があるため、型検査器は型の正しさの条件（TCC）を証明の義務として生成します。比較表で「型は決定可能」にバツが付いているのは、この性格によるものです。

4. Coq（現在の Rocq）

Laurent Théry の回答によれば、Coq は、依存型を持つラムダ計算である Calculus of Inductive Constructions にもとづきます。

Curry-Howard 同型に従い、システムの核は、証明の正しさを確かめる型検査のアルゴリズムです。明示的な証明オブジェクトを扱うため、システムの健全性は型検査のアルゴリズムの正しい実装だけに依存します。形式的な仕様を満たすプログラムを取り出す、プログラム抽出の機能も持ちます。

同書には、タクティクの証明に加えて、そのタクティクが生み出した証明の項も載っています。また、Georges Gonthier の流儀による、四色定理の証明のために拡張したタクティクを使った形式化も載っています。

5. Otter/Ivy

William McCune の回答によれば、Otter の論理は、型のない、等号付きの一階述語論理です。実装は、導出（resolution）、パラモジュレーション、書き換えにもとづく自動定理証明器です。

Otter が見つけた証明は、Ivy の証明オブジェクトとして出力され、独立に検査できます。比較表で「小さな証明の核」に丸が付いているのは、このためです。実数を扱わないため、√2 の無理性そのものではなく、その中心となる補題を証明しています。

6. Isabelle/Isar

Markus Wenzel の回答によれば、Isabelle は論理の枠組み（logical framework）で、HOL や ZF などの対象論理を、最小の高階論理（Pure）による一般的な自然演繹の環境に埋め込みます。

Isabelle/Pure は、型理論の言葉で言えば λ-HOL に対応し、構文上の関数の矢印 ⇒、全称量化の依存的な矢印 ⋀、含意の矢印 ⟹ という3つの水準のラムダ計算を持ちます。

実装は HOL や LCF と同じく完全に展開的で、すべての証明は核の基本推論に展開されます。Curry-Howard の命題型対応を使い、基本推論をラムダ項として記録して、独立に検査することもできます。

構造化された Isar の証明と、構造化されていないタクティクのスクリプトを、同じ理論の中で自由に混ぜて書けます。

7. Alfa/Agda

Thierry Coquand の回答によれば、論理は Martin-Löf が1972年に提案した直観主義的な型理論に、一般のデータ型の宣言と場合分けの記法を加えたものです。

証明と、依存型を持つ関数型プログラムを同一視し、メタ変数（穴）を使って対話的に証明とプログラムを組み立てます。構文は、Lennart Augustsson が設計した関数型言語 Cayenne に非常に近いとされています。Alfa は、このシステムのための利用者向けの画面（インターフェース）の名前です。

同書に載っているのは2005年当時のシステムであり、その後の Agda とは実装が異なる可能性があります。

8. ACL2

Ruben Gamboa による形式化では、ACL2 が帰納法に非常に強いことを生かし、偶数を2つずつたどる帰納法の型（even-induction）を定義したうえで、定理ごとに帰納法の方針などのヒントを与えて自動証明させています。

比較表では、「読みやすい証明の入力ファイル」に丸が付いた4つのシステムの1つであり、型を持たない一方で、強力な自動証明を持つとされています。

9. PhoX

形式化の担当者は Christophe Raffalli と Paul Rozière です。比較表では、小さな証明の核を持ち、計算を自動で証明でき、型が決定可能な、高階論理にもとづくシステムとされています。一方、強力な自動証明と、大きな数学のライブラリにはバツが付いています。

10. IMPS

形式化の担当者は William Farmer です。比較表では、高階論理にもとづき、型が決定可能で、強力な自動証明と大きな数学のライブラリを持ち、実数についての定理を記述できるシステムとされています。小さな証明の核にはバツが付いています。

11. Metamath

形式化の担当者は Norman Megill です。比較表では、17のうち論理の枠組み（logical framework）に丸が付いた2つのシステムの1つであり（もう1つは Isabelle）、ZFC 集合論にもとづき、小さな証明の核を持ちます。型を持たず、計算の自動証明と強力な自動証明の両方にバツが付いています。自動化に頼らず、証明の各段階を明示するシステムであることが読み取れます。

12. Theorema

形式化の担当者は Wolfgang Windsteiger、Bruno Buchberger、Markus Rosenkranz です。Dana Scott は序文で、Theorema は証明の読みやすさを第一の要件とし、その成功は報告に表れていると評しています。ただし、Buchberger が当初設定した目的は研究ではなく教育の道具であり、その力はまだ HOL 系のシステムには及ばない、とも述べています。比較表では、読みやすい入力と強力な自動証明の両方に丸が付いています。

13. Lego

形式化の担当者は Conor McBride です。比較表では、小さな証明の核、構成的な論理、依存型を持ち、型が決定可能なシステムとされています。

Wiedijk は序章で、McBride の指摘を紹介しています。√p の無理性を証明するとき、p について「既約である（約数が1と自分自身だけ）」と仮定するか、「素である（積を割り切れば、どちらかの因数を割り切る）」と仮定するかの2通りがあり、後者を仮定すると、√2 の無理性を証明するよりかえって易しくなる、というものです。その場合、難しい部分は「2が素である」ことの証明に移ります。

14. Nuprl

形式化の担当者は Paul Jackson です。比較表では、利用者が拡張・プログラムでき、構成的な論理と依存型を持ち、大きな数学のライブラリを持つシステムとされています。

17のうち、依存型を持ちながら「型は決定可能」にバツが付いているのは、PVS と Nuprl の2つだけです。

筆者は、過去の記事で Nuprl を詳しく扱いました。Nuprl は、Cornell 大学の PRL プロジェクトが1984年から作ってきた証明支援系で、computational type theory の原型です。computational type theory は、先に推論規則を書いて型理論を定義する流儀（formal type theory）とは逆に、先にプログラミング言語とその計算の仕方を定め、型はプログラムの振る舞いとしてあとから意味づける流儀です。

Nuprl の型理論は外延的で、equality reflection（命題として等しいことが証明できれば、判断としても等しいと扱ってよい、という規則）を持ちます。この規則を適用したあと、等しさの証明は項の中に残りません。そのため、型検査器は「2つの型が等しいことの証明が存在するか」を自分で判定しなければならず、型検査は決定不能になります。比較表の「型は決定可能」のバツは、この性格の表れです。Nuprl の系統では、型検査器が自動で判定するのではなく、利用者がタクティクを書いて証明を組み立てる作りになっています。

また、同じ過去の記事では、De Morgan cubical type theory の原論文が、その意味論の大部分が Mark Bickford によって Nuprl で形式的に検証されたと述べていることも紹介しました。規則を先に書く流儀の型理論の意味論が、計算を先に置く流儀の実装である Nuprl の中で確かめられている、という点で、2つの流儀が交わっています。

出典：
Etale Cohomology「Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す」、Qiita
https://qiita.com/etale_cohomology/items/a830a5ac5013a298fb97

出典：
Etale Cohomology「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」、Qiita、2026年9月12日
https://qiita.com/etale_cohomology/items/4035a0b3f4d40766437c

15. Ωmega

形式化の担当者は Christoph Benzmüller、Armin Fiedler、Andreas Meier、Martin Pollet、Jörg Siekmann です。比較表では、高階論理にもとづき、型が決定可能で、小さな証明の核、利用者による拡張性、強力な自動証明を持つシステムとされています。

16. B method

形式化の担当者は Dominique Cansell です。比較表では、ZFC 集合論にもとづき、型を持たず、強力な自動証明を持つシステムとされています。17のうち、ZFC 集合論にもとづくとされたのは、Mizar、Isabelle（Isabelle/ZF）、Metamath、B method の4つです。Wiedijk は、ZF 流の集合論は理論上の道具にすぎず現実の証明には使えない、と考える人もいるが、この表は4つのシステムが集合論の基礎の上で多くの現実の数学を形式化できることを示している、と述べています。

17. Minlog

形式化の担当者は Helmut Schwichtenberg です。比較表では、小さな証明の核、利用者による拡張性、構成的な論理を持ち、型が決定可能なシステムとされています。

Coq の節によれば、Coq の2つ目の形式化は、この Minlog の形式化から着想を得たものです。正の整数を2進表現で表す型を使うことで、偶数かどうかを簡単に判定でき、整礎帰納法の代わりに通常の帰納法で済ませています。

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Radboud University Nijmegen, 2005（書籍版は Springer LNCS 3600, 2006）
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

第6章　タクティクと宣言的スタイルの見分け方

6-1　2つの書き方

タロウくん：
先生、タクティク と 宣言的スタイル は、何が違うのですか？

専任講師：
タクティク は、証明の手順を、定理証明支援系への命令として積み重ねる書き方です。

「帰納法を使え」「この等式で書き換えよ」「自動証明を試せ」と命令していきます。

命令を1つ実行するたびに、定理証明支援系が「残りの証明すべきこと」を表示します。

宣言的スタイル は、証明の筋道そのものを、数学の証明に近い形で書き下す書き方です。

「$A$ が成り立つ。したがって $B$ が成り立つ」と、途中の主張を明示しながら進みます。

タロウくん：
どちらがよいのでしょうか。

専任講師：
一長一短です。

タクティクは、対話的にゴールを変形しながら自動化を利用しやすい書き方です。
ただし、コードだけを読んでも、証明の筋道が分かりにくいことがあります。

宣言的スタイルは、途中の主張を明示することで、人間が証明の筋道を追いやすい形にしやすい書き方です。
ただし、途中の主張をすべて書くので、コードが長くなりがちです。

6-2　定理証明支援系ごとの性格

『The Seventeen Provers of the World』 で、それぞれの定理証明支援系の開発者が説明している書き方のうち、代表的な7個を表にまとめます。

17個すべての解説は、第5章のコラムをご覧ください。

定理証明支援系 書き方 資料での説明
HOL Light タクティク 形式化は、OCaml のソースコードとして解釈されるタクティクのスクリプト
Rocq タクティク 証明は、LCF 流のタクティクの方法で対話的に組み立てる
Isabelle 両方 構造化された Isar の証明と、構造化されていないタクティクのスクリプトを、自由に混ぜて書ける
Mizar 宣言的スタイル 古典論理と Jaśkowski の自然演繹にもとづき、数学の日常の言葉づかいに非常に近い
PVS タクティク（コマンド） 利用者が与えるコマンドにもとづいて、シーケントの証明木を組み立てる
Agda どちらでもない 証明とプログラムを同一視し、依存型を持つ関数型言語でプログラムを書く感覚で証明を書く
ACL2 どちらでもない 定理ごとに、帰納法の方針などのヒントを与えて、自動証明させる

同じ資料の比較表では、「読みやすい証明の入力ファイル」の項目に丸が付いているのは、17のシステムのうち、Mizar、Isabelle/Isar、ACL2、Theorema の4つだけでした。

6-3　Lean の場合

Lean の証明の書き方は、「タクティク」と「宣言的スタイル」ではなく、tactic mode と term mode に分かれます。

  • tactic mode は、by で始めて、タクティクを積み重ねる書き方です。
     
  • term mode は、証明の項、つまり証明そのものにあたるプログラムを、直接書く書き方です。

2026年の論文は、論文が解析の対象とした時点の mathlib のソースファイルを静的解析し、17万985件の定理のうち、44.9%（7万6,708件）が tactic mode、55.1%（9万4,277件）が term mode で証明されていると報告 しています。

この割合は、Lean という言語の一般的な性質ではありません。
ある時点の mathlib を、ある基準で数えた観測値です。
mathlib は日々更新されるため、割合も変わります。

tactic mode の証明の多くは短く、手順の数の中央値は2です。
by simp のような1手順の証明が39.2%、3手順以内が68.7%を占め、10手順以上の証明は9.4%だけでした。

出典：
"The Network Structure of Mathlib", arXiv:2604.24797
https://arxiv.org/pdf/2604.24797

タロウくん：
Lean には、Isar のような宣言的スタイル はないのですか？

専任講師：
Isar にあたる独立した言語はありません。

ただし、tactic mode の中で have、show、calc を使うと、途中の主張を明示しながら、宣言的スタイルに近い形で 書けます。

とくに calc を使った計算の証明について、Lean で Virasoro 代数を形式化した2025年の論文は、読みやすく、更新にも強いと述べています。同じ論文は、その研究で実際に書かれた証明では、手順を1つずつ書くタクティクの証明のほうが多かった、とも述べています。

なお、term mode は、証明項を直接書くという入力の様式の分類であり、Isar のように途中の主張を文章として並べる宣言的スタイルと、1対1に対応する概念ではありません。短いラムダ項も term mode ですし、tactic mode の中でも have や calc で構造を明示できます。

出典：
"Virasoro algebra and Sugawara constructions formally in Lean", arXiv:2510.21741
https://arxiv.org/pdf/2510.21741

6-4　実例：√2 の無理性を4つの書き方で読む

『The Seventeen Provers of the World』 から、√2 の無理性の証明の一部を、4つの書き方で引用 します。

以下は歴史的な資料からの引用と転記です。
現在の版で動くことは保証せず、書き方を比べることだけを目的に載せます。

HOL Light（タクティク）

p * p = 2 * q * q ならば q = 0 という、証明の中心となる補題です。

let NSQRT_2 = prove
 (`!p q. p * p = 2 * q * q ==> q = 0`,
  MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
  REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
  POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);;

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Section 1（HOL、John Harrison による HOL Light の版）
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

MATCH_MP_TAC、REWRITE_TAC のように、_TAC で終わる命令がタクティクです。命令を THEN でつないで、手順を積み重ねています。コードだけを読んでも、どんな筋道で証明しているかは読み取りにくいことが分かります。

Mizar（宣言的スタイル）

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;
  :: 中略
  hence contradiction by A10,W5,A11,W3;
end;

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Section 2（Mizar、Andrzej Trybulec による版）。中略は筆者による
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

assume（仮定する）、then consider（それゆえ、次のものがとれる）、hence contradiction（したがって矛盾）のように、数学の証明の言葉づかいに近い形で、背理法の筋道を書き下しています。

Isabelle/Isar（宣言的スタイル）

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 ..
  (* 中略 *)
  with p show False by simp
qed

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Section 6（Isabelle/Isar、Markus Wenzel による版）。組版された原文を、筆者がテキストに書き起こした（記号は同じ意味の Unicode の文字で表した。識別子の「-」や、式を囲む引用符の省略は、原文の組版のとおりであり、Isabelle のソースファイルでの表記とは異なる場合がある）。中略は筆者による
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

assume、then have、obtain、show で、途中の主張を1つずつ明示しています。途中の主張を正しいと確かめる細かい作業は、by simp のように、最後に自動証明に任せています。

Isabelle（タクティクの apply スタイル）

同じ Isabelle でも、タクティクを並べる書き方ができます。

lemma prime-dvd-other-side:
  n * n = p * (k * k) ⟹ p ∈ prime ⟹ p dvd n
  apply (subgoal-tac p dvd n * n, blast dest: prime-dvd-mult)
  apply (rule-tac j = k * k in dvd-mult-left, simp)
  done

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Section 6.4（Isabelle/HOL のスクリプト版、Larry Paulson による版）。組版された原文を、筆者がテキストに書き起こした（識別子の「-」や、式を囲む引用符の省略は、原文の組版のとおり）
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

apply で始まる行が、タクティクの命令です。Isar の版と比べると、途中の主張が書かれていないことが分かります。

タロウくん：
同じ Isabelle なのに、ずいぶん見た目が違いますね。

専任講師：
そうです。

だからこそ、一覧で「Isabelle で形式化された」と分かっても、それが Isar で書かれたのか、apply スタイルで書かれたのかは、コードを読むまで分かりません。

見分けるときは、proof、assume、have、show、qed が並んでいれば Isar らしい構造化された書き方、apply が続いていれば apply スタイル、と見当を付けるとよいでしょう。

ただし、これは最初の見当を付けるための目印です。

by は、Lean では tactic mode の始まりを示しますが、Isabelle では構造化された証明の末尾で自動証明を呼ぶためにも使われます。

キーワードだけで分類せず、途中の主張と証明の状態がどう書かれているかを見てください。

第7章　「正しいと検証された」と「正しいとは言い切れない」の読み方

タロウくん：
先生、一覧で「形式化されていない」と書かれている定理は、定理証明支援系で「正しいとは言い切れない」と判定された、ということですか？

専任講師：
いいえ、違います。

ここは、誤解しやすいところです。

一覧が示しているのは、「形式化された」か「まだ形式化されていない」か、です。

「まだ形式化されていない」は、「定理証明支援系で検査したら誤りが見つかった」という意味ではありません。「まだ誰も、その定理証明支援系のコードに置き換え終えていない」という意味です。

タロウくん：
では、形式化の試みが失敗した記録は、どこにあるのでしょうか。

専任講師：
本稿で取り上げた一覧は、失敗の記録を整理したものではありません。

形式化の途中で元の論文の誤りが見つかった場合は、第1章で紹介した例のように、その形式化を報告する論文の中に書かれるのが普通です。

タロウくん：
「形式化された」ならば、その定理は絶対に正しい、と考えてよいのですか。

専任講師：
定理証明支援系が正しく作られていて、定理の記述が数学者の意図どおりに書かれていれば、その証明には論理の飛躍がない、と言えます。

ただし、2つの点に注意が必要 です。

1つ目 は、定理の記述そのものが、数学書の定理と同じ意味になっているか、という点です。
第3章で見たように、形式化された定理の記述は、数学書の定理より多くの前提を明示します。
その前提が意図どおりかは、人間が確かめる必要があります。

2つ目 は、形式化に使われた公理です。
Rocq 版の付録で、形式化に使われた公理を表示できるのは、そのためです。

🔬 上級者向けコラム：「機械が検証した」の信頼性を支える、小さな検査の核

定理証明支援系が「証明は正しい」と判定するとき、その判定を最終的に下すのは、システムの中の小さな検査の部分です。

『The Seventeen Provers of the World』の比較表には、「小さな証明の核（証明オブジェクト）」という項目があり、この性質は de Bruijn 基準とも呼ばれる、と注記されています。

de Bruijn 基準は、大規模な自動証明や証明の生成器とは分けて、比較的小さく単純な検査器で最終の結果を確かめられるようにする、という設計上の考え方を指します。LCF 方式の小さな核や、独立に検査できる証明オブジェクトは、その考え方を実現する代表的な方法です。

たとえば HOL Light の開発者の John Harrison は、同書で、HOL Light の論理の核は、補助の関数を含めても、注釈と空行を除いて433行の OCaml のコードだけでできている、と説明しています。

核が小さければ、核そのものが正しく作られているかを、人間が確かめやすくなります。どれほど複雑なタクティクや自動証明を使っても、最終的にはこの小さな核が1ステップずつ検査するので、証明全体の信頼性は、小さな核の信頼性に帰着します。

出典：
F. Wiedijk (compiler), "The Seventeen Provers of the World", Introduction の比較表と、Section 1.6（HOL Light）
https://www.cs.ru.nl/~freek/comparison/comparison.pdf

第8章　定理証明支援系ごとの実績を比べる

一覧を使うと、定理証明支援系ごとの実績を比べることができます。

ただし、次の数値は、同じ定理を同じ定式化で数えた統一の物差しではありません。

各一覧の収録の基準、更新の時点、同値な定理の扱い、リンク切れや保守の状況に左右されるため、成熟度の単純な順位表として採用することには慎重であるべきです。

また、各一覧は更新されるため、数は確認した日の時点のものです。
いつの時点の数かを必ず確かめてください。

時期 数 典拠
2008年 100の定理のうち、すべてのシステムを合わせて80が形式化済み。HOL Light 69、Mizar 45、ProofPower 42、Isabelle 40、Coq 39 Wiedijk、Notices of the AMS、2008年
2020年 100の定理のうち、95が少なくとも1つのシステムで形式化済み。Isabelle は83で、HOL Light に次ぐ2位 Koutsoukou-Argyraki、2020年
2026年9月23日確認（一覧の最終更新は2026年9月17日） 100の定理のすべてが形式化済み（100%）。システムごとの数は、HOL Light 95、Isabelle 95、Lean 83、Rocq 80、Metamath 74、Mizar 71、nqthm/ACL2 48、ProofPower 43、PVS 26、Imandra 20、Megalodon 12、Naproche 10、NuPRL/MetaPRL 8 Freek Wiedijk「Formalizing 100 Theorems」のトップページ
2026年9月23日確認 Rocq で形式化された定理は80。Lean でまだ形式化されていない定理は15（形式化された定理は85） 各言語の付録のページ

2008年から2026年9月23日までのあいだに、100の定理はすべて、少なくとも1つのシステムで形式化されました。
とくに Lean の数が大きく伸びています。
2020年4月の時点で Lean は29でしたが、2026年9月23日に確認した時点では83から85です。

Lean の数が83と85で食い違うのは、Freek Wiedijk のトップページと、Lean のコミュニティのページとで、更新の時期が異なるためと考えられます。一覧の数を引用するときは、どのページを、いつ確認したものかを明記してください。

定理証明支援系ごとの実績について参照した文章（出典）：

タロウくん：
数が多い定理証明支援系ほど、優れているのでしょうか？

専任講師：
そうとは言い切れません。

数は、そのシステムの利用者の数や、コミュニティの関心の向きにも左右されます。

Metamath の公式ページも、この一覧が、良くも悪くも、定理証明支援系の評価に使われている、という書き方をしています。

一覧の数は、「どの定理証明支援系で、どの分野の形式化が進んでいるか」を知る手がかりとして使うのがよいでしょう。

第9章　一覧から学びにつなげる手順

最後に、一覧を使って証明の書き方を学ぶ手順をまとめます。

  1. 「Formalizing 100 Theorems」で、よく知っている定理を1つ選ぶ（√2 の無理性、素数の無限性などがおすすめ）
     
  2. その定理の下に並んでいる形式化から、自分の学んでいる定理証明言語で書かれたコードを読む
     
  3. 同じ定理を別の定理証明言語で書いたコードも読み、並べて比べる
     
  4. コードに proof、have、show などが並んでいるか、apply や by とタクティクが並んでいるかで、書き方を見分ける
     
  5. 数学書の定理の文と、形式化された定理の記述を見比べ、形式化で何が明示されたかを確かめる
     
  6. 慣れてきたら、Lean 版の「1000+ theorems」や AFP で、より多くの定理の書き方を読む

タロウくん：
同じ定理を、いくつもの言語で読み比べるのですね。

学んでいる言語別の、最初の一歩

2026年9月23日に確認した時点での、たどり方です。各ページの作りは変わることがあります。

学んでいる言語 たどり方
Lean 「Formalizing 100 Theorems」の Lean 版で定理を選び、表示された定理の名前を mathlib の文書の検索に貼り付けて、定理の定義の位置を見る。定理の直後の by、補助の補題、calc を追う。次に「1000+ theorems」の Lean 版へ広げる
Isabelle 「Formalizing 100 Theorems」の Isabelle 版で定理を選ぶ。次に AFP の各成果のページから理論ファイルへ進み、目的の theorem や lemma をファイルの中で検索する
Rocq 「Formalizing 100 theorems in Rocq」で定理を選び、定理の記述に加えて、使われた公理と、動作を確かめた版の情報を表示させる

専任講師：
そうです。

同じ数学的主張を形式化していても、定理の記述や前提、証明戦略には違いがあります。

その違いに注目すると、それぞれの定理証明言語の考え方が、よく見えてきます。

構成的か古典的か、集合論的な基礎、定理の定式化の仕方などによって、同じ数学的題材でも形式化の内容は変わり得ます。

第7章では、形式化された定理の記述や前提、公理について、人間が確認する必要があることを取り上げます。

参考文献

形式化の実績の一覧とアーカイブ：

書き方の比較と統計：

形式化の事例と実績：

  • A. Koutsoukou-Argyraki, W. Li, L. C. Paulson, "Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL", Experimental Mathematics, 31(2), pp. 401–412, 2022. doi: 10.1080/10586458.2021.1980465。arXiv:2101.05257
    https://arxiv.org/pdf/2101.05257
  • L. C. Paulson, T. Nipkow, M. Wenzel, "From LCF to Isabelle/HOL", Formal Aspects of Computing, 31, pp. 675–698, 2019. doi: 10.1007/s00165-019-00492-1。arXiv:1907.02836
    https://arxiv.org/pdf/1907.02836
  • F. Wiedijk, "Formal Proof—Getting Started", Notices of the AMS, 55(11), 2008
    https://www.ams.org/notices/200811/tx081101408p.pdf
  • A. Koutsoukou-Argyraki, "Formalising Mathematics – in Praxis; A Mathematician's First Experiences with Isabelle/HOL and the Why and How of Getting Started", Jahresbericht der Deutschen Mathematiker-Vereinigung, 2020. doi: 10.1365/s13291-020-00221-1
    https://link.springer.com/article/10.1365/s13291-020-00221-1
0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?