【Arend Theorem Prover 連載（初回）】「同型なものは等しい」を機械に検査させる ── 定理証明支援系 Arend がHoTTを公理としなかった理由

本記事は、Arend連載記事の第１回目です

Arend という定理証明支援系について、全６回にわたってお伝えします。

本記事はその初回の記事にあたります。

本稿は、以下の論点を扱います。

• Arendはどのような問題意識の下で設計された言語なのか
• 既存の定理証明言語（Lean 4、Isabelle、Idris 2、Agda等）との相違点は何か
• その違いは、続々と成果が積み上がりつつある数学定理の機械証明の国際数学プロジェクトや、その他の実務領域での利活用において、どのような価値を発揮することが期待されているのか

第２回以降で取り扱う論点の相互関係性については、この記事の末尾に予告編として掲載させて頂いております。

各回は、単独の独立した記事としても、お読めいただけるように心がけます。

---

連載初回記事（本記事）のExecutive Summary

本記事が述べることを、１枚の図にまとめます。

図の上半分 ── 数学の基礎が、型理論へ移りつつある

2006年、ホモトピー型理論（HoTT）という数学の理論が生まれました。

２つの対象が等しいことについて、複数の異なる根拠を見出す理論です。

この理論のもとでは、構造が同じものは等しいと言えるようになります。２つの群が同型なら、区別せずに扱ってよい。数学者が慣行として続けてきた扱いに、根拠が与えられます。

そこから、数学の基礎そのものを組み替える構想が生まれました。

**一価的基礎づけ（UF）**といいます。集合論の代わりに、**マーティン＝レーフ型理論（MLTT）**の上に数学を築き直す試みです。

ここに、思わぬ一致があります。

UF が土台に選んだ MLTT は、定理証明支援系が数学の定理の検証に使い続けてきた型理論と、同じものだったのです。

Rocq、Agda、Lean 4、Idris 2。いずれもこの理論を土台にしています。

そして2026年、AI が数学の定理の証明を書き、定理証明支援系がそれを検証する時代が始まりました。

図の下半分 ── HoTT を、どう取り込むか

既存の定理証明言語も、新しい数学理論である HoTT を扱えるようになろうとする動きが出てきました。

Rocq（旧 Coq）は、Coq-HoTT と UniMath という２つのライブラリによって HoTT を扱えるようになっています。UniMath は、HoTT の提唱者であるヴォエヴォドスキー自身が2010年に始めたものです。

しかし、これらはどれも、後付けの対応でした。

HoTT の主張を、**証明抜きに正しいものとして認める。**数学の言葉でいえば、公理として扱うということです。

公理には、計算規則が伴いません。「こういうものが存在する」と宣言するだけで、それを使った式をどう計算するかが定められていないのです。

なお、すべての定理証明支援系が HoTT を扱えるわけではありません。

Lean には、かつて HoTT を扱うモードがありました。
しかし Lean 3 以降で廃止され、現行の Lean 4 は HoTT に対応していません。

ここで、Arend が登場します。
2019年に公開された、定理証明支援系の分野の新参者です。

Arend は、HoTT の主張を公理としてではなく、計算して成立を確かめる対象として扱います。

より正確を期すならば、次のように述べるべきです。

Arend は、HoTT に関わる 一部の構成 を、計算内容のない公理として追加するだけでなく、計算的簡約規則を伴う形で扱います。

ただし、Cubical Agda のように一価性そのものを計算可能にした体系とは異なります。

Arend の設計は、計算可能性と、理論・実装の複雑さとのあいだに置かれた、別の選択肢です。

図の末端 ── １つの難点と、３つの可能性

Arend は、正準性という性質を持ちません。

書いた式が必ず具体的な値まで計算される、という性質です。それを持たないため、計算の途中で止まる式が残ります。

それでもなお、３つの可能性があります。

第１に、HoTT の一部の構成に、計算的簡約規則を与えられること。
公理として足す場合よりも、多くの式が計算できます。

第２に、構造の階層を柔軟に組めること。
モノイド、群、環、体。数学の構造の積み上げを、そのままコードに写せます。

第３に、証明を持ち回らずに済むこと。
Agda や Lean では引数として運び続ける必要のある証明が、Arend では型そのものに含まれています。

---

本記事の全体像 ── HoTT から Arend まで

ホモトピー型理論 という、2006年に産声を上げて、2013年に HoTT Bookという体系的な理論書が刊行されたばかりの新しい数学の理論があります。

この理論の特徴は、２つの対象を空間の中の２つの点として捉えるところにあります。

そして、２つの対象が「等しい」ということを、その２点を結ぶ経路として表現します。

このとき、２点のあいだを形状の異なる複数の経路で結ぶことができれば、２つの対象のあいだに、複数の異なる「等しさの根拠」を見出したことになります。

具体例をお見せします。

真偽値の型 Bool を考えてください。

Bool と Bool は、当然ながら等しいです。

しかし、その「等しさ」の根拠は、１つだけではありません。

少なくとも、以下のように２つの異なる根拠を、考えることができるのではないでしょうか。

	何も変えずに対応させる	論理反転して対応させる
対応づけ	true → true false → false	true → false false → true
比較するもの	true と true false と false	false と false true と true
結果	同じ	同じ

どちらも「Bool と Bool は等しい」ことの根拠です。

対応のつけ方が、２通りあります。

true と false を、元の値のまま比べる対応づけ と、
両者を論理反転した結果どうしを比べる対応づけ の ２つの対応付け です。

どちらも、Bool の要素と Bool の要素を過不足なく一対一に対応づけていますので、 いずれも「Bool と Bool は等しい」ことの根拠となります。

しかし、対応のつけ方そのものは別物 です。

等しさの根拠が、２つ存在する ことになります。

従来の型理論では、この区別ができませんでした。

等しいなら等しい。根拠は１通りに潰れていた のです。

ここまでの議論を数学的により厳密に述べてみましょう。

ここでいう「対応づけ」は、単なる全単射ではなく、型の 同値（equivalence）を指します。

Bool には、自分自身への同値が少なくとも２つあります。

１つは true と false をそのまま保つ 恒等写像、
もう１つは 両者を入れ替える否定写像 です。

通常の集合論 では、これらは「同じ集合の上の異なる写像」でしかありません。

しかし、一価性を採用する HoTT では、型の同値 Bool ≃ Bool が、型の等しさ Bool = Bool の経路に対応します。

したがって Bool = Bool には、恒等写像に由来する経路 と、否定写像に由来する経路 という、異なる経路が存在しうる のです。

なお、複数の経路が現れるのは、値としての Bool の内部ではありません。

Bool という型を要素として含む宇宙において です。

この点は、記事の後半であらためて扱います。

ところで、ホモトピー理論については、筆者の過去の記事も参考になるかと思います。

• 【連載初回】「型」を「空間」として捉え、「2点を結ぶ経路」の数だけ「異なる等しさ」を識別するホモトピー型理論（HoTT）は、数学と情報科学にどう役立つのか
   
• 【連載第2回】「複数の等しさ」を扱う2つの流派 ── ホモトピー型理論（HoTT）と ∞-圏論のあいだに双方向の橋が開通する日はくるか？（片側車線のみ開通済み）

また、「等しさ」を、関数型言語や定理証明支援言語の「型」としてどこまで宣言できるかという問いを主題に掲げた上で、Python から定理証明支援系言語までを横断して論じた記事も公開済みです。

• 「等しさ」はどのレベルまで型として宣言し、型検査できるか？ ── Pythonから関数型言語・定理証明言語へ

本連載シリーズは、上記の記事群をお読みいただかなくても、理解いただけるように心がけて執筆して参ります。

本論に戻ります。

複数の等しさを数学の言葉で区別できると、何が変わるのでしょうか？

（１つ目）「同型なものは等しい」と言えるようになる

数学者は昔から、構造が同じものを、同じものとして扱ってきました。

ここでいう 群 とは、足し算や掛け算のような演算を１つ持ち、その演算について一定の規則が成り立つ集まりのことです。整数と足し算の組み合わせが、その典型です。

２つの群が 同型 であるとは、名前を付け替えただけで、中身の構造がそっくり重なる ということです。

要素どうしを過不足なく対応させられて、しかも演算の結果まで一致する。
そういう関係を指します。

同型なら、区別せずに扱う。 数学者は、そうしてきました。

しかし従来の集合論では、この慣行を正当化できませんでした。
同型な２つの群も、集合としては違うものだから です。

ホモトピー型理論 は、これを 構造同一原理 として支えます。

同型な群、同型な位相空間は、等しいものとして扱うことができます。
（なお、位相空間 というのは、点の集まりに「近さ」の情報を添えたものです。どの点とどの点が近いかが決まっている、そういう構造をご想像ください）

こうした事情を背景に、数学の基礎そのものを組み替える試みが始まりました。

19世紀末から20世紀初頭にかけて、数学は集合論の上に基礎づけられました。

カントールが集合の理論を築き、ツェルメロらが公理系を整え、現在、ZFCと呼ばれる体系 ができあがります。

それ以来、集合論は数学の共通の土台であり続けてきました。

近年、その土台を型理論に置き換えようとする動き が出てきています。

1970年代にペール・マーティン＝レーフが提唱した マーティン＝レーフ型理論 の上に、数学を築き直そうという構想です。

この試みは、2012年から2013年にかけて、国際的な共同研究として本格的に動き始めました。

かつてアインシュタインや、数理論理学の世界で（第１・第２）不完全性定理を提唱したゲーデルらが在籍したことで知られるアメリカのプリンストン高等研究所が、数学の基礎をマーティン＝レーフ型理論の上に築き直すという構想を主題とする特別年を設けたのです。

出典
Special Year on Univalent Foundations of Mathematics, Institute for Advanced Study, 2012–2013 https://www.ias.edu/math/sp/univalent

世界各地から研究者が集まり、その成果は2013年、一冊の教科書としてまとめられました。執筆は GitHub 上で共同で行われています。

出典
The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013 https://homotopytypetheory.org/book/ リポジトリ：https://github.com/HoTT/book

定理証明の言葉に置き換えると

ここまでの話を、証明を書く側の視点に移してみます。

「複数の等しさ」 は、証明の言葉に置き換えると、 「ある主張が成り立つ根拠が、複数ありうる」 ということになります。

そして、HoTT の主張を定理証明支援系に取り込むとき、その扱い方で設計が分かれます。

第１の道は、検証抜きに正しいものとして受け取ることです。

数学では、証明抜きに正しいと認める前提を 「公理」（axiom） と呼びます。

第２の道は、証明式を実際に計算し、結論までたどれるかを確かめることです。

数学の言葉でいえば、「構成的に」検証する ということになります。

この違いが、Arend と既存の定理証明言語の立ち位置を分けています。

RocqのHoTTライブラリ や、通常のAgda は、第１の道 を採ります。
Arend は、第２の道を採りました。

なお、Agda に 立方体型理論 を組み込んだ Cubical Agda も、第２の道 を採っています。

同じAgda であっても、--cubical オプションを付けるかどうかで立ち位置が変わります。

Arend とCubical Agdaとの違いは、どこまで計算しきれるかにあります。
この点は、本連載の第２回で、「正準性」を巡る論点として取り上げます。

立場	処理系
公理として扱う	Rocq 上の HoTT ライブラリ（Coq-HoTT、UniMath）、通常の Agda
計算対象として扱う	Arend、Cubical Agda

なお、Cubical Agda については、筆者が過去に公開済みの記事も適宜、ご参考になさってください。

• Cubical Agda とは何か ── 複数の「等しさ」を証明できる言語は、なぜビジネス事例がほぼ無いのに注目されるのか

さて。

根拠を区別できると、具体的に何ができるようになるのでしょうか？

本連載シリーズの次回記事（第２回目）では、移送、商型、関数外延性 の ３つの題材 を事例に選んで詳しく見ていきます。

集合論から型理論へ ── 数学をその上に基礎付ける土台そのものを移す試み

2006年ごろから、数学者たちは、長らく集合論に立脚してきた数学を、型理論に立脚した数学へ作り替える地道な努力を積み重ねています。

この試みは、ヴォエヴォドスキーというフィールズ賞受賞者によって 「一価的基礎づけ」（Univalent Foundations、以下 UF と略記します）と名づけられました。

一体なぜ、そのような大掛かりなことをしはじめたのでしょうか。

理由の１つは、いま見た「同型な群、同型な位相空間は、等しいものとみなす」という扱いが、集合論をもとにした数学ではきわめて難しい ことにあります。

ヴォエヴォドスキーと書簡を交わしていた Andrei Rodin は、この点についてこう記しています。

（原文引用）

Vladimir, of course, appreciated the fact that UF helped to make the conventional informal mathematical talk about the "equality up to isomorphism" formally justified and logically rigorous.

（筆者による日本語訳）

ヴラジーミルはもちろん、UF が「同型を除いた等しさ」についての通常の非形式的な数学の語りを、形式的に正当化し、論理的に厳密にする助けとなったという事実を高く評価していた。

出典
Andrei Rodin, "Vladimir Voevodsky on the concept of mathematical structure in his letter exchange with Andrei Rodin", arXiv:2409.02935, 2024年
https://arxiv.org/abs/2409.02935

引用文にある 「同型を除いた等しさ」 とは、先ほど見た「名前を付け替えただけで、中身の構造がそっくり重なるなら、同じものとみなす」という扱いを指します。

数学者は、この扱いを慣行として続けてきました。しかし、その慣行を基礎の側から裏づける枠組みがなかったのです。

UF ── Univalent Foundations、一価的基礎づけ ── は、その裏づけを与えるものでした。

動機は、これだけではありません。

数学の基礎付けの土台を、集合論から型理論へと移す試みが始まった２つ目の理由は、
集合論による数学の形式化が、扱いにくいものになりがちだという認識です。

ヴォエヴォドスキー自身の言葉を引用しましょう。

（原文引用）

Whilst it is possible to encode all of mathematics into Zermelo-Fraenkel set theory, the manner in which this is done is frequently ugly; worse, when one does so, there remain many statements of ZF which are mathematically meaningless. This problem becomes particularly pressing in attempting a computer formalization of mathematics; in the standard foundations, to write down in full even the most basic definitions — of isomorphism between sets, or of group structure on a set — requires many pages of symbols.

（筆者による日本語訳）

数学のすべてをツェルメロ＝フレンケル集合論へ符号化することは可能だが、その方法はしばしば醜い。さらに悪いことに、そうしたとき、数学的に無意味な ZF の言明が数多く残ってしまう。この問題は、数学を計算機で形式化しようとするとき、とりわけ切実になる。標準的な基礎づけのもとでは、最も基本的な定義でさえ ── 集合のあいだの同型や、集合上の群構造の定義でさえ ── 完全に書き記すには何ページもの記号を要する。

出典
Andrei Rodin, "Axiomatic Method and Category Theory", arXiv:1210.1478, §6.10（ヴォエヴォドスキーの記述を引用）
https://arxiv.org/abs/1210.1478

「何ページもの記号を要する」という指摘です。

紙の上で数学を書くぶんには、そこまで困りません。

しかし、機械に検査させる形で書こうとすると、この負担が一気に表面化します。

数学の基礎づけの土台を集合論から型理論へと移す試みが始まった３つ目の理由は、
証明の再利用という問題 です。

集合論をもとにした数学の形式化 では、たとえ２つの構造が同型であったとしても、一方について証明したことを他方へ持ち込むには、その都度あらためて証明し直す必要がありました。

この点、UF のもとでは、UF という数学の基礎づけの枠組みそのものが、その持ち込みを可能にします。

２つの構造が同型であることさえ示せば、一方について証明したことを、他方でもそのまま使えるのです。

この仕組みについては、本連載の第２回で扱います。

UF が土台に選んだ型理論

UF は、集合論の代わりに型理論の上で数学を組み立てる試みです。

そして、その 型理論 とは、マーティン＝レーフ型理論**（Martin-Löf Type Theory、以下 MLTT と略記します）** のことです。

1970年代にスウェーデンの数学者ペール・マーティン＝レーフが提唱したもので、型が値に依存できる という特徴を持ちます。

Vector Int 3

のように、「長さ3の整数のベクトル」という型を宣言することができます。
3 という値が、型の一部になっています。

Haskell の型システムには、値を型に埋め込む仕組みがありません。

この仕組みを、依存型と呼びます。

より正確を期すならば、次のように述べるべきです。

標準的な Haskell の型システムは、MLTT の意味での全面的な依存型を備えているわけではありません。

GHC の拡張には型レベル自然数などの近い機構もありますが、Vector Int 3 のような添字付きデータを依存型理論と同じ一般性で扱う仕組みとは区別されます。
ヴォエヴォドスキー自身が、次のように述べています。

（原文引用）

Univalent foundations seeks to improve on this situation by providing a system, based on Martin-Löf's dependent type theory, whose syntax is tightly wedded to the intended semantical interpretation in the world of everyday mathematics.

（筆者による日本語訳）

一価的基礎づけは、マーティン＝レーフの依存型理論に基づく体系 ── その構文が、日常の数学の世界における意図された意味論的解釈と緊密に結びついた体系 ── を提供することで、この状況の改善を目指す。

出典
Andrei Rodin, "Axiomatic Method and Category Theory", arXiv:1210.1478, §6.10
https://arxiv.org/abs/1210.1478

定理証明支援系による数学定理の証明の検証との接点

ところで、型が値に依存できるマーティン＝レーフ型理論（MLTT）は、そもそも計算機での実装に適した理論として発展してきたもの です。

後ほど登場する Rocq、Agda、Lean 4、Idris 2 といった定理証明支援系は、いずれも MLTT かその近縁の体系を土台にしています。

つまり、数学の基礎づけの土台として UF が選んだマーティン＝レーフ型理論（MLTT）は、定理証明支援系が数学定理の証明の正しさを検証するために使い続けてきた型理論（MLTT）と、同じものだったのです。

より数学的に正確を期すならば、次のように述べるべきです。

本記事の書き方	より正確な言い方
UF が土台に選んだのは MLTT	UF は、依存型理論、とくに MLTT 系の型理論を基盤とし、一価性・高次帰納的型などを取り込んで数学を基礎づけようとする構想である
Rocq、Agda、Lean 4、Idris 2。いずれもこの理論を土台にしています	Rocq、Agda、Lean、Idris はいずれも依存型理論の系譜に属するが、採用する中核理論・論理・宇宙階層・計算規則は同一ではない
同じ MLTT を土台にしている	MLTT と近縁の依存型理論を共有する系譜にある

UF は、素朴な意味での MLTT そのものではありません。

そして Rocq、Agda、Lean、Idris も、同一の理論を共有しているわけではないのです。

本記事は Arend の理論設計が他とどう違うかを論じるものですから、各処理系の土台が厳密には同一でないことを、ここで認めておきます。

この一致には、理由があります。

プリンストン高等研究所は、2012年から13年にかけて UF を主題とする特別年を設けました。その研究計画の位置づけが、次のように記されています。

（原文引用）

This research program was centered on developing new foundations of mathematics that are well suited to the use of computerized proof assistants as an aid in formalizing mathematics.

（筆者による日本語訳）

この研究計画は、数学を形式化する際の助けとして計算機による証明支援系を用いることに適した、数学の新しい基礎づけを発展させることを中心に据えていた。

出典
Special Year on Univalent Foundations of Mathematics, Institute for Advanced Study, 2012–2013
https://www.ias.edu/math/sp/univalent

「証明支援系の利用に適した基礎づけ」を作ること。

この記述が示すとおり、証明支援系との接続は、当初から目的の一部に含まれていたのです。

ヴォエヴォドスキーによる定理証明支援系を用いた数学の形式化

※ 画像中のコードはイメージとして捉えて下さい。コードとしては意味を成しません。

ヴォエヴォドスキーは2010年2月、Coq（当時。現在のRocq）を用いて UF に基づく数学ライブラリの構築に着手しています。

（原文引用）

I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models.

（筆者による日本語訳）

私は2010年2月にこのライブラリの作業を始めた。一価的モデルから得た直観に基づく構成的型理論において、数学を形式化する経験を得るためである。

出典
Vladimir Voevodsky, "An experimental library of formalized Mathematics based on the univalent foundations", Mathematical Structures in Computer Science, vol. 25, no. 5, 2015, pp. 1278–1294, doi:10.1017/S0960129514000577
https://arxiv.org/abs/1401.0053

このライブラリは Foundations と名づけられ、2014年に他の２つのリポジトリと統合されて UniMath となりました。

現在も開発が続いています。

出典
UniMath — a computer-checked library of univalent mathematics
https://github.com/UniMath/UniMath

ここまでを整理します

• HoTT は、複数の異なる等しさを扱える理論である

 

• UF は、HoTTの上に数学の基礎を築き直す試みである

 

• UF が土台に選んだのは、MLTT という型理論である

 

• 定理証明支援系 も、同じ MLTT を土台にしている

 

• したがって、UFという基礎付けの上に立脚する数学について、その数学の定理が成立しているのか、成立していないのかは、定理証明支援系によって検証可能である

MLTT が、２つの流れの合流点になっています。

集合論の上に数学を組み立てると、数学の定理を定理証明支援系に検証させる際に、膨大な量の記号を書き並べることになります。

型理論の上で組み立てれば、書いたものがそのまま定理証明線形による検査の対象になります。

AI が証明を書く時代の到来

※ 画像中のコードはイメージとして捉えて下さい。コードとしては意味を成しません。

2026年8月、Anthropic が Claude による数学の成果を公開しました。

リーマン予想に関連する未解決問題について、これまで人間の数学者が示せた記録を大きく更新したのです。

その証明が正しいことを確かめたのは、Lean 4 という言語でした。

同じ月、OpenAI も10件の数学的成果を公開しています。そちらも、Lean で形式化されていました。

AI が証明を書き、機械がその正しさを検査する。

そういう時代が、すでに始まっているのです。

この流れについては、筆者が連載記事で詳しく扱いました。

• AIが数学の証明を書けるようになった6年間 ── Neural Theorem Proving の全体像

定理証明支援系とは何か（再掲）

※ 画像中のコードはイメージとして捉えて下さい。コードとしては意味を成しません。

すでに触れた定理証明支援系について、ここであらためて解説させてください。

定理証明支援系とは、証明を書くための言語と、その証明を検証する処理系を合わせたものです。

人間が専用の言語で数学の定理の証明を書き、処理系がそれを一行ずつ検証します。論理の飛躍があれば、そこで止まります。

既存の定理証明支援言語による HoTT の取り込み方 ── 公理として扱う

これら定理証明支援言語のうち、いくつかの言語は、冒頭に述べたホモトピー型理論（HoTT）を扱えるようにしようとしています。

ただし、後付けで、HoTTを扱えるようにしている様子が窺えます。

後付け とは、どういうことでしょうか？

HoTTの主張を、議論抜きに正しいものとして前提に置く という取り込み方です。

数学の用語では、証明抜きに正しいものとして扱う前提を「公理」（axiom）と呼びます。

公理には、計算規則が伴いません。

「こういうものが存在する」と宣言するだけであり、それを使った式をどう計算するかが定められていないためです。

（原文引用）

This approach can, in principle, be implemented using an ITP based on MLTT, such as Coq or Agda, by merely appending univalence and higher inductive types as axioms devoid of any computational content. However, this severely impairs the computational properties of MLTT, which are crucial for practical formalization efforts.

（筆者による日本語訳）

この手法は、原理的には Coq や Agda のような MLTT に基づく対話型定理証明系を用いて実装できる。一価性と高次帰納的型を、計算内容を一切持たない公理として単に付け加えればよい。しかし、これは MLTT の計算的性質を著しく損なう。計算的性質は、実際の形式化の作業において決定的に重要である。

出典
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
https://arend-lang.github.io/assets/lang-paper.pdf

HoTT に対応した定理証明支援系の一覧

本記事では Rocq、Agda、Arend を中心に扱いますが、ほかにも実装があります。

なお、以下の表で「通常の Agda」とは、--cubical モードを使わない標準的な Agda を指します。

処理系	HoTT・一価性との関係	計算上の位置づけ
Rocq（旧 Coq）	Coq-HoTT や UniMath では、一価性や高次帰納的型を公理として仮定する形式化が中心	公理として加えた原理については、一般に計算規則を持たない
通常の Agda	--without-K を用いて HoTT 的な形式化を行える。一価性などは通常、追加の仮定として扱う	追加した公理は、一般に計算しない
Cubical Agda	立方体型理論に基づき、一価性を計算規則とともに扱う	一価性を計算可能に扱える
Arend	HoTT Book に近い理論を、独自の計算規則・高次構造・h-type 宇宙とともに実装する	一部の HoTT 的構成で計算規則を持つが、一般的な正準性は保証しない
Lean 2	HoTT モードを持っていた	Lean 3 以降は廃止。現行の Lean は HoTT 非対応
RedPRL	立方体型理論の実装	研究用
redtt	デカルト立方体型理論の実装	開発は停止しているとみられる
cooltt	redtt の後継	実験的
cubicaltt	立方体型理論の最初の実装	探索用のため、証明支援系としては未整備
yacctt	デカルト立方体型理論の型検査器	研究用

--without-K について、一点だけ補足します。

このフラグは HoTT 的な開発を可能にする重要な設定ですが、それ自体が一価性や高次帰納的型を実装するものではありません。 等しさの証明が一意であるという仮定を外すだけです。

なお、nLab は Arend について次のように記しています。

（原文引用）

Arend implements a theory that enhances Book HoTT with an interval type similar to that of cubical type theory, but without the extra structure necessary to make univalence computational.

（筆者による日本語訳）

Arend は、立方体型理論のものと似た区間型によって HoTT Book の理論を拡張した体系を実装している。ただし、一価性を計算可能にするために必要な追加の構造は持たない。

そして Lean については、こう記されています。

（原文引用）

Current versions of Lean (3 and now 4) have UIP built-in and are not HoTT-compatible, but the old Lean 2 had a HoTT mode.

（筆者による日本語訳）

現行の Lean（3 および 4）は UIP を組み込んでおり、HoTT と両立しない。ただし、旧来の Lean 2 には HoTT モードがあった。

出典
formalized libraries of homotopy type theory, nLab
https://ncatlab.org/nlab/show/formalized+libraries+of+homotopy+type+theory

Arend 登場

この文脈の中で、2019年8月 に Arend が公開されました。

Arend は、HoTTの主張を 「公理」としてではなく、具体的に計算することで、その主張が成立するのか、しないのかを構成的に確かめるべき対象としてとり扱う 言語です。

検証不要の公理や前提としてではなく、検証すべき対象として HoTT を扱う。

この点で、これまでの定理証明支援系とは立ち位置を大きく異にします。

より数学的に正確を期すならば、次のように述べるべきです。

Arend は、一価性や高次帰納的型に関わる 一部の項 について、計算的な簡約規則を中核理論に備えています。

そのため、これらを計算内容のない公理として追加する場合よりも、型検査や定義的等号の判定において、式を先へ簡約できる場面が増えます。

ただし、任意の閉じた項が必ず正準形まで評価されるわけではなく、一般的な正準性は持ちません。

構成的型理論であっても、任意の命題について成立するか否かを計算で判定できるわけではありません。 この点は、あらかじめ断っておきます。

（原文引用）

Unlike MLTT augmented merely with axioms for univalence and higher inductive types, Arend's type theory includes a number of computational reduction rules for involved terms, which prove crucial for practical usage.

（筆者による日本語訳）

一価性と高次帰納的型のための公理を単に付け加えただけの MLTT とは異なり、Arend の型理論は、関係する項に対する多数の計算的簡約規則を含む。これらは実用上、決定的に重要であることが判明している。

出典
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
https://arend-lang.github.io/assets/lang-paper.pdf

Arend は何を成し遂げたのか

2026年8月末の現時点では、Arendはまだ、さしたる実績を挙げられていないようです。

標準ライブラリに収められた成果は、いずれも、他の処理系ですでに達成されているもの です。

一例を挙げならば、ホップ束 は 2013年の HoTT Book にすでに 掲載されており、 ブレイカーズ＝マッシー定理 の定理証明支援系による機械証明は、2016年に Agdaを用いて達成されています。

出典
Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine, "A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory", LICS 2016
https://arxiv.org/abs/1605.03227

数学の定理証明問題以外の 産業応用についても同様 です。

Rocq には CompCert という検証済み C コンパイラがあり、Isabelle には seL4 という検証済み OS カーネルがあります。

しかし、Arend には、それに相当する実績がまだないのです。

より正確を期すならば、次のように述べるべきです。

2026年8月末時点で、筆者が確認できた範囲では、Arend には CompCert、seL4、Mathlib のように 広く参照される大規模形式化プロジェクトは、まだ多くありません。

これは Arend の理論的価値を否定するものではありません。

公開からの期間、利用者層、ライブラリ規模、周辺ツールの成熟度が異なることを反映していると考えるべきでしょう。

Arend が公開されたのは、まだ7年前のことです。

Arend が数学研究やその他の実務領域でその真価を発揮し、実績を積み上げていくのは、これからだと思われます。

Arendが抱える難点

ところで、Arendは、正準性という性質を持たない 言語です。

正準性 とは、閉じた項が必ず正準形へ評価されるという性質です。

Python でいえば、2 + 3 と書けば必ず 5 になる、ということです。

自然数は、「自然数の型に属する閉じた項は、すべて zero と successor だけを使って構成されたものと同一である」 と定義することが可能です。

Arendの開発者自身が、公開時に以下のように答えています。

（原文引用）

Does Arend have the canonicity property, i.e. does it evaluate closed expressions to their canonical forms? No, but it computes more terms than ordinary homotopy type theory, which makes it more convenient in many aspects.

（筆者による日本語訳）

Arend は正準性を持つか、すなわち閉じた式を正準形へ評価するか。いいえ。しかし通常のホモトピー型理論より多くの項を計算するため、多くの面でより便利になっている。

出典
New theorem prover Arend is released, Homotopy Type Theory mailing list, 2019年8月6日
https://groups.google.com/g/homotopytypetheory/c/rf6YJB5Omj0

正準性を持たないことは、弱みなのか

正準性を持たないことは、弱みと受け取るべきです。

正準性とは、書いた式が必ず具体的な値まで計算されるという性質です。

Arendがこの正準性を持たないということは、計算の途中で止まったまま、具体的な値にたどり着かない式が残るということです。

より数学的に正確を期すならば、次のように述べるべきです。

正準性とは、典型的には 「閉じた自然数型の項が、zero と後続子からなる数値の形まで評価される」 という性質を指します。より一般には、データ型の閉じた項が、対応する正準的な値へ到達することを保証する性質です。

どんな閉じた式も必ず具体的な値になる、という一般化ではありません。

そして、正準性がないことの帰結も、次の程度に述べるのが安全です。閉じたデータ型の項であっても、期待する正準形へ簡約できない場合があり、証明から計算結果を取り出す用途では制約になりうる。

Coq や Agda で数学を形式化する人々が「計算的性質は決定的に重要である」と述べているのは、このあたりの事情を取られた発言です。

ただし、これは、程度の問題として捉える必要があります。

	HoTT の扱い	計算できるか
Coq / Agda（公理として追加）	公理	ほとんど計算できない
Arend	計算規則を伴う	多くの式が計算できる。ただし完全ではない
Cubical Agda	完全に計算可能	すべて計算できる

Arend は、この３つのうち真ん中に位置しています。

公理として足す場合よりは計算できる。しかし、Cubical Agda ほどではない。

計算しきれない項が残るということは、書いた証明を、そのまま実行可能なプログラムとして取り出せない場合がある ということを意味します。

（ 参考 ）
なお、Cubical Agda については、筆者が別の記事で詳しく扱っております。よろしければご参照ください。

• Cubical Agda とは何か ── 複数の「等しさ」を証明できる言語は、なぜビジネス事例がほぼ無いのに注目されるのか

Arend が持つ、３つの大きな可能性

Arendには、広く知られた成果や利用実績が、筆者の調べた範囲では見当たりませんでした。
さらに、正準性という難点も抱えています。

それでもなお、Arend には３つの可能性があります。

第１の可能性 ── HoTT の一部の構成に、計算的簡約規則を与えること

これが、この記事の冒頭から述べてきたことです。

HoTT の主張を公理として受け取る場合でも、証明を書くことはできます。

しかし、その証明を実際に走らせると、途中で止まります。

なぜ、止まってしまうのでしょうか？

その理由は、公理は「これは正しいものとする」と宣言するだけで、その先をどう計算するかを定めていないから です。

Arend の場合、HoTT の主張を計算するための規則が、言語そのものに組み込まれています。

そのため、証明を最後まで計算し、具体的な値を取り出すことが可能なのです。

より正確を期すならば、こうなります。

Arend では、公理追加型の形式化よりも 簡約を進められる場面があります。 ただし、すべての閉じたデータ項が正準形へ到達するわけではありません。

その結果、Arendは、具体的に何ができるようになるのでしょうか？

本連載の第２回目の記事では、移送、商型、関数外延性 の３つを取り上げて、具体的にArendができることを、解説致します。

第２の可能性 ── 構造の階層を、柔軟に組めること

数学の構造は、階層をなしています。

モノイド、群、環、体。下の構造に条件を加えて、上の構造ができあがります。

構造	何を持つか	身近な例
モノイド	演算と単位元	文字列と連結（単位元は空文字列）
群	モノイド ＋ 逆元	整数と足し算（逆元は符号を変えたもの）
環	群 ＋ もう１つの演算	整数と、足し算・掛け算
体	環 ＋ 除算	有理数、実数

上の表 は、階層の感覚をつかむための略記です。

より数学的に正確を期すならば、それぞれ次のように定義されます。

構造	正確な定義
群	モノイドであって、その演算についてすべての要素が逆元を持つもの
環	加法について可換群、乗法についてモノイドであり、分配法則が成り立つもの
体	零でない元がすべて乗法逆元を持つ可換環

この階層を、そのままコードとして書けるでしょうか。

公式論文は、既存の処理系の設計をこう述べています。

（原文引用）

The development of major theorem provers from MLTT family such as Lean, Coq and Agda has been avoiding subsumptive subtyping and manifest fields in the core theory thus making record types the same as sigma types.

（筆者による日本語訳）

Lean、Coq、Agda といった MLTT 系の主要な定理証明系の開発は、中核理論において包摂的部分型付けと顕在フィールドを避けてきた。その結果、レコード型はシグマ型と同じものになっている。

出典
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
https://arend-lang.github.io/assets/lang-paper.pdf

Arend は、この道を選びませんでした。

実際に、モノイドと群を書いてみます。

\class Monoid (E : \Set0)
  | ide : E
  | \infixl 7 * : E -> E -> E
  | ide-left (x : E) : ide * x = x
  | ide-right (x : E) : x * ide = x
  | *-assoc (x y z : E) : (x * y) * z = x * (y * z)

\class Group \extends Monoid
  | inverse : E -> E
  | inverse-left (x : E) : inverse x * x = ide

型検査は通ります。

$ java -jar Arend.jar G5.ard

--- Typechecking \default ---
[ ] src.G5
--- Done (110ms) ---

コードを読み解きます。

\class Monoid (E : \Set0) の E が、台となる集合です。
ide が単位元、* が二項演算にあたります。

そして ide-left 以下の３行に注目してください。

これらは値ではなく、法則そのものです。
単位元律と結合律が、クラスのフィールドとして書かれています。

Haskell では、法則をドキュメントに書くことしかできませんでした。
Arend では、法則がクラスの一部 です。

そして \class Group \extends Monoid の一行で、群がモノイドの拡張として定義されます。

さらに、同じ定義が３通りに読めます。

\func t1 : \Type => Monoid                 -- モノイドの型
\func t2 : \Type => Monoid Nat             -- Nat 上のモノイド構造の型
\func t3 : \Type => Monoid Nat 1 (Nat.*)   -- 1 と * がモノイドをなす証明の型

この３行も、型検査を通ります。

引数をどこまで書くかによって、意味が変わるのです。

何も書かなければモノイド全体の型、
台を指定すればその上の構造の型、
演算まで指定すれば証明の型

になります。

Haskell で型クラスを設計するときの「型引数にするか、フィールドにするか」という判断が、そもそも生じません。

引用文に出てきた包摂的部分型付けと顕在フィールドについては、本連載の第３回で扱います。

第３の可能性 ── 証明を持ち回らずに済むこと

Agda や Lean では、ある型が集合であることを使いたいとき、その証明を引数として関数から関数へ渡し続ける必要があります。

この点、Arend では、ある型が集合であるという情報が、その型の宣言そのものに含まれています。

理由は、Arend の「宇宙」の設計にあります。

宇宙とは、型を集めたものです。
Int や Bool といった型そのものを、値として扱うための入れ物だとお考えください。

そして、宇宙は階層をなしています。

Agda や Lean では、その階層が Type 0、Type 1、Type 2 と、１つの数で並んでいます。

この数が表すのは、階層の何段目かという位置だけです。

ちょっと抽象的でわかりづらいですね。
どういうことなのか、少し腰を据えて説明してみたいと思います。

プログラムでは、すべての値に型が付きます。

true という値の型は Bool です。3 という値の型は Int です。

では、Bool そのものに型は付くのでしょうか。

依存型を持つ言語では、型そのものを関数の引数として渡すことができます。
つまり Bool は、値として扱われるのです。

値である以上、型が必要になります。その型を Type 0 と書きます。

そして Type 0 にも、型が必要です。

Type 0 自身をその型とすると、体系に矛盾が生じることが知られています。そこで、１つ上に Type 1 を用意します。

書き方	読み方
true : Bool	値 true の型は Bool
Bool : Type 0	型 Bool の型は Type 0
Type 0 : Type 1	Type 0 の型は Type 1
Type 1 : Type 2	Type 1 の型は Type 2

この積み上げが、限りなく続きます。

Type のあとに付く数字は、この積み上げの何段目かを表しているだけです。

Arend では、もう１つの数が加わります。

第２の数が表すのは、その宇宙に属する型において、等しさの根拠が何本ありうるか です。

この記事で解説した「２点を結ぶ経路」の本数にあたります。

Arend では、宇宙を \0-Type0 のように、２つの数で指定します。

最初に登場する 0 が、等しさの根拠が何本ありうるかを表示しています。

次に登場する 0 は、先ほど見た積み上げの何段目かを表しています。

\Set0 という表記も可能です。
これは、\0-Type0 の略記になります。

Set という語が、「等しさの根拠は高々１本」という情報を担っています。

より正確を期すならば、２つの添字は次のように整理できます。

位置	何を表すか
\0-Type0 の左側の 0	ホモトピーレベルに関する添字
Type0 の右側の 0	宇宙階層の添字

そして \Set0 は、集合レベルに制限した宇宙を表す略記です。

なお、「等しさの根拠が何本ありうるか」という言い方は、少し直接的にすぎます。

ホモトピーレベルは、単純に経路の本数を数える添字ではありません。n-truncated であること、すなわち等しさの反復がどの段階で命題になるか、という性質に関わります。

より慎重に述べるなら、こうなります。左側の添字は、その宇宙に属する型の等しさが、どこまで高次の構造を持ちうるかを制限するための添字です。

ここで、Agda や Lean との違いが表れます。

Agda や Lean の宇宙は、大きさを表す数しか持ちません。
「等しさの根拠が何本ありうるか」を、型の側に書く場所がないのです。

そのため、Agda や Lean では、「この型については、等しさの根拠が高々１本しかない」という事実を、証明として別に用意することになります。

これらの言語では、証明は値です。
数や文字列と同じように、変数に入れたり、関数の引数として渡したりできます。

Haskell の型シグネチャと並べてみます。

Haskell で、Eq a という制約を付けた関数を書いたことがあるかもしれません。

member :: Eq a => a -> [a] -> Bool

Eq a => の部分は、「型 a は等値比較ができる」という条件です。

この条件は、コンパイラが自動で解決します。
プログラムを書く側が、何かを渡す必要はありません。

Lean では、事情が違います。

-- 「この型は、等しさの根拠が高々１本しかない」という性質
def IsSet (A : Type) : Prop := ∀ (x y : A) (p q : x = y), p = q

-- その性質を前提にする関数。h が、証明を受け取る引数
def f (A : Type) (h : IsSet A) (x y : A) (p q : x = y) : p = q :=
  h x y p q

-- f を呼ぶ関数。受け取った h を、そのまま f へ渡す
def g (A : Type) (h : IsSet A) (x y : A) (p q : x = y) : p = q :=
  f A h x y p q

-- g を呼ぶ関数。ここでも h を渡す
def i (A : Type) (h : IsSet A) (x y : A) (p q : x = y) : p = q :=
  g A h x y p q

型検査は通ります。

h : IsSet A に注目してください。３つの関数すべてが、この引数を持っています。

そして f A h x y p q のように、次の関数を呼ぶたびに h を書いて渡しています。

関数が増えれば、そのすべてに h が付いて回ります。
これが「証明を持ち回る」ということです。

Arend では、\Set0 と書いた時点で、この情報が型に含まれています。

同じ３つの関数を、Arend で書いてみます。

-- Lean の３関数チェーンに対応する Arend のコード
-- 証明を受け取る引数が、どこにもない

\func f (A : \Set0) (x y : A) : \Prop => x = y

\func g (A : \Set0) (x y : A) : \Prop => f A x y

\func h (A : \Set0) (x y : A) : \Prop => g A x y

型検査の結果です。

$ java -jar Arend.jar G4.ard

--- Typechecking \default ---
[ ] src.G4
--- Done (108ms) ---

通りました。

Lean のコードと見比べてください。

	Lean	Arend
型の宣言	(A : Type)	(A : \Set0)
証明の引数	(h : IsSet A)	なし
次の関数への受け渡し	f A h x y p q	f A x y

\Set0 と書いた時点で、「等しさの根拠は高々１本である」という情報が型に含まれています。

そのため x = y が \Prop に属することを、証明を受け取らずに主張できるのです。

型を見れば「等しさの根拠は高々１本」と分かります。
そのため、証明を引数として持ち回る必要が、そもそも生じない のです。

（原文引用）

This way the universes of h-types behave just like the ordinary ones, but you do not need to carry proofs that a type belongs to a certain homotopy level.

（筆者による日本語訳）

これにより、h-型の宇宙は通常のものと同じように振る舞うが、ある型があるホモトピーレベルに属することの証明を持ち回る必要がない。

出典
Arend features, Arend Documentation
https://arend-lang.github.io/documentation/getting-started/arend-features

訳文にある ホモトピー と ホモトピーレベル について、補足します。

ホモトピー とは、もともと図形を扱う数学の言葉です。ある経路を、切ったり貼ったりせずに、連続的に変形して別の経路に移せるか を問うものです。

輪ゴムを想像してください。平面の上に置いた輪ゴムは、縮めて一点にまとめられます。しかし、ドーナツの穴に通した輪ゴムは、一点にまとめられません。

この違いを調べる分野が、ホモトピー論です。

そして HoTT では、等しさの根拠を経路として捉えました。したがって、経路についての議論が、そのまま等しさについての議論になります。

ホモトピーレベル は、その等しさがどこまで複雑になりうるかを表す数です。

番号を追うより、呼び名で捉えるほうが分かりやすいでしょう。

呼び方	直感	例
命題（proposition）	証明があれば、その証明どうしの区別は問題にしない	「この数は偶数である」
集合（set）	要素の等しさの証明は、実質的に一意	自然数、文字列、通常の Bool の値
高次の型	等しさの証明自体にも、非自明な構造がある	型を要素として含む宇宙、空間やグルーポイド的な対象

上へ行くほど、等しさの構造は単純になります。

ここで、記事の冒頭で見た Bool の例について、注意すべき点があります。

複数の経路が現れるのは、値としての Bool の内部ではありません。 Bool という型を要素として含む宇宙においてです。

一価性により、Bool の異なる自己同値が、宇宙のなかの Bool = Bool の異なる経路として現れます。

値としての Bool そのものは、上の表でいえば 集合 にあたります。true = true の証拠は、実質的に１通りしかありません。

宇宙を２つの数で指定するという設計は、Cubical Agda にはありません。Arend の特徴的な設計です。

本記事で扱う問い

Arend は、既存の定理証明支援系と、どこがどう異なるのか。

HoTT を扱える他の処理系 ── Cubical Agda や、Rocq 上の HoTT ライブラリ ── と、HoTT 研究でどう競い合っていくことが期待されるのか。

HoTT 研究以外に、どのような場面で、どのような働きが期待される言語なのか。

そして ── HoTT を公理として扱わない Arend は、定理証明支援系による数学の検証にどう貢献しうるのか。

最後の問いについて、いま言えることを述べておきます。

Lean 4 との役割分担

現在、AIと定理証明を結びつける研究の中心は、Lean 4にあります。

Claude も、OpenAI のモデルも、Lean で形式化しました。
Mathlib という巨大な数学ライブラリが、その基盤にあります。

Arend がこの地位を奪うとは考えにくいでしょう。

ライブラリの規模が違いすぎます。
Lean 4 には、大規模な形式化を支える運営組織もあります。

Arend は Lean 4 に取って代わるのではなく、自らに適した領域で力を発揮することが期待されているのではないでしょうか。

では、その領域とはどこでしょうか？

【本記事執筆者の見解】

本記事執筆者は、Arendの活躍の舞台として期待されるのは、構成的な数学の形式化 だと見ています。

Lean の Mathlib は、古典論理を前提に組み立てられています。
排中律 も 選択公理 も、自由に使われます。

ただし、ここは Lean そのものと Mathlib を区別する必要があります。

Lean 自体の依存型理論的な核は、構成的な開発も記述できます。
その一方で、Mathlib は、広範な既存数学を扱う実用上の方針として、古典論理の道具を利用する場面が多いのです。

そのため、計算内容を強く保持した構成的形式化や、HoTT的な等しさを中心に据える研究では、Arend や Cubical Agda が異なる設計上の魅力を持ちます。

排中律 とは、「どんな主張も、正しいか正しくないかのどちらかである」という考え方です。

当たり前に思えますが、「正しい」とも「正しくない」とも示せていない主張について、どちらかだと決めてよいのか。

そう問う立場があります。

選択公理 は、「空でない集まりからは、要素を１つ取り出せる」という主張です。

どれを取り出すのか具体的に示せなくても、取り出してよい と認めるものです。

この２つを使わずに数学を組み立てることを、構成的といいます。

「存在する」と言うためには、実際に作って見せなければ ならない。

そういう立場です。

Arend の標準ライブラリは、そのどちらも使わずに書かれています。

構成的な設定では、古典的に同値な定義が同値でなくなります。

そのぶん、数学の風景が豊かになるのです。

この領域で蓄積を積み上げていくことが、Arend の現実的な進路ではないかと考えます。

Arendが活躍できる舞台は、もう１つあると考えられます。

HoTT を計算対象として扱う体系で、実際にどこまで形式化できるのかを示すこと。

これは、公理として扱う体系にはできない役割 です。

Cubical Agda との比較を通して、二層理論の複雑さが本当に必要なのかを問う立場に、Arend は立っています。

---

本記事全体の見取り図

ここまで述べてきたことを、１つの図にまとめます。

図の読み方を述べます。

青い枠が、出発点です。 2006年に生まれた理論から、すべてが始まります。

金色の枠が、合流点です。 UF が基盤に据えた理論と、定理証明支援系が数学の定理の証明の検証に使ってきた理論が、ここで一致します。

赤い枠が、問題と難点です。 Rocq 上の HoTT ライブラリや通常の Agda が公理として扱うこと、そして Arend が正準性を持たないこと。

緑の枠が、Arend の立ち位置と可能性です。

本記事の読み方

Haskell の型クラスを使ったことがあれば、読み進められるように書きました。

依存型もホモトピー型理論も、一価性公理も、何ひとつご存じない前提です。これらの言葉は、出てくるたびに解きほぐしていきます。

そして、専門用語が出てくる箇所には 対話篇 を置きました。

登場するのは、タロウくん（機械学習に携わるエンジニア）と、専任講師 です。用語につまずいたときは、対話篇を読んでいただければ足ります。

コードは、すべて実機で検証しました。

• Arend 1.10（Java 21）
• GHC 9.4.7
• Lean 4.15.0

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

---

第１部 ── なぜ、Arend という言語が生まれたのか

「本記事の全体像 ── HoTT から Arend まで」 では、HoTT から Arend に至る道筋を駆け足でお伝えしました。

• ホモトピー型理論とは何か
• 一価的基礎づけとは何か
• マーティン＝レーフ型理論とは何か

これらの言葉が、なぜ１本につながるのか？

そのいきさつを、タロウくんの疑問に専任講師が答えていく形で、もう一度たどってみることにしましょう。

登場するのは、機械学習に携わるエンジニアの タロウくん と、型システムと数学の基礎を扱う 専任講師 です。

１ ── 等しさが複数あるとは、どういうことか

タロウくん：
先生、ホモトピー型理論という語を見かけました。
数学の新しい分野だそうですが、何を扱うのですか？

専任講師：
「複数の異なる等しさ」を厳密に扱える理論です。

タロウくん：
等しさが複数ある、というのは、どういう状況ですか？

専任講師：
２つのものが等しいと言うとき、その根拠が１通りとは限らないのです。

タロウくん：
根拠、ですか。

専任講師：
等しさを、空間の中の２点を結ぶ経路として捉えてみてください。
経路が１本しかなければ、根拠は１通りです。

タロウくん：
経路が複数あることもある、ということでしょうか。

専任講師：
そのとおりです。
その場合、その複数の経路を別のものとして識別できるのです。

タロウくん：
・・・従来の数学では、そこを区別しなかったのですか？

専任講師：
等しいなら等しい。それだけでした。

２ ── 同型なものを等しいとみなす、とは

タロウくん：
複数の等しさを区別できると、何が変わるのですか？

専任講師：
「同型なものは等しい」と言えるようになります。

タロウくん：
同型なら等しい、というのは当たり前ではないのですか。
数学者はいつもそうしていると思っていました。

専任講師：
習慣的に毎日行っていること、いわば数学的思考の慣行としては、そのとおりです。

２つの群が同型なら、区別せずに扱ってきました。

タロウくん：
では、何が問題なのですか？

専任講師：
私たちが毎日行っている慣行を、数学を基礎づけている集合論のレベルで正当化するのが難しかったのです。

タロウくん：
どういうことですか？

専任講師：
集合論では、同型であることと、等しいことは別のことなんです。

同型な２つの群も、集合としては違うものです。

タロウくん：
・・・高校生からプロの数学者まで、実務上の慣行として行ってきた思考が、数学の集合論的な基礎付けという数学基礎論のレベルでは、根拠がなかったということですか？

専任講師：
そうです。現在主流の数学では、そういうことになります。

ところが、2006年に登場した新しい数学理論であるホモトピー型理論は、私たちが日々行っている数学的な思考習慣を、構造同一原理 として、数学基礎論のレベルで保証するのです。

３ ── 数学の基礎を作り替えるとは

タロウくん：
先生がいまおっしゃったのは、こういうことですか？

いま主流の数学は、集合論によって基礎付けられるものです。

それに対して、私たちの日々の数学思考の習慣を保証してくれる、新しい数学は、ホモトピー型理論をその基礎付けの土台に持つ数学である

そういうことですか？

もしそうだとしたら、数学基礎論のレベルで、数学の基礎付けの土台を集合論からホモトピー型理論にとりかえようとしている壮大な試み に見えてきますね！

専任講師：
君が見抜いたとおりです。

数学の基礎付けの土台を取り換える試み は、2006年ごろから始まり ました。

この試みは、一価的基礎づけ、略して UF と呼ばれます。
ヴォエヴォドスキーというフィールズ賞受賞者が名づけました。

タロウくん：
集合論をやめる、ということですか？

専任講師：
集合論の代わりに、型理論の上で数学を組み立て直します。

タロウくん：
この試みの動機は、「同型なものを等しいとみなす」ことだけですか？

専任講師：
ほかにもあります。

ヴォエヴォドスキー自身が、集合論による形式化を「しばしば醜い」と述べています。

タロウくん：
醜い、ですか・・・。

専任講師：
集合のあいだの同型を完全に書き記すだけで、何ページもの記号を要すると。

タロウくん：
・・・紙に書くぶんには、そこまで困らないのでは。

専任講師：
機械に検査させようとすると、その負担が一気に表面化します。

４ ── 型理論とは何か

タロウくん：
型理論とは、Haskell の型のようなものですか？

専任講師：
近いものです。

ただし、もっと強力です。
型が値に依存できます。

タロウくん：
値に依存する、というのは、どういうことですか？

専任講師：
Vector Int 3 のように、「長さ3の整数のベクトル」という型が書けます。

タロウくん：
・・・3 という値が、型の中に入っている。

専任講師：
そうです。
依存型 と呼ばれる仕組みです。

タロウくん：
その理論に、名前はあるのですか？

専任講師：
マーティン＝レーフ型理論、略して MLTT といいます。

1970年代に、スウェーデンの数学者ペール・マーティン＝レーフが提唱しました。

５ ── なぜ、その理論が機械での検査に向くのか

タロウくん：
先ほど「機械に検査させる」と仰いましたが、それはどういうものですか。

専任講師：
定理証明支援系 という道具があります。
証明を書くための言語と、それを検査する処理系を合わせたものです。

タロウくん：
数学の定理の証明を、処理系が検証する。

そういえば最近、これまで長年、人間の数学者が証明（反証）できないでいた有名な数学の予想問題や、まだ正しいか間違っているか未検証だった数学の証明式が、定理証明支援系によって証明された、というニュースに触れる機会が増えたように思います。

専任講師：
最新のニュースをしっかりとキャッチしていますね！

まさにそうしたニュースの舞台になっているのが、この道具です。

人間が専用の言語で証明を書き、処理系が一行ずつ確かめる。

論理の飛躍があれば、そこで止まります。

タロウくん：
一行ずつ、ですか。

専任講師：
そうです。

定理証明支援系としては、Rocq、Agda、Lean 4、Idris 2・・・。
いくつも存在します。

これらはいずれも MLTT かその近縁の体系を土台にしています。

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

いま名前を挙げていただいた定理証明支援系が土台にしている理論は、UF が数学の基礎づけのために選んだ理論と、同じものですか？

専任講師：
同じです。

タロウくん：
偶然ですか？

専任講師：
理由があります。

プリンストン高等研究所が2012年に UF の特別年を設けたとき、その研究計画にこう記されています。

「計算機による証明支援系を用いることに適した、数学の新しい基礎づけを発展させることを中心に据えていた」 と。

タロウくん：
・・・ということは・・・最初から、定理証明支援系に検証させることを目的の一部にしていた のですね？

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

そのことは、ヴォエヴォドスキー自身の行動にも表れています。
彼は2010年2月から、Coq でライブラリの構築を始めているのです。

タロウくん：
数学者が、自分でコードを書いたのですか。

専任講師：
「一価的モデルから得た直観に基づく構成的型理論において、数学を形式化する経験を得るため」 と述べています。

そのライブラリは Foundations と名づけられ、いまも UniMath として開発が続いています。

タロウくん：
・・・数学の基礎を作り替えることと、定理証明支援系に検証させることが、最初からつながっていたのですね。

専任講師：
そういうことです。

なぜつながるのかというと、数学の土台の選び方が、数学の定理証明支援系による検証のしやすさをそのまま決めてしまうから です。

集合論の上に数学を組み立てると、数学の定理を定理証明支援系に検証させる際に、膨大な量の記号を書き並べることになります。

しかし、型理論の上に組み立てれば、数学者が書いた証明が、そのまま定理証明支援系による検証の対象になるのです。

そのように言える理由は、はっきりしています。

数学が基礎づけられている土台 も、その数学の定理の証明を検証するときに用いる定理証明支援系 も、どちらも MLTT（マーティン＝レーフ型理論）か、その近縁の型理論に基づいているから です。

６ ── 後付けで組み込む、とはどういうことか

タロウくん：
では、Lean 4 や Agda でも HoTT を扱えるのですか？

専任講師：
扱えます。
ただし、後付けでです。

タロウくん：
後付け、というのは？

専任講師：
HoTT の主張を、議論抜きに正しいものとして 前提に置きます。

タロウくん：
証明せずに、正しいことにする。

専任講師：
数学の用語では、そういう前提を 「公理」 と呼びます。

タロウくん：
それで何か困るのですか？
証明できているなら、それでよさそうですが・・・。

専任講師：
計算が、そこで止まってしまうのです。

タロウくん：
止まる、というのは？

専任講師：
公理には、計算規則が伴いません。

「こういうものが存在する」と宣言するだけで、それを使った式をどう計算するかが定められていない のです。

タロウくん：
・・・証明は書けるが、計算はできない・・・。

専任講師：
Arend の開発チームが書いた論文 Theorem prover Arend は、この状態を「MLTT の計算的性質を著しく損なう」と述べています。

さらに、「計算的性質は、実際の形式化の作業において決定的に重要である」とも。

７ ── 公理ではなく計算するとは、何が違うのか

タロウくん：
Arend では、こうした状況は変わるのですか？

専任講師：
Arend は、HoTT の主張を公理としてではなく、具体的に計算して確かめる対象として扱います。

タロウくん：
計算して、確かめるられるようになるのですね？

専任講師：
そうです。

検証不要の前提、つまり、検証せずに正しいものとして認める 公理としてではなく、検証すべき対象として扱う ということです。

タロウくん：
・・・立ち位置が、根本から違いますね。

専任講師：
公式論文の言葉を借りれば、「一価性と高次帰納的型のための公理を単に付け加えただけの MLTT とは異なり、Arend の型理論は、関係する項に対する多数の計算的簡約規則を含む」となります。

タロウくん：
すると、公理として足す場合よりも、計算が先へ進むのですね。

専任講師：
そういうことです。

ただし、すべての式が計算しきれるわけではありません。
そこが、Arend の抱える難点でもあります。

８ ── 連載の第２回以降で何を扱うのか

タロウくん：
先生、Arend が何を目指した言語なのかは、分かりました。

専任講師：
では、具体的に何が違うのか。

そこが、次回以降の主題になります。

タロウくん：
どういう順序で扱うのですか？

専任講師：
まず、Arend が何を諦めたのかを見ます。

計算対象として扱う道を選んだ結果、正準性という性質 を手放しました。
しかし、失ったものがある反面、Arendが手にしたものもあります。

タロウくん：
その論点は、次回の記事（２回目）で取り上げるのですね？

専任講師：
そうです。

そして第３回以降で、構造の階層、高次帰納的型、宇宙の設計を、それぞれコードとともに扱います。

タロウくん：
構造の階層と宇宙の設計は、本記事でも触れられていましたね。

専任講師：
可能性として、名前を挙げただけです。
短いコードもお見せしましたが、なぜそう書けるのかまでは説明していません。

タロウくん：
高次帰納的型は？

専任講師：
本記事では、名前が出てきただけです。
第４回目の記事で、Haskell の data から説き起こします。

次回以降の記事の流れ（予告）

本連載は、全６回を予定しています。

各回で扱うこと

回	タイトル（予定）	扱う内容（予定）
１ （本記事）	「同型なものは等しい」を機械に検査させる ── 定理証明支援系 Arend が、HoTT を公理としなかった理由	HoTT の起点、構造同一原理、UF と MLTT、機械検査との接続、公理として扱うか計算対象として扱うか、実績と難点
２	「正しいと認める」のをやめた代償 ── Arend が正準性を手放し、Cubical Agda が二層理論を選んだ理由	HoTT の起源とグルーポイド解釈、移送・商型・関数外延性の詳説、正準性とは何か、二層理論とは何か、区間型の扱いの違い、iso による移送の検証
３	数学の構造の階層を、そのままコードに写せるか ── Arend のレコードと、Lean・Coq・Agda が選ばなかった道	型クラスにおける「法則」とは何か、レコード型とシグマ型、包摂的部分型付け、顕在フィールド、匿名拡張、部分実装、多重継承
４	帰納型に条件を付けるだけで、円周が書ける ── Arend の高次帰納的型	一価性公理と高次帰納的型の詳説、Haskell の代数的データ型、帰納型の限界、条件付き帰納型、円周と商型、Cubical Agda との実装上の違い
５	証明を持ち回るか、型に書くか ── Arend の宇宙が２つの数で指定される理由	宇宙とは何か、ホモトピーレベル、Lean との対比コード、証明を持ち回らずに済む仕組み
６	AI による数学証明の機械検証は、「複数の等しさ」を見分ける型理論による数学の基礎づけと Arend によって加速するか	Arend の CLI と arend-skills、Claude Code 連携、Lean 4 との役割分担、キャリア別の学ぶ価値、有向 HoTT への展望、連載の総括

太字にした項目は、本記事で概観だけを述べ、詳細を次回以降へ譲ったものです。

全体の流れ

図の読み方

第１回と第２回が、対になっています。

本記事で「HoTT を計算対象として扱うことで何を得たか」を述べました。第２回では、その代わりに何を手放したのかを掘り下げます。

第３回から第５回までは、並列です。

いずれも本記事で概観した特徴を、それぞれ１回分かけて扱います。どこから読んでいただいても構いません。

第６回が、連載の到達点です。

冒頭に掲げた「複数の等しさ」という主題に、６回分の検証を経て答えを返します。

対話篇 ── 何から読めばよいか

タロウくん：
先生、全部で６回もあるのですね。

専任講師：
主題が多いので、１本にまとめると読み通せる分量になりません。

タロウくん：
順番に読まないと、分からないでしょうか。

専任講師：
そんなことはありません。 各回は、単独でも読めるように書きます。

タロウくん：
とはいえ、興味の持ち方によって、読む順序も変わりそうです。

専任講師：
おっしゃるとおりです。おすすめの入口を、３つ挙げましょう。

Haskell の型クラス設計に関心があるなら、第３回です。

「型引数にするか、フィールドにするか」という、あの悩みが出てきません。その仕組みを扱います。

タロウくん：
本記事の後半で触れられていた話ですね。

専任講師：
言語設計の判断に関心があるなら、第２回です。

何かを得るために、何を手放したのか。Cubical Agda との比較を通して、設計とは何を選ぶことなのかが見えてきます。

タロウくん：
・・・私は、そちらのほうが気になります。

専任講師：
そして、AI と定理証明の接点に関心があるなら、第６回です。

Arend の開発チームは、AI エージェントとの連携を公式に整備しました。その中身を扱います。

タロウくん：
第４回と第５回は。

専任講師：
第４回は、Haskell の data から出発します。 代数的データ型をご存じなら、そのまま読み進められます。

第５回は、本記事で最も抽象的だった箇所 ── 宇宙が２つの数で指定される話 ── を、コードで詳しく見ます。

タロウくん：
分かりました。まずは第２回を待つことにします。

専任講師：
なお、専門用語はその都度、対話篇を交えて解きほぐしていきます。 どの回から読み始めても、置いていかれることはありません。

予定の変更について

第２回以降の内容は、あくまで現時点での予定です。

筆者は Qiita で、型システムや定理証明支援系について複数の記事を公開しています。それらとの重複を避けるため、あるいは新たに公開する記事との関係を踏まえて、各回で扱う内容を変更する可能性があります。

タイトルについても、同様です。

実際に公開する際には、本稿の予定と異なる構成になることがあります。あらかじめご了承ください。

---

補足 ── Arend は、いまどれだけ使われているのか

利用者の正確な人数を示す統計は、公開されていません。

そこで、GitHub の指標を代わりに見てみます。2026年8月時点の数値です。

処理系	Star 数
Lean 4	約8,700
Agda	約2,900
Arend	753

Arend のリポジトリには、これまでに4,890件のコミットが積まれています。

IntelliJ IDEA 用のプラグインは別リポジトリになっており、そちらの Star は95です。

Lean 4 の10分の1以下、Agda の4分の1程度。 これが現在の位置です。

ただし、Star 753という数字を、公開から7年の新参者としてどう評価するかは、見方が分かれるところです。

補足 ── JetBrains は、なぜこの開発に資金を投じたのか

Arend を作ったのは、JetBrains Research です。

IntelliJ IDEA や PyCharm を作っている JetBrains の、研究部門にあたります。

同社の公式ブログに、この取り組みが説明されています。

（原文引用）

The main focus of the HoTT and Dependent Types group is to build Arend, a dependently typed language and a theorem prover based on Homotopy Type Theory. HTT is a more advanced theoretical framework than those on which systems like Agda and Coq are based. The ultimate goal is to create an online collaborative proof assistant based on a modern type theory to enable the formalization of certain branches of mathematics.

（筆者による日本語訳）

HoTT および依存型グループの主たる焦点は、Arend ── ホモトピー型理論に基づく依存型言語かつ定理証明器 ── を構築することにある。HoTT は、Agda や Coq といった体系が基づくものより進んだ理論的枠組みである。最終的な目標は、現代的な型理論に基づくオンライン共同証明支援系を作り、数学の特定の分野の形式化を可能にすることである。

出典
Scientific Research Initiatives by JetBrains, JetBrains Blog, 2020年12月21日
https://blog.jetbrains.com/blog/2020/12/21/scientific-research-initiatives-by-jetbrains/

「オンライン共同証明支援系」という目標が掲げられています。

複数の研究者が同時に１つの形式化に取り組める環境。それが、この開発の先に見据えられているものです。

そして、開発者自身の言葉もあります。

2020年4月、Andrej Bauer が主催する連続講演で、Valery Isaev はこう述べています。

（原文引用）

The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics.

（筆者による日本語訳）

Arend の目的は、ホモトピー型理論における結果と、通常の数学における結果の双方を形式化するための、強力な体系を提供することである。

出典
Every proof assistant: Arend, Mathematics and Computation, 2020年4月28日
https://math.andrej.com/2020/04/28/every-theorem-prover/

「ホモトピー型理論と、通常の数学の双方」と述べられています。

HoTT に特化した処理系ではなく、一般の数学の形式化にも使えるものを目指した ということです。

実際、標準ライブラリ arend-lib の主要部分は、HoTT ではなく構成的数学が占めています。

訳語について

本記事の訳語は、上村太一氏による日本語版の教科書『ホモトピー型理論』に従いました。

一価性公理、高次帰納的型、構造同一原理、同一視型。いずれも、同書の用語です。

出典
上村太一『ホモトピー型理論』2023年
（著者はホモトピー型理論の意味論を専門とする研究者。アムステルダム大学で博士号を取得）
https://uemurax.github.io/hott-ja/

著者の経歴を、参考までに記しておきます。

項目	内容
学位	アムステルダム大学 博士号（2021年、Abstract and Concrete Type Theories）
所属歴	京都大学数理解析研究所、アムステルダム大学 ILLC
受賞	HoTT 2019 Best Student Paper Award／FSCD 2023 Best Paper Award by Junior Researchers

主要な論文

• A General Framework for the Semantics of Type Theory, Mathematical Structures in Computer Science, 2023, doi:10.1017/S0960129523000208
• Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses, FSCD 2023, doi:10.4230/LIPIcs.FSCD.2023.5
• On Church's Thesis in Cubical Assemblies（Andrew Swan と共著）, Mathematical Structures in Computer Science, 2022, doi:10.1017/S0960129522000068

なお、同書は査読を経た出版物ではありません。

著者本人が公開している教科書です。日本語で書かれた体系的な HoTT の教科書としては、筆者が調べた範囲でほぼ唯一のものでした。

そして、訳語が学界で統一されているわけでもありません。

英語文献で higher inductive type と書かれるものを「高次帰納型」と訳す例も見られますが、本記事は同書に合わせて「高次帰納的型」を採ります。

---

関連記事

本記事の背景となる、筆者の過去の記事です。

ホモトピー型理論について

• ホモトピー型理論とは何か（連載 第１回）
• ホモトピー型理論とは何か（連載 第２回）
• Cubical Agda とは何か ── 複数の「等しさ」を証明できる言語は、なぜビジネス事例がほぼ無いのに注目されるのか

型システムと代数構造について

• Haskellのbaseには群も環も体もない ── 代数構造を型クラスでどこまで表現できるか
• 「等しさ」はどのレベルまで型として宣言し、型検査できるか？ ── Pythonから関数型言語・定理証明言語へ

定理証明支援系について

• Lean 4 とは何か ── AI が数学オリンピックに挑み、フェルマーの最終定理がコードに書き写される時代の主役言語
• コードなのに、そのまま数学の証明文として読める（タクティクスタイル編）
• コードなのに、そのまま数学の証明文として読める（宣言的スタイル編）

AI と定理証明について

• AIが数学の証明を書けるようになった6年間 ── Neural Theorem Proving の全体像

---

出典一覧

Arend

• Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
  https://arend-lang.github.io/assets/lang-paper.pdf
• New theorem prover Arend is released, Homotopy Type Theory mailing list, 2019年8月6日
  https://groups.google.com/g/homotopytypetheory/c/rf6YJB5Omj0
• Arend features, Arend Documentation
  https://arend-lang.github.io/documentation/getting-started/arend-features
• Every proof assistant: Arend, Mathematics and Computation, 2020年4月28日
  https://math.andrej.com/2020/04/28/every-theorem-prover/
• Scientific Research Initiatives by JetBrains, JetBrains Blog, 2020年12月21日
  https://blog.jetbrains.com/blog/2020/12/21/scientific-research-initiatives-by-jetbrains/
• JetBrains/Arend, GitHub
  https://github.com/JetBrains/Arend

一価的基礎づけ（UF）

• Vladimir Voevodsky, "An experimental library of formalized Mathematics based on the univalent foundations", Mathematical Structures in Computer Science, vol. 25, no. 5, 2015, pp. 1278–1294, doi:10.1017/S0960129514000577
  https://arxiv.org/abs/1401.0053
• Andrei Rodin, "Axiomatic Method and Category Theory", arXiv:1210.1478
  https://arxiv.org/abs/1210.1478
• Andrei Rodin, "Vladimir Voevodsky on the concept of mathematical structure in his letter exchange with Andrei Rodin", arXiv:2409.02935, 2024年
  https://arxiv.org/abs/2409.02935
• Special Year on Univalent Foundations of Mathematics, Institute for Advanced Study, 2012–2013
  https://www.ias.edu/math/sp/univalent
• UniMath — a computer-checked library of univalent mathematics
  https://github.com/UniMath/UniMath

ホモトピー型理論（HoTT）

• The Univalent Foundations Program, "Homotopy Type Theory: Univalent Foundations of Mathematics", Institute for Advanced Study, 2013
  https://homotopytypetheory.org/book/
• Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, Peter LeFanu Lumsdaine, "A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory", LICS 2016
  https://arxiv.org/abs/1605.03227
• 上村太一『ホモトピー型理論』2023年（著者はホモトピー型理論の意味論を専門とする研究者。アムステルダム大学で博士号を取得。本記事の訳語は、これに従いました）
  https://uemurax.github.io/hott-ja/
• 上村太一「Homotopy Type Theory 入門」2017年
  https://uemurax.github.io/pdfs/hott-intro-ja.pdf

型システム一般

• サブタイピング（計算機科学）, Wikipedia 日本語版
  https://ja.wikipedia.org/wiki/サブタイピング_(計算機科学)