Executive Summary
本記事の主題
LLMを搭載したAI Agentに、数学定理の証明の正しさを検証するための特定の定理証明支援系（Lean 4, Isabelle, Rocq, Arendなど）の検証用コードを自動生成させて、定理証明支援系が、AI Agentから受け取った検証用コードが型検証器を通るかどうかをチェックするプロジェクトが、複数、走っており、一般向けの報道ニュースでも取り上げた記事を目にする機会が増えてきました。
こうしたプロジェクトでは、学習データ・ライブラリ・検証環境として Lean を採用する事例が目立っています。
ところで、このようなプロジェクトでArendが採用される事例は、見つけるのが難しいです。
本稿のテーマは、「Arend の開発者が行ってきた言語設計の判断の数々を学ぶことは、定理証明に関心をもつプログラマにとって、それでも意味を持つか」ということです。
さて。本連載シリーズの前回（第６回目）の記事の末尾では、次の問いを残しました。
では、その道具は、実際にどう使われるのでしょうか。
そして、本連載シリーズでは、第１回目から第６回目までの記事で、Arend の設計判断を見てきました。
区間を型の中に置いたこと。
階層を土台で支えたこと。
宇宙に２つ目の軸を足したこと。
どの言語設計判断も、「形式化の実践」という判断基準に従って、下されてきた様子を解説してきました。
では、その「形式化の実践」は、いまどこで行われているのでしょうか。
現在、特に注目を集め、急速に成果が公表されている場のひとつが、冒頭で言及したAI による数学定理証明の試みです。
2024年、DeepMind の AlphaProof が国際数学オリンピックの問題を解きました。2025年、Harmonic の Aristotle が金メダル級の成績を、証明つきで達成しました。
いずれも、AI が特定の定理証明言語による証明コードを生成し、定理証明支援系がそのコードを検証する、という構図です。
そして、近年の主要な事例では、その特定の定理証明言語として、Lean 4が採用される事例が圧倒的に目立っています。
筆者が確認した、近年公表された主要な AI 定理証明の事例では、Arend の採用例を見つけることはできませんでした。
６回かけて、その設計判断を読んできたArendが、少なくとも筆者が確認できた主要なAIによる数学定理証明のプロジェクトに関する公開情報を見る限り、前面に現れていない。
この事実を、本記事の出発点に置きます。
そのうえで、３つの問いに答えます。
| # | 問い |
|---|---|
| ① | なぜ AI は Lean を選んだのか |
| ② | Arend の設計判断は、AI の観点からどう見えるか |
| ③ | Arend を使わない読者は、この連載から何を持ち帰るのか |
③が、本連載全体の総括になります。
なお、AI による数学定理の自動証明については、本連載とは別の連載で扱いました。本記事では、その内容を必要な範囲で要約します。
対話篇 ── なぜ最終回で AI の話が出てくるのか
タロウくん：
先生、最終回で、いきなり AI の話が出てきましたね。
専任講師：
唐突に思われたかもしれません。しかし、つながっています。
タロウくん：
・・・どうつながるのですか。
専任講師：
第６回目の記事の末尾で、「その道具は、実際にどう使われるのか」と問いました。
タロウくん：
はい。
専任講師：
「使われる」とは、数学の形式化が実際に行われる、ということです。
そして、いま数学の形式化で特に注目を集め、急速に成果が公表されているのが、AI による定理証明の現場です。
タロウくん：
・・・だから、AI の話になる。
専任講師：
Arend が使われているかどうかを確かめるには、その現場を見るのが最も確実です。
タロウくん：
・・・そして、使われていなかった。
専任講師：
そうです。調べた主要な事例は、どれも Lean でした。
タロウくん：
・・・では、Arend と Lean の比較になるのですね。
専任講師：
そのとおりです。
本連載シリーズを通じて、Arend と Lean を何度も比べてきました。第４回目、第５回目、第６回目の記事です。
本記事は、その比較を「AI が選んだ」という事実の側から、もう一度見直します。
タロウくん：
・・・６回分の比較を、実務の側から読み直す。
専任講師：
本記事は、その構図で進みます。
本記事で扱う Arend のリリースバージョンについて
本記事を読む前に、先に３点、述べておきます。
第１に、Arend バージョン 1.12.0 で、宇宙の仕様が変わりました。
第６回目の記事で扱った宇宙の設計は、Arend 1.10 で検証したものです。
2026年8月4日に告知された 1.12.0 では、宇宙／レベル系が刷新されました。詳細は、第６回補足記事をご覧ください。
出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
第２に、1.12.0 の実機検証は、本記事では行っていません。
ブログは 1.12.0 を告知していますが、GitHub の master と最新リリースは 1.10 のままです。そのため、2026年9月時点で実施可能な範囲内でコード検証を行いました。本記事に掲載したコードは、すべて Arend 1.10 で検証したものです。
第３に、本記事で AI による数学定理証明と Arend の親和性を論じるときは、２つのリリースバージョンを分けて論じます。
| リリースバージョン | 何を指すか | どの記事で扱ったか |
|---|---|---|
| 1.12.0 より前の Arend | 本連載で実機検証に使った 1.10 | 第１回目〜第６回目の記事 |
| 1.12.0 の Arend | 宇宙系を刷新し、CLI に JSON 出力と証明探索を加えたリリースバージョン | 第６回補足記事 |
出典：Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
本文で「Arend では〜」と述べるとき、どちらのリリースバージョンを指しているかを、そのつど明示します。
本記事を読むと、何が分かるのか
本記事は、本連載シリーズの最終回です。
第１回目から第６回目までの記事で、Arend という定理証明支援系の設計判断を見てきました。
本記事では、その設計判断が実務でどう評価されているかを、AI による定理証明という最前線の事実から確かめます。
そして、Arend を使わない読者が、本連載から何を持ち帰るのかを、最後に述べます。
本記事の結論
- 近年の主要な AI による数学証明の事例では、Lean が圧倒的に目立っています。
- Lean が有利になった要因として、３つが考えられます。Mathlib という形式化資産の量、古典数学という対象、そして UIP により証明を持ち回らずに済むこと。
- Arend の設計判断は、AI の観点からも意味を持ちうる場面があります。HoTT を扱いながら証明を持ち回らずに済ませたい場面です。ただし、その場面が現実になるかどうかは分かりません。
- 実際に AI と Arend を組ませることができます。本記事で実機で試します。Arend の開発者自身が、公式論文で Claude Code との連携を論じており、
arend-skillsというスキル集も公開されています。
- Arend の管理元である JetBrains は、Arend を研究プロジェクトとして維持しており、2025年12月と2026年8月にリリースの告知がありました。ただし、一般の開発者に向けた製品としての普及活動は、筆者が調べた範囲では確認できませんでした。
- それでも本連載を読んだ価値はあります。設計判断を読む目は、道具を選ぶ目になるからです。
本稿の論旨展開
青い枠が、出発点です。
近年の主要な AI による定理証明の事例は、Lean を使っています。
その事実と、その背景から始めます。
赤い枠が、問いです。
６回かけて読んできた Arend の設計判断は、AI の観点からどう見えるのか。
使われていない道具の設計に、意味はあるのか。
金色の枠が、本記事の中心です。
実際に AI と Arend を組ませ、Arend の証明スタイルを確かめ、Arend の管理元の現状を整理します。
緑の枠が、到達点です。
本連載を通じて読者に持ち帰ってほしいことを、最後に述べます。
設計判断を読む目は、道具を選ぶ目になる、ということです。
対話篇 ── 本記事は何を扱うのか
タロウくん：
先生、本記事は最終回ですね。
専任講師：
そうです。６回かけて、Arend の設計判断を見てきました。
タロウくん：
・・・その Arend は、実際に使われているのですか。
専任講師：
隠さずに述べます。少なくとも筆者が確認できた主要な公表事例では、Arend は前面に現れていません。
タロウくん：
・・・え。
専任講師：
AlphaProof、Aristotle、DeepSeek-Prover。この３つは、どれも Lean を使っています。
タロウくん：
・・・では、６回かけて読んだ意味は、なかったのですか。
専任講師：
その問いに、本記事全体で答えます。
なぜ AI は Lean を選んだのか。Arend の設計判断は、AI の観点からどう見えるのか。
そして、Arend を使わない読者が、この連載から何を持ち帰るのか。
タロウくん：
・・・使わない道具から、持ち帰るもの。
専任講師：
設計判断を読む目です。
それは、Lean を使うときにも効きます。
本記事の読み方
| 関心 | どこから読むか |
|---|---|
| AI による定理証明の現状を知りたい | 第１部 |
| なぜ AI が Lean を選んだのかを知りたい | 第２部 |
| Arend の設計が AI にどう見えるかを知りたい | 第３部 |
| AI と Arend を実際に組ませた結果を見たい | 第４部 |
| Arend にタクティクがあるかを知りたい | 第５部 |
| Arend の管理元と現状を知りたい | 第６部 |
| 連載全体の総括を読みたい | 第７部 |
| Arend 1.12.0 で何が変わったのかを知りたい | 第６回補足記事（本記事では扱わない） |
| 1.12.0 の CLI が AI 連携にどう効くかを知りたい | 第４部（告知の範囲で述べる） |
出典（1.12.0 の告知）：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
本記事における情報の区分
-
公式情報：公式サイト、公式論文、公式リポジトリ、公式リリースノートによる記述です。
-
実機検証：筆者が指定のリリースバージョンで型検査・実行して確認した結果です。
-
筆者実測：リポジトリのファイル数・行数・検索件数などを、筆者が集計した値です。
- 筆者の見解：実測や公開情報を踏まえた解釈です。実証済みの一般法則ではありません。
記号と用語の再掲
過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。
過去記事を読んでいない読者や、読んだが内容を忘れた読者のほうが多いと考えるためです。
| 語 | 初出 | 意味 |
|---|---|---|
| UIP | 第６回目の記事 | どの型のどの２つの要素についても、等しいことの証明は高々１つしかない、という原理 |
| 証明無関係 | 第５回目・第６回目の記事 | 同じ主張についての証明は、すべて等しいとみなす規則 |
| 宇宙 | 第４回目・第６回目の記事 | 型を分類するための型 |
| ホモトピーレベル | 第４回目・第６回目の記事 | 型の等しさの構造が、どこまで複雑になりうるかを表す数 |
isSet |
第６回目の記事 | 「この型は集合である」という性質を、型として書いたもの |
| 高次帰納型 | 第５回目の記事 | 値どうしの等しさを与える構成子を持てるデータ型 |
| 一価性 | 第１回目〜第３回目の記事 | 同値な型は等しいとする原理 |
| 形式化の実践 | 第２回目・第４回目・第６回目の記事 | Arend 公式論文が設計判断の基準とした言葉 |
本記事で初めて登場する用語は、初出の箇所で、そのつど説明します。
第１部 ── 近年の主要な AI 数学証明の事例は、Lean を使っている
専任講師：
冒頭で述べたとおり、AI による定理証明の現場を見ます。
別の連載で扱った内容の要約になりますが、本記事に必要な範囲で要約して示します。
何が起きているのか ── 事実の一覧
2024年から2026年にかけて、AI による数学定理の自動証明が急速に進みました。
| 年 | 出来事 | 使われた定理証明支援系 |
|---|---|---|
| 2024年7月 | DeepMind の AlphaProof が、国際数学オリンピック（IMO）の６問中４問を解き、銀メダル相当の成績 | Lean |
| 2025年 | Harmonic の Aristotle が、IMO で金メダル級の成績を、証明つきで達成 | Lean |
| 2026年5月 | AlphaProof Nexus が、未解決だったエルデシュの問題353問中９問を解決 | Lean |
| 2026年8月1日 | OpenAI の Astra が、数学と理論計算機科学の10件の成果を公開 | Lean |
| 2026年8月10日 | Anthropic の Claude が、リーマン予想に関連する下界を41.6%から67.2%へ更新 | Lean |
| 2026年9月4日 | Anthropic が、Fermat の最終定理の計算機検証済みの完全な証明を公開 | Lean |
ここに挙げた事実のうち、2026年7月までの分の詳細は、別の連載の記事に記載しました。DeepSeek の DeepSeek-Prover も、Mistral の Leanstral も、Lean を対象としています。2026年8月以降の３件（Astra、リーマンゼータ、Fermat の最終定理）は、各社の公式発表を筆者が確認しました（2026年9月6日）。
出典：
- Ten advances in mathematics and theoretical computer science, OpenAI, 2026年8月
- Learning more about Claude's mathematical capabilities, Anthropic, 2026年8月10日
- Formalizing Fermat's Last Theorem, Anthropic, 2026年9月4日
これは、AI 定理証明に用いられる定理証明支援系が Lean だけだ、という意味ではありません。
Isabelle、Rocq／Coq、HOL 系などを対象にした研究もあります。
近年大きく報じられた数学証明の事例を中心に見ているため、Lean が際立って見えます。
その一方で、本記事で取り上げた主要な事例の中に、Arend を使うものは見当たりませんでした。
ここで、上の表に登場した固有名詞について、あらかじめ補足説明をさせていただきます。
AlphaProof は、DeepMind が開発した、Lean で証明を生成する強化学習エージェントです。2024年に国際数学オリンピックの問題を解きました。
Aristotle は、Harmonic が開発した AI です。2025年に国際数学オリンピックで金メダル級の成績を、Lean の証明つきで達成しました。
DeepSeek-Prover は、DeepSeek が開発した、Lean の証明を生成する言語モデルです。
Leanstral は、Mistral が開発した、Lean 向けの言語モデルです。
強化学習とは、AI が試行と評価を繰り返して学習する方法です。定理証明では、証明が検証器を通ることを評価の基準にします。
訓練データとは、AI が学習に使うデータです。定理証明では、既存の形式化された証明の量が効きます。
検証器（チェッカー）とは、証明が正しいかどうかを機械的に判定する、定理証明支援系の中核部分です。それ自体が小さく、厳密に作られたプログラムで、誤った証明を通しません。
AI と定理証明支援系の役割分担
タロウくん：
先生、AlphaProof は、Lean の競合なのですか。
専任講師：
違います。役割が別です。
別の連載の記事で、次のように述べました。
**AlphaProof** は、**Lean のコードを書くAI** です。
**定理証明支援系そのものではありません。**
Lean や Isabelle のような処理系とは、役割が違います。
出典：
【全４回連載（第１回）】AIが数学の証明を書けるようになった6年間, Qiita, 2026年8月12日（第６部）
タロウくん：
・・・AI が証明を生成し、Lean が検査する。
専任講師：
そのとおりです。
| 段階 | 担当 |
|---|---|
| 証明を生成する | AI（AlphaProof、Aristotle など） |
| 生成された証明を検査する | 定理証明支援系（Lean） |
AI は、事実でないことを、さも事実であるかのように出力することがあります。幻覚（ハルシネーション）と呼ばれる現象です。
証明においては、検証器がその出力を弾きます。
AI が速く賢くなるほど、「機械的に検査できる」という定理証明支援系の性質が、価値を増します。
タロウくん：
・・・だとすると、Arend も検証器を備えた定理証明支援系です。なぜ、Arend は使われないのでしょうか。
専任講師：
その問いが、第２部の主題です。
Lean には公式のスキル集がある
もうひとつ、事実を挙げます。
Lean の開発元は、AI コーディングエージェント向けのスキル集を公式に公開しています。
| 項目 | 内容 |
|---|---|
| リポジトリ | leanprover/skills |
| 内容 | AI coding agents が Lean 4 で作業するためのスキル。証明の記述、ツールチェーンの設定、リグレッションのデバッグ |
| 対応 | Claude Code、Codex、Gemini CLI |
Lean は、AI に使われることを前提とした整備を、公式に進めています。
では、Arend の側には何があるのでしょうか。第４部で見ます。そこには、意外な発見がありました。
第２部 ── AI による定理証明で Lean が有利になった３つの要因
タロウくん：
先生、なぜ AI は Lean を選んだのですか。
専任講師：
３つの観点から説明します。どれも、本連載で既に見てきたことの帰結です。
第１の観点は、形式化資産の量です。
観点① ── 形式化資産の量
タロウくん：
・・・形式化資産。
専任講師：
AI は、既存のコードから学びます。Mathlib には、28万を超える定理が形式化されています（2026年9月6日の時点で 287,051 定理・136,422 定義。公式統計ページの筆者実測）。AI が Lean の証明を生成する際に利用できる、巨大な形式化資産です。
ただし、Mathlib の定理数＝AI の訓練データの量、ではありません。そのコードが実際にモデルの学習データに入っているか、どのバージョンが入っているか、証明コードのどの部分が学習に効くかは、別の問題です。
段階を分けると、次のようになります。
| 段階 | 何が起きるか | Mathlib の量が効く理由 |
|---|---|---|
| 学習前 | モデルが公開済みコードを学ぶ場合がある | 例が多いほど構文・定石を学びやすい可能性がある |
| 証明生成中 | 既存補題を検索・呼び出す | 使える補題が多いほどゼロから証明しなくてよい |
| 検証 | Lean が型検査する | ライブラリの定理を正しく使えているか確認できる |
📌 厳密性を担保した説明をすると ── ライブラリの規模は、AI の性能を直接決める数値ではない
ライブラリの定理数は、利用可能な補題・学習可能なコード例・検索対象の広さの、ひとつの目安にすぎません。AI の性能には、データの質、形式化のスタイル、検索機構、モデル、学習方法、問題の分布なども影響します。したがって本記事では、「Mathlib が大きいことは Lean を有利にしうる重要な条件」と述べますが、「定理数だけで性能差が決まる」とは主張しません。
タロウくん：
・・・Arend は。
専任講師：
arend-lib 1.10 は、233 モジュール、41,316 行です。規模が違います。
1.12.0（告知）では代数幾何と解析が加わりましたが、規模は未確認です。いずれにせよ、Mathlib の28万定理との差は大きいままです。
出典：
- Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
- Mathlib statistics, Lean Community（2026年9月6日に筆者取得）
別の連載で、次のように述べました。
**AIの能力ではなく、ライブラリに何が揃っているかが、扱えることを決めているのです。**
出典：
【全４回連載（第１回）】AIが数学の証明を書けるようになった6年間, Qiita, 2026年8月12日（第６部）
タロウくん：
・・・AI が賢いかどうかではなく、学ぶ材料があるかどうか。
専任講師：
そのとおりです。そして、本連載シリーズの第４回目の記事で、Mathlib という蓄積を Arend が持たないことを述べました。
その差が、AI の時代にはさらに効きます。
arend-lib には、何が入っているのか
タロウくん：
先生、arend-lib の中身を、具体的に教えてください。
専任講師：
公式論文が、次のように述べています。
（原文引用）
The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.
（筆者による日本語訳）
Arend の主要ライブラリ arend-lib は、構成的代数、位相、合成ホモトピー論の形式化を含む。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
Arend 1.10 の arend-lib を、筆者が実測しました。
| 分野 | arend-lib 1.10（実測） | arend-lib 1.12.0（告知） | Mathlib |
|---|---|---|---|
| 構成的代数 | Algebra 73ファイル | Noether 環、Hilbert の基底定理、テンソル積を追加 | あり |
| 位相 | Topology 34ファイル | ロケールとサイトを再構成 | あり |
| 合成ホモトピー論 | Homotopy 24ファイル（円周、トーラス、Hopf、Blakers–Massey） | 変更の告知なし | なし（UIP のため） |
| 代数幾何 | AG ディレクトリあり | scheme、Spec、Proj を追加 | あり |
| 解析 | Analysis 5ファイル | sin、cos、cos π = -1、Banach 代数を追加 | 充実 |
| 数論 | Arith 11ファイル | 変更の告知なし | 充実 |
1.10 の数値は筆者が実測したものです。1.12.0 の内容は告知から読み取ったもので、実機では未確認です。
出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
タロウくん：
・・・「合成ホモトピー論」の行だけ、Mathlib が「なし」になっています。
専任講師：
注目してほしい行です。
Homotopy ディレクトリの24ファイルには、円周、トーラス、球面、Hopf ファイブレーション、懸垂、プッシュアウト、切断、そして Blakers–Massey 定理の形式化が入っています。
出典：
筆者による実測（2026年9月5日。手順は本稿 Appendix A-9）
本連載シリーズの第５回目・第６回目の記事で実機で示したとおり、Lean 4 の標準的な論理・言語機構では、HoTT で用いる高次帰納型を、そのまま原始的な構文として定義することはできません。そのため、Arend の Homotopy ディレクトリにあるような、HoTT と高次帰納型を基礎にした合成ホモトピー論の形式化は、Mathlib にはありません。
📌 厳密性を担保した説明をすると ── Mathlib にもホモトピー論はある
「Mathlib にはホモトピー論がない」という意味ではありません。Mathlib には、基本群、基本亜群、ホモトピー群など、通常のトポロジー・代数的トポロジーの形式化が存在します。位相空間の上でパスやホモトピーを定義し、古典的な手法で扱う形式化です。
本文で問題にしているのは、その古典的なホモトピー論との違いです。Arend の Homotopy ディレクトリにあるのは、円周やトーラスを高次帰納型として直接定義し、パスの構造を型理論の内部で扱う形式化です。この方法は synthetic homotopy theory（合成ホモトピー論）と呼ばれ、HoTT と高次帰納型を土台にします。Lean 4 は UIP を採用しているため、この土台の側が成立しません。
まとめると、「Mathlib にホモトピー論がない」のではなく、「HoTT と高次帰納型を基礎にした合成ホモトピー論の形式化が Mathlib にない」が正確な言い方です。
出典：
Mathematics in mathlib（Topology の節に fundamental group、homotopy 等の項目）, Lean Community
タロウくん：
・・・Arend でしかできない形式化が、確かにある。
専任講師：
あります。しかし、AI が解いている問題には、それが含まれていません。第２の観点に進みます。
観点② ── 対象が古典数学
専任講師：
第２の観点は、対象が古典数学であることです。
タロウくん：
・・・古典数学。
専任講師：
IMO の問題は、整数、代数、幾何、組合せです。すべて古典数学です。
IMO のような古典数学の問題を形式化する際には、HoTT 固有の機能が必須になるとは限りません。
📌 厳密性を担保した説明をすると ── HoTT は古典数学に使えないのか
「使えない」のではありません。HoTT の上でも、整数や代数のような通常の数学は形式化できます。集合にあたる階層（h-level が 0 の型、本連載の言い方では \Set）の内部で作業すれば、古典的な数学はそのまま展開できます。arend-lib に Algebra や Arith のディレクトリがあることが、その実例です。
本文で述べているのは、可否ではなく必要性です。IMO の整数・代数・幾何・組合せのような問題では、高次のパス構造が証明の対象になりません。HoTT 固有の機能（高次帰納型、単価性）の出番が少ないので、UIP を認める Lean 4 で困る場面がない、というのが正確な整理です。
タロウくん：
・・・第５回目の記事で、Lean 4 は円周を扱えないと見ました。
専任講師：
しかし、IMO に円周の基本群は出ません。
ここで注意をひとつ添えます。ここでいう「円周」とは、オリンピック幾何で描く平面図形としての円ではなく、ホモトピー型理論で「点と、その点から自分自身への非自明な道」を持つ対象として扱う円周です。両者は同じ語を使いますが、本記事で問題にしている構造は別のものです。
Lean 4 が HoTT を扱えないことは、AI による定理証明では制約になりません。
タロウくん：
・・・第６回目の記事で、「古典数学を形式化するなら、UIP を認めて困ることはない」と伺いました。
専任講師：
そのとおりです。AI が解いている問題は、まさにその範囲です。
観点③ ── UIP が効く
専任講師：
第３の観点は、UIP が効くことです。
タロウくん：
・・・第６回目の記事の主題ですね。
専任講師：
「証明を持ち回るか、型に語らせるか」。それを、AI の側から見直します。
AI が証明を生成するとき、生成すべきトークンが少ないほど、失敗の余地が減ります。
トークンとは、AI が生成する文字列の単位です。生成量の目安になります。
タロウくん：
・・・持ち回る証明が多いほど、生成量が増える。
専任講師：
Lean 4 では、等式の証明は Prop 側で証明無関係として扱われます。その結果、通常の Lean の型では、「等式証明どうしの違い」を持ち回って扱う必要がありません。
📌 厳密性を担保した説明をすると ── 「Lean は UIP を採用している」とはどういう意味か
本記事では、比較のために「Lean 4 は UIP を採用している」という言い方を使っていますが、厳密には、Lean 4 が UIP という公理をそのまま置いているのではありません。
Lean 4 の Prop には proof irrelevance（証明の無関心性）があります。同じ命題の証明は、どの２つも定義上等しい、という性質です。そして Lean 4 の等式型 Eq は Prop に属します。この２つを合わせると、「a = b の証明はどの２つも等しい」が従います。これが、型理論で UIP（Uniqueness of Identity Proofs）と呼ばれる性質です。
つまり、isSet（本文の言い方では「p q : x = y ならば p = q」）が、Lean 4 ではすべての型について最初から成立しています。だから証明を持ち回る必要がありません。
HoTT では事情が逆になります。等式型（identity type）の証明が２つ以上あって互いに等しくない、という状況（円周の loop と自明なパス）こそが、ホモトピーの情報を運びます。UIP を認めると、この情報が消えます。第５回目・第６回目の記事で実機で見たのは、この違いです。
実際に測ってみました。第３部でお見せします。
タロウくん：
・・・Arend も持ち回らないのでは。
専任講師：
そうです。しかし、理由が違います。第６回目の記事で見たとおりです。
そして、Arend が持ち回らずに済む理由（宇宙の２つ目の軸）は、HoTT を扱うためのものです。AI が古典数学を解くときには、その利点が使われません。
第２部のまとめ ── 目的が違う
専任講師：
３つの観点を並べます。
| # | 観点 | Lean 4 | Arend |
|---|---|---|---|
| ① | 形式化資産の量 | Mathlib 28万定理（287,051） | arend-lib 233 モジュール |
| ② | 対象が古典数学 | UIP で困らない | HoTT の利点が使われない |
| ③ | UIP が効く | 持ち回らない | 持ち回らないが、理由が別 |
タロウくん：
・・・どれも、Arend の設計が悪いという話ではないですね。
専任講師：
そのとおりです。
Arend の設計判断は、HoTT を扱うためのものでした。AI が求めたのは、古典数学を大量に解くことでした。
目的が違うのです。
別の連載で、Lean と Isabelle の差について述べました。
**Lean の記録が99.6%、Isabelle の記録が66.0%。** しかし差を生んでいるのは言語の優劣ではなく、**ライブラリの規模と、問題集の性質である**
出典：
【全４回連載（第１回）】AIが数学の証明を書けるようになった6年間, Qiita, 2026年8月12日（TL;DR）
タロウくん：
・・・Arend と Lean の差も、言語の優劣ではない。
専任講師：
ライブラリの規模と、対象の性質です。
なお、Arend にも、Lean と共通する限界があります。公式論文は、Arend の商型の実装について、次のように述べています。
（原文引用）
Arend's implementation of the approach (4) to the definition of a quotient type has the same disadvantages as the axiomatic approach (2) as is implemented in Lean
（筆者による日本語訳）
商型の定義への方式(4)の Arend における実装は、Lean に実装されている公理的方式(2)と同じ欠点を持つ。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第2.3.2節
開発者自身が、自分たちの設計の限界を論文に明記しています。「Arend が優れていて Lean が劣っている」という単純な話ではないことを、ここでも確認できます。
第３部 ── 「証明を持ち回るか」は、AI にとっても問題である
第６回目の記事のテーマを、AI の側から見直す
本連載シリーズの第６回目の記事で、次の対比を実機で確かめました。
| 体系 |
isSet の証明 |
|---|---|
| Lean 4 | 持ち回らない（UIP による） |
Agda --without-K
|
持ち回る |
| Arend | 持ち回らない（宇宙の軸による） |
この対比を、AI の側から見直します。
AI が証明を生成するとき、検証器が受け入れるまで何度も試行します。
持ち回る証明が多いほど、生成すべきトークンが増え、失敗の余地が増えます。
| 体系 |
isSet の証明 |
記述量の観点から見た生成負担の目安 |
|---|---|---|
| Lean 4 | 持ち回らない（UIP） | 小さい |
Agda --without-K
|
持ち回る | 大きい |
| Arend | 持ち回らない（宇宙） | 小さい |
ここで測っているのは、AI が実際に生成するトークン数ではなく、人間が記述するコードの量です。「生成負担の目安」の列は、筆者の推測です。実証した研究は、筆者が調べた範囲では見つかっていません。この点は、本部の末尾の【本記事執筆者の見解】に記します。
小実験 ── isSet を明示的に引き回す場合と、型の階層情報に載せる場合の記述量
推測のままでは終わらせません。コードの長さは、実測できます。
次の実験をしました。
| 処理系 | 内容 |
|---|---|
Agda --without-K
|
useIsSet1 から useIsSet10 まで、10個の関数を記述する。h : isSet A を毎回引数に取り、次の関数へ渡す |
| Arend 1.10 | 同じ10個の関数を記述する。A : \Set0 で済ませる |
Agda 側のコードの冒頭を示します。
＜Agda のコード（抜粋）＞
{-# OPTIONS --without-K #-}
module CARRY10 where
open import Agda.Builtin.Equality
isSet : Set → Set
isSet A = (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet1 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet1 A h x y p q = h x y p q
useIsSet2 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet2 A h x y p q = useIsSet1 A h x y p q
この調子で、useIsSet10 まで続きます。どの関数も、isSet A の証明 h を引数に取り、次の関数へ渡しています。
Arend 側の全文は、次のとおりです。
＜Arend のコード＞
\import Paths
\import Logic
\func useIsSet1 (A : \Set0) (x y : A) (p q : x = y) : p = q => prop-isProp p q
\func useIsSet2 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet1 A x y p q
\func useIsSet3 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet2 A x y p q
\func useIsSet4 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet3 A x y p q
\func useIsSet5 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet4 A x y p q
\func useIsSet6 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet5 A x y p q
\func useIsSet7 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet6 A x y p q
\func useIsSet8 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet7 A x y p q
\func useIsSet9 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet8 A x y p q
\func useIsSet10 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet9 A x y p q
コードの読み方を添えます。
Agda 側では、関数の型に isSet A → が入っています。呼び出す側は、h を毎回渡さなければなりません。
Arend 側では、引数の型を A : \Set0 と宣言しています。「A はホモトピーレベル０の型、すなわち集合である」という情報が、宇宙の軸に載っています。したがって、isSet の証明を引数に取る必要がありません。式 prop-isProp p q は、arend-lib の補題で、集合においては等しさの証明どうしが等しいことを与えます。
＜Arend の型検査結果＞
$ java -Xmx4g -jar Arend.jar -L libs -l arend-lib src/CARRY10.ard
[ ] src.CARRY10
--- Done (102ms) ---
両方とも型検査を通ります（Agda 2.6.3 と Arend 1.10 で確認）。測った結果は、次のとおりです。
Agda --without-K
|
Arend 1.10 | |
|---|---|---|
| 文字数 | 1,372 | 856 |
h の出現回数 |
20（署名10＋本体10） | 0 |
この実験は、isSet A を各関数の明示引数として受け渡す、という書き方に限定した比較です。Agda 一般の記述量や、両言語で同じ数学を形式化したときの総コストを測るものではありません。
📌 厳密性を担保した説明をすると ── この小実験が比較しているもの
この比較は、Agda と Arend の全体的な表現力・使いやすさ・証明開発コストを測るものではありません。isSet の証明を関数境界ごとに明示的に渡す設計と、\Set0 のように型の分類情報へ載せる設計とで、同じ連鎖の例において引数の記述量がどう変わるかを観察したものです。
Agda 側でも、レコード、暗黙引数、モジュール、インスタンス解決などの設計しだいで記述量は変えられます。ここでは、両者の違いを最も素朴な形で見るために、明示引数で受け渡す書き方に揃えています。
タロウくん：
・・・Arend は、Agda の 62% の文字数で同じことを記述できています。
専任講師：
数式で述べ直します。関数の個数を $n$ とすると、Agda では h の出現回数が $2n$ 本（署名に $n$、本体に $n$）に比例して増えます。Arend では $0$ のままです。
$$\text{Agda の } h \text{ の出現回数} = 2n, \qquad \text{Arend の } h \text{ の出現回数} = 0$$
関数が増えるほど、差は開きます。
タロウくん：
・・・AI が生成すべき量も、比例して増えるということですか。
専任講師：
そこは、慎重に区別します。
測ったのは、コードの長さです。AI の話ではありません。
しかし、AI が生成する量の目安にはなります。
Agda では、10個の関数で h を10回、署名も含めれば20回記述しました。Arend では、０回です。
📌 厳密性を担保した説明をすると ── コードの記述量と、AI の証明成功率は同じではない
本文の実測（Agda 1,372文字、Arend 856文字）から言えるのは、人間が記述するコードの量の差までです。AI の成功率の話に進むには、いくつもの段差があります。
- 文字数とトークン数は別です。トークンの切られ方は言語と字句に依存します。
- 生成量が減っても、探索空間が狭くなるとは限りません。短いコードほど１トークンあたりの情報密度が上がり、誤りの影響が大きくなる可能性もあります。
- AI の証明は一発で終わらず、検証器のエラーを見て書き直すループで進みます。ループの回数や、エラーメッセージの読みやすさも成功率に効きます。
- 既存ライブラリから補題を探し当てる能力も効きます。この点では、資産の大きい Lean が有利です。
本文の実験は「記述量の小さな実験」であって、AI のベンチマークではありません。「証明を持ち回らない体系のほうが AI の成功率が高い」ことを実証した研究は、筆者が調べた範囲では見つかっていません。
【本記事執筆者の見解】
「型に語らせる」設計は、人間だけでなく AI にとっても利点になりうる、と筆者は考えます。
根拠は、上の実測です。生成すべきコードが短ければ、AI が誤りを混入させる箇所も減ります。
ただし、これは筆者の解釈です。次の２点を、事実と区別して明記します。
| # | 内容 |
|---|---|
| ① | 「生成すべき量が減る」ことと、「AI が正しく生成できる」ことは、別です。コードが短くても、AI がArend の構文に不慣れであれば、誤りは出ます（第４部で実例を見ます） |
| ② | 「証明を持ち回らない体系のほうが AI の成功率が高い」ことを実証した研究は、筆者が調べた範囲では見つかっていません |
第４部 ── 実際に AI と Arend 1.10 を組ませてみる
タロウくんの質問 ── CLI 以外の利用法
タロウくん：
ArendのCLIコマンドラインインターフェイスについて書いていますが、ArendはCLI以外の利用法はあるのですか？
専任講師：
あります。３つの使い方があります。
| # | 使い方 | 内容 |
|---|---|---|
| ① | IntelliJ Arend | IntelliJ IDEA のプラグイン。公式が「full-fledged IDE」と呼ぶ。本連載では使っていない |
| ② | CLI |
java -jar Arend.jar。本連載で使ってきた |
| ③ | REPL |
java -jar Arend.jar -i。対話的に式を評価できる |
CLI とは、コマンドラインインターフェースのことです。本連載で使ってきた java -jar Arend.jar がそれにあたります。
Arend の公式サイトの記述を引用します。
（原文引用）
IntelliJ Arend is a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language.
（筆者による日本語訳）
IntelliJ Arend は、IntelliJ IDEA を Arend 言語の本格的な IDE に変えるプラグインである。
タロウくん：
・・・本連載では、なぜ CLI だけを使ったのですか。
専任講師：
３つの理由があります。
| # | 理由 |
|---|---|
| ① | 再現性。CLI なら、コードと実行コマンドをそのまま記事に載せられる。読者が同じコマンドを打てば、同じ結果が出る |
| ② | AI との連携。AI エージェントはコマンドを実行して結果を読む。IDE の画面は読めない（2026年9月時点の一般的な AI エージェントについての記述であり、将来は変わりうる） |
| ③ | 環境の軽さ。IntelliJ IDEA を導入せずに済む |
なお、筆者は IntelliJ Arend を実機で試していません。
タロウくん：
・・・IntelliJ Arend でしかできないことは、ありますか。
専任講師：
1.10 の時点では、証明探索が IDE 限定でした。
1.12.0（告知）で、証明探索が CLI の -ps オプションとして追加されました。告知文に「previously IDE-only」とあります。
出典：Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
つまり、CLI と IDE の差は、縮まっています。
タロウくん：
・・・REPL は、何に使うのですか。
専任講師：
式を評価して、結果を見るのに使います。実機で試しました。
$ java -jar Arend.jar -i
>suc (suc zero)
2
suc (suc zero) が 2 に評価されました（Arend 1.10）。
ただし、1.10 の REPL は、命令の体系に不慣れだと使いにくい面があります。1.12.0（告知）では、複数行入力やモジュールの事前読み込みが改善されたとあります。
出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
開発者自身が、Claude Code との連携を論文に記述している
AI と Arend の CLI を組ませる話は、筆者の思いつきではありません。
Arend の公式論文の第５節は、「Using Claude Code with Arend CLI」と題されています。
（原文引用）
One use case that has recently become practical is LLM-assisted formalization: coupling the type checker with an AI coding agent such as Claude Code developed by Anthropic. An agent of this kind works in an edit–check loop: it modifies source files, invokes external tools, reads their textual output and iterates. A command-line type checker with textual feedback is therefore a natural fit for such an agent, and the absence of a graphical environment is no obstacle.
（筆者による日本語訳）
最近実用的になった用途のひとつが、LLM 支援形式化である。すなわち、型検査器を、Anthropic が開発した Claude Code のような AI コーディングエージェントと組み合わせることである。この種のエージェントは、編集–検査ループで動作する。ソースファイルを修正し、外部ツールを呼び出し、そのテキスト出力を読み、繰り返す。したがって、テキストによるフィードバックを返すコマンドライン型検査器は、このようなエージェントに自然に適合し、グラフィカル環境の不在は障害にならない。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第５節
タロウくん：
・・・開発者自身が、Claude Code を名指ししています。
専任講師：
そうです。そして、CLI に検索ツールを備えた理由についても、こう述べています。
（原文引用）
For an agent these tools play the role of the IDE's navigation features: they answer the questions "does this lemma already exist?", "what is it called?" and "how is it used?" cheaply, without reading the sources of arend-lib.
（筆者による日本語訳）
エージェントにとって、これらのツールは IDE のナビゲーション機能の役割を果たす。「この補題は既にあるか」「何と呼ばれているか」「どう使われているか」という問いに、arend-lib のソースを読まずに安価に答える。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第５節
タロウくん：
・・・検索ツールというのは、何ですか。
専任講師：
1.12.0（告知）で CLI に追加されたオプション群です。
| オプション | 内容 |
|---|---|
--serialize |
型検査結果をバイナリキャッシュ（.arc）に保存 |
-ss |
記号検索 |
-ps |
証明探索。1.10 では IDE 限定だった |
-fu |
使用箇所検索 |
-ch |
クラス階層 |
-sc |
スコープ |
--json |
すべての出力を JSON 形式で |
--json 出力と -ps 証明探索は、AI エージェントが Arend を使うための基盤です。JSON 形式なら、AI が結果を機械的に読めます。
ただし、筆者はこれらを実機で試せていません。2026年9月時点で、1.12.0 の jar が GitHub から取得できないためです（第６部で述べます）。
出典：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
arend-skills ── Arend のためのスキル集は、実在した
第１部で、Lean には公式のスキル集 leanprover/skills があると述べました。
Arend の側にも、スキル集があります。
| 項目 | 内容 |
|---|---|
| リポジトリ | https://github.com/sxhya/arend-skills |
| 最終コミット | 2026年8月10日（2026年9月5日に確認） |
| 出どころ | 公式論文の第５節、脚注14 で参照されている |
出典：sxhya/arend-skills, GitHub、Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第５節
タロウくん：
先生、スキルというのは何ですか。
専任講師：
AI コーディングエージェントに与える、作業手順の文書です。
Claude Code は、~/.claude/skills/ に置かれた文書を読み、その分野の作業のしかたを学びます。
Claude Code とは、Anthropic の、コマンドラインから使う AI エージェントです。ファイルの読み書きとコマンドの実行ができます。
arend-skills をクローンして、中身を確認しました（2026年9月5日）。
| スキル | 行数 | 内容 |
|---|---|---|
arend-formalize |
265行 | 非形式的な数学の主張を、型検査の通る Arend の定義・補題に変える手順。CLI の検索ツールの使い方、arend-lib の歩き方 |
arend-prove |
642行 |
{?} を埋める手順。メタの一覧（rewrite、cases、mcases、simplify、equation、cong、ext、linarith、unfold） |
arend-quirks |
472行 | Arend の構文・意味が Coq・Agda・Lean とどう違うかの注意書き |
arend-error-type-mismatch |
108行 | 誤解を招く Type mismatch エラーの診断 |
arend-error-extraneous-input |
69行 |
extraneous input パーサエラーの診断 |
注目すべき設計があります。論文には、こうあります。
（原文引用）
Notably, the skills also instruct the agent to feed newly acquired knowledge (language quirks, meta failure modes) back into the skill files, so that the collection grows with use.
（筆者による日本語訳）
注目すべきことに、スキルはエージェントに対し、新たに獲得した知識（言語の癖、メタの失敗モード）をスキルファイルに書き戻すよう指示する。そのため、スキル集は使うほどに成長する。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第５節
タロウくん：
・・・AI が Arend を学ぶ仕組みが、スキル自体に組み込まれている。
専任講師：
そうです。
ただし、２点、注意があります。
| # | 内容 |
|---|---|
| ① | arend-skills は、1.12.0 の CLI（-ss、-ps、--serialize）を前提としています。筆者がスキルの本文を数えたところ、-ss が55回、--serialize が39回、-ps が18回、使われていました。1.10 の CLI（java -jar Arend.jar）には、これらのオプションが存在しません。したがって、1.10 の環境ではスキルの中心的な部分が動きません |
| ② | README によれば、一部のスキルは作成者のマシン上の絶対パス（arend-lib のローカルチェックアウト）を参照しており、使うときは調整が要ります |
出典：
sxhya/arend-skills, GitHub
そこで本記事の実験は、次の方針を採ります。
Arend 1.10 の CLI で、スキルなしで AI に Arend を記述させます。そして、「1.12.0 の CLI が入手できれば、arend-skills を組み合わせられる」ことを、今後の課題として述べます。
なお、leanprover/skills は Lean の開発元による公式のリポジトリであり、sxhya/arend-skills は開発者個人のリポジトリです。「公式か、個人か」という違いも、両言語の普及の差を表しています。
実験 ── AI に Arend のコードを記述させ、CLI で検証する
別の連載で見た「AI が証明を生成し、Lean が検証する」という構図を、Arend で再現します。
実験の手順は、次のとおりです。
| 手順 | 内容 |
|---|---|
| ① | AI に、Arend のコードを記述する課題を与える |
| ② | AI の出力を java -jar Arend.jar で型検査する（Arend 1.10） |
| ③ | エラーが出たら、そのエラーメッセージを AI に返す |
| ④ | AI が修正する |
| ⑤ | ②〜④を、通るまで繰り返す |
実験の条件を明記します。
| 項目 | 内容 |
|---|---|
| 処理系 | Arend 1.10（Java 21） |
| AI | Claude |
| プロンプトの指定 | 「Arend 1.10 の構文で記述すること」を指定した。1.12.0（告知）で導入された .{l} 構文（詳細は第６回補足記事）は 1.10 で弾かれるため |
| 試行回数 | 各課題２回まで記録 |
出典（.{l} 構文について）：
Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
先に、この実験の限界を述べます。
本実験に使った AI（Claude）は、本実験を行うのに先立ち、事前にArend のコードに触れさせる期間を設けました。そのため、こうした期間を経ていないClaudeとは、公平なパフォーマンス比較を行うことはできません。
課題① ── 加法の交換法則
課題：plus-comm (n m : Nat) : n Nat.+ m = m Nat.+ n を、標準ライブラリなしで証明する。
１回目の出力は、失敗しました。
＜Arend の型検査結果（１回目）＞
[ERROR] src/AI1.ard: Termination check failed
再帰の構造が、Arend の停止性検査に受け入れられませんでした。
このエラーメッセージを AI に返したところ、２回目の出力は、補題を分離した形になりました。
＜Arend のコード（２回目）＞
\func pmap {A B : \Type} (f : A -> B) {a a' : A} (p : a = a') : f a = f a' => path (\lam i => f (p @ i))
\func \infixr 9 *> {A : \Type} {a a' a'' : A} (p : a = a') (q : a' = a'') : a = a'' \elim q | idp => p
\func plus-zero (n : Nat) : n Nat.+ 0 = n => idp
\func zero-plus (n : Nat) : 0 Nat.+ n = n \elim n
| 0 => idp
| suc n => pmap suc (zero-plus n)
\func plus-suc (n m : Nat) : n Nat.+ suc m = suc (n Nat.+ m) => idp
\func suc-plus (n m : Nat) : suc n Nat.+ m = suc (n Nat.+ m) \elim m
| 0 => idp
| suc m => pmap suc (suc-plus n m)
\func plus-comm (n m : Nat) : n Nat.+ m = m Nat.+ n \elim m
| 0 => inv (zero-plus n)
| suc m => pmap suc (plus-comm n m) *> inv (suc-plus m n)
\where \func inv {A : \Type} {a a' : A} (p : a = a') : a' = a \elim p | idp => idp
＜Arend の型検査結果（２回目）＞
$ java -jar Arend.jar src/AI1.ard
[ ] src.AI1
--- Done (254ms) ---
コードの読み方を添えます。pmap は「等しさに関数を適用する」補題、*> は等しさの連結、zero-plus と suc-plus は交換法則の証明に必要な２本の補助補題です。本体の plus-comm は、m についての帰納法で、補助補題を組み合わせています。
同じ課題を Lean 4（4.33.1）でも試しました。１回目で通りましたが、simp の警告が出ました。２回目は Mathlib 相当の Nat.add_comm を直接使う１行になりました。
theorem plus_comm (n m : Nat) : n + m = m + n := Nat.add_comm n m
タロウくん：
・・・Lean では、ライブラリの補題を知っていれば１行です。
専任講師：
条件を揃えて整理すると、次のようになります。
| 比較 | Arend | Lean |
|---|---|---|
| ライブラリ補題なし | 補題を自作して交換法則を示す | 帰納法・補助補題を用いる証明になる |
| 既存ライブラリを使う | 該当補題があれば呼び出せる |
Nat.add_comm を１行で呼び出せる |
ここでの「１行」という差は、Lean の言語構文そのものの差というより、既に Nat.add_comm が利用可能なライブラリ資産として存在することの差です。
第２部の観点①が、ここに現れています。ライブラリに何が揃っているかが、AI の作業量を決めています。
課題② ── 円周と loop
課題：円周 S1 を高次帰納型として定義し、loop を使う簡単な証明を記述する。
この課題は、Lean 4 では試みることすらできません。Lean 4 には高次帰納型を定義する手段がないためです（第５回目の記事で実機で確認しました）。
１回目の出力は、失敗しました。
＜Arend の型検査結果（１回目）＞
[ERROR] src/AI4.ard: Cannot resolve reference 'inv' in Path
標準ライブラリなしの環境では、道の逆 inv が定義されていません。AI は arend-lib の補題を前提にしていました。
エラーメッセージを返したところ、２回目は inv を自前で定義した形になりました。
＜Arend のコード（２回目）＞
\data S1 | base | loop : base = base
\func inv {A : \Type} {a a' : A} (p : a = a') : a' = a \elim p | idp => idp
\func loop-inv : base = base => inv loop
\func loop-twice : base = base => path (\lam i => loop @ i) *> loop
\where \func \infixr 9 *> {A : \Type} {a a' a'' : A} (p : a = a') (q : a' = a'') : a = a'' \elim q | idp => p
＜Arend の型検査結果（２回目）＞
$ java -jar Arend.jar src/AI4.ard
[ ] src.AI4
--- Done (171ms) ---
\data S1 | base | loop : base = base の２行目に注目してください。値の構成子 base と並べて、等しさの構成子 loop : base = base を記述しています。第５回目の記事で見た、Arend の高次帰納型の定義そのものです。
実験の観察
| # | 観察 |
|---|---|
| ① | Arend の１回目の失敗は、２件とも「Arend 固有の事情」によるものでした。停止性検査の厳しさと、標準ライブラリなしでの関数の不足です。論理の誤りではありません |
| ② | エラーメッセージを返すと、AI は２回目で修正できました。「編集–検査ループ」が、Arend の CLI でも成立します |
| ③ | Lean 4 では、このセッションでは１回目の出力が型検査を通りました。ただし、この差を訓練データの量、言語設計、既知補題の存在、プロンプトとの相性などのどれに帰すべきかは、この小規模な記録だけでは判断できません |
| ④ | 高次帰納型の課題は、Arend でしか出題できませんでした |
「AI は Arend を記述できない」とも、「問題なく記述できる」とも、この実験からは断定できません。試行回数と条件を明記したうえで、記録として残します。
第５部 ── Arend の証明スタイル ── タクティクはあるのか
本連載シリーズより前に、筆者は証明の記法についての記事を２本公開しています。
-
コードなのに、そのまま数学の証明文として読める（タクティクスタイル編）
- コードなのに、そのまま数学の証明文として読める ── AIが証明を書く時代に注目すべきMizar・Isabelle・Lean 4 の宣言的スタイルの記法
タクティクスタイルとは、証明の手順を命令として記述する方式です。Coq や Lean の intros、apply などがそれにあたります。
Isar とは、Isabelle の構造化証明言語です。proof ... have ... show ... qed のように、証明の構造を自然言語に近い形で記述します。
この２本を読まれた方は、次の疑問を抱くはずです。
タロウくんの問い
タロウくん：
先生、ひとつ質問してもいいですか。
ここまでの記事を見ると、Arend は Isar 記法だけで、タクティクは無いように思います。それで合っていますか。
専任講師の返答
専任講師：
半分合っていて、半分違います。
合っている点 ── Coq や Lean のような「タクティク言語」はありません
Arend には、Proof. ... Qed. や by ... のような、証明を組み立てる専用の層がありません。
公式論文が、この点を明言しています。
（原文引用）
Metas should be seen as "expression-level tactics", meaning they can be seamlessly interwoven with standard Arend term constructs. In other words, unlike Coq, Arend does not have separate "proof" and "term" levels.
（筆者による日本語訳）
メタは「式レベルのタクティク」と見なすべきである。すなわち、標準の Arend の項の構文と、継ぎ目なく織り交ぜることができる。言い換えれば、Coq とは違い、Arend には「証明」と「項」という別々の階層がない。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
本連載で示したコードは、すべて項を直接記述する形でした。
\func c : toNat (mySuc (mySuc myZero)) = 2 => idp
これは Agda に近い記述のしかたです。
違う点 ── 「メタ」という仕組みがあります
Arend には \meta という機能があり、公式ドキュメントは、この機能を「標準タクティク」と呼んでいます。
\meta とは、Arend の式を生成・変形・探索するための拡張機構です。矛盾からの自動証明や穴埋めにも使えるため、結果として、タクティクに似た役割を果たします。公式ドキュメントは「式レベルのタクティク」と呼んでいます。通常の項と同じ場所に記述できます。
📌 厳密性を担保した説明をすると ── Arend の meta は何に近いのか
Arend の \meta は、Lean や Coq の対話的タクティク言語に、そのまま対応するものではありません。Arend では、証明と通常の項を別の言語階層に分けず、メタを式の位置に記述できます。このため、本文では入門向けに「式レベルのタクティク」と説明していますが、より広くは、エラボレーション・式変換・探索を担う拡張機構として理解するのがよいです。
そして、arend-lib には実際に使えるメタが用意されています。contradiction は、そのひとつです。
（原文引用）
This meta will try to derive a contradiction from the context if no arguments are specified.
（筆者による日本語訳）
このメタは、引数を指定しなければ、文脈から矛盾を導こうと試みる。
出典：\module Logic.Meta, Arend Documentation
実機で試しました。
＜Arend のコード＞
\import Logic.Meta
\import Logic
\lemma equality {x y : Nat} (p : x = y) (q : Not (x = y)) : Empty => contradiction
\lemma usingTest (P Q : \Prop) (q : Q) (e : P -> Empty) (p : P) : Empty => contradiction
＜Arend の型検査結果＞
$ java -Xmx4g -jar Arend.jar -L libs -l arend-lib src/META1.ard
[ ] src.META1
--- Done (150ms) ---
contradiction の一語で、２つの補題が証明されました（Arend 1.10、arend-lib 1.10）。
コードの読み方を添えます。equality は、x = y の証明 p と、x = y の否定 q の両方が文脈にある状況です。contradiction は文脈を走査し、q p : Empty という矛盾を自動で組み立てています。
メタの定義について、公式ドキュメントは次のように述べています。
（原文引用）
Meta definitions are usually defined externally in Java code, but it is also possible to describe simple metas directly in Arend code.
（筆者による日本語訳）
メタ定義は通常、外部の Java コードで定義される。しかし、単純なメタを Arend のコードで直接記述することもできる。
出典：Meta definitions, Arend Documentation
「Arend のコードで直接記述する」ほうも、実機で試しました。
＜Arend のコード＞
\meta double x => x Nat.+ x
\func four : Nat => double 2
\func check : four = 4 => idp
＜Arend の型検査結果＞
$ java -jar Arend.jar src/META2.ard
--- Done (137ms) ---
arend-lib なしで、単純なメタを定義できました（Arend 1.10）。double 2 が 2 Nat.+ 2 に展開され、four = 4 が定義的に成立しています。
「Isar 記法」という言い方について
Isar は Isabelle の構造化証明言語です。Arend の記述のしかたは、Isar とは違います。
| 記述のしかた | 例 | 特徴 |
|---|---|---|
| Isar（Isabelle） | proof ... have ... show ... qed |
証明の構造を自然言語に近い形で記述する |
| タクティク（Coq、Lean） | intros. apply foo. exact bar. |
証明の手順を命令として記述する |
| 項スタイル（Agda、Arend） | => idp |
証明を項として直接記述する |
項スタイルとは、証明を項として直接記述する方式です。=> idp のように、証明そのものを式として記述します。Agda と Arend がこの形です。
Arend の基本は項スタイルです。そこにメタが加わります。
なお、1.12.0（告知）では natarith と intarith が追加されました。linarith 系の自動証明を、自然数と整数の割り算・剰余に拡張したものです。筆者は実機で試せていません。
出典：Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
まとめ
| 問い | 答え |
|---|---|
| タクティク言語はあるか | ない（Coq・Lean のような専用層はない） |
| 自動証明の仕組みはあるか | ある（\meta。公式は「標準タクティク」と呼ぶ） |
| Isar 記法か | 違う（項スタイル。Agda に近い） |
【本記事執筆者の見解】── AI は、どのスタイルを生成しやすいのか
本連載では、ここまでメタを一度も使ってきませんでした。しかし、AI との連携を考えるとき、メタは重要になると筆者は考えます。
AI が生成しやすいのは、タクティク列か、項か、メタか。筆者の整理は、次のとおりです。
| スタイル | AI にとって |
|---|---|
| タクティク列（Lean） | 一手ずつ生成し、検証器のフィードバックを受けやすい。AlphaProof がこの形 |
| Isar（Isabelle） | 自然言語に近く、LLM が生成しやすい可能性がある |
| 項スタイル（Agda、Arend） | 型が正確に分かっていれば生成できる。一手ずつのフィードバックは得にくい |
| メタ（Arend） | 自動証明を呼び出す一語。AI が生成すべき量が減る可能性がある |
この表は、筆者の推測です。スタイルごとの AI の生成しやすさを実証した研究は、筆者が調べた範囲では見つかっていません。
なお、別の連載で見たとおり、AI が生成する Lean の証明は「宣言的スタイルで骨格を立て、タクティクで埋める」形でした。arend-skills の arend-prove が示す作業手順も、「{?}（穴）を置いて骨格を立て、メタで埋める」形であり、構図が似ています。
出典：
sxhya/arend-skills, GitHub、【全４回連載（第１回）】AIが数学の証明を書けるようになった6年間, Qiita, 2026年8月12日
第６部 ── Arend の管理元と、その現状 ── JetBrains
第６回補足記事で見たように、Arend は 2026年8月時点で活発にメンテナンス、アップデートが継続されている言語です。
なお、メンテナンス元は JetBrains です。
Arend の管理元
JetBrains とは、IntelliJ IDEA などの開発ツールを作っている企業です。本社はアムステルダムにあります。
JetBrains Research とは、JetBrains の研究部門です。Arend は、この部門の「HoTT and Dependent Types Lab」の成果物です。
IntelliJ Arend とは、IntelliJ IDEA 上で動く、Arend の IDE プラグインです。
| 項目 | 内容 | 出典 |
|---|---|---|
| 開発元 | JetBrains Research | https://lp.jetbrains.com/research/hott-and-dependent-types/ |
| GitHub |
JetBrains/Arend、JetBrains/arend-lib、JetBrains/intellij-arend
|
https://github.com/JetBrains/Arend |
| 開発者 | Valery Isaev、Fedor Part、Sergey Sinchuk | 公式論文 |
| IDE | IntelliJ Arend | https://plugins.jetbrains.com/plugin/11162-arend |
開発は続いているのか ── 確認できた活動
| 日付 | 出来事 | 性質 |
|---|---|---|
| 2019年8月 | HoTT メーリングリストで公開を告知 | 研究者向け |
| 2020年4月 | 「Every proof assistant」セミナーで Isaev が講演 | 研究者向け |
| 2020年 | ICMS 2020 のセッションで発表 | 研究者向け |
| 2025年 | HoTT/UF 2025 ワークショップで、Part・Isaev・Sinchuk が「The Arend theorem prover」を発表 | 研究者向け |
| 2025年12月11日 | 1.11.0 をブログで告知 | リリース |
| 2025年12月22日 | IntelliJ プラグインを更新 | 保守 |
| 2026年7月30日 | 1.12.0 のプラグインを JetBrains Marketplace で配布 | リリース |
| 2026年8月4日 | 1.12.0 をブログで告知 | リリース |
| 2026年8月10日 | 論文の完成をブログで告知 | 研究者向け |
出典
- HoTT/UF 2025
- Every proof assistant セミナー
- ICMS 2020
- IntelliJ Arend プラグイン
- Arend 1.11.0 released, Arend Theorem Prover, 2025年12月11日
- Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
- Paper on Arend, Arend Theorem Prover, 2026年8月10日
開発は、続いています。2019年から2026年まで、ブログではリリースノートの公開が継続しています。
そして、1.12.0（告知）では JetBrains Educational plugin への対応（course builder、project generator、task checker）が加わりました。教育向けの経路です。
出典：Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
一方で、JetBrains の製品発表やマーケティングといった、一般の開発者に向けた普及活動は、筆者が調べた範囲（2026年9月5日時点）では確認できませんでした。
JetBrains にとっての位置づけ
製品ではなく、研究プロジェクトです。ただし、活発に更新されています。
2019年の公開当時、Hacker News で次のように評されていました。
（原文引用）
I guess JetBrains wants to be in this space once things mature
（筆者による日本語訳）
JetBrains は、この分野が成熟したときに、そこにいたいのだろう。
７年後のいまも、その姿勢は変わっていないように見えます。
なお、JetBrains Research の Arend チームは、サンクトペテルブルクにありました。2022年のロシアのウクライナ侵攻を受けて、JetBrains はロシアでの販売と研究開発活動を無期限に停止し、2023年2月にロシア法人を清算しました。
Arend チームがどうなったかは、公開情報からは確認できませんでした。ただし、2025年に HoTT/UF での発表があり、2026年にリリースの告知と論文の公開があったことは、開発が続いている根拠です。
GitHub とブログの不整合
ひとつ、注意すべき事実があります。
| 項目 | 状態（2026年9月5日に確認、9月6日に再確認） |
|---|---|
| ブログ | 1.11.0（2025年12月）と 1.12.0（2026年8月）を告知 |
JetBrains/Arend の最新タグ |
v1.10（9月6日の時点でも変わらず） |
JetBrains/arend-lib の最新タグ |
v1.10.0（9月6日の時点でも変わらず） |
| GitHub releases/latest の Arend.jar | 1.10（本連載で使用したものと同一） |
出典：
JetBrains/Arend, GitHub、JetBrains/arend-lib, GitHub、Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
ブログでは告知されていますが、1.12.0 の jar は GitHub からは取得できませんでした。1.12.0 のプラグインは JetBrains Marketplace で配布されています。
本記事の実機検証を 1.10 で行ったのは、この不整合のためです。
コミュニティの現状
別の連載で、Lean の Zulip コミュニティが「詰まったときに質問できる場所」として重要だと述べました。Arend には、それに相当する場所があるでしょうか。
| 場所 | 状態（2026年9月5日〜6日に確認） |
|---|---|
| Gitter | ルーム arend-lang/community は存在。Gitter 自体が Matrix（Element）へ移行済みで、投稿履歴の閲覧には Matrix クライアントが必要（筆者の環境からは読めなかった）。検索エンジンのキャッシュには2020年頃の質疑が残る |
| GitHub Issues | 総数 257 件、うち open 49 件（2026年9月6日、筆者実測）。作成日の新しい順で見ると、直近の起票は2025年10月2日（#354）で、2026年に入ってからの新規起票は確認できなかった |
| HoTT メーリングリスト | 2019年8月の公開スレッド以降、Arend への言及は未確認 |
| Zulip | Arend のチャンネルは確認できなかった |
| JetBrains Educational plugin | 1.12.0（告知）で対応。教育向けの経路 |
出典：
JetBrains/Arend, GitHub、arend-lang/community, Gitter、GitHub Issues の集計は本稿 Appendix A-11（筆者の実測、2026年9月6日）、Arend 1.12.0 released, Arend Theorem Prover, 2026年8月4日
「コミュニティがない」と断定することはできません。確認した日付と場所を記したうえで、この時点では、Lean の Zulip に相当する規模の場所は確認できなかった、と述べるにとどめます。
タロウくんの質問 ── 数学以外の利用事例
タロウくん：
先生、Arendは、数学の定理の証明が合っているか(論理の飛躍なく成立するか)、間違っているかを検証する目的以外に、汎用関数型プログラミング言語としてつかったり、数学ではなく、ソフトウェアが仕様どおり書かれているかどうか調べる目的で使ったりされている利用事例はありませんか？
専任講師：
公式には「定理証明支援系であり、プログラミング言語でもある」と述べられています。
（原文引用）
Arend is a theorem prover and a programming language based on Homotopy Type Theory.
（筆者による日本語訳）
Arend は、ホモトピー型理論に基づく定理証明支援系であり、プログラミング言語である。
出典：
JetBrains/Arend, GitHub README
しかし、筆者が調べた範囲（2026年9月5日時点。GitHub、公式ドキュメント、公式論文）では、次のとおりです。
| 用途 | 事例 |
|---|---|
| 汎用関数型プログラミング言語として | 公開事例は確認できなかった |
| ソフトウェアの仕様検証 | 公開事例は確認できなかった。arend-lib にもソフトウェア検証の形式化はない |
| 数学の形式化 | arend-lib（構成的代数、位相、合成ホモトピー論。1.12.0（告知）では代数幾何、解析を追加。出典：Arend 1.12.0 released） |
| 計算機科学の形式化 | ある。高階項書き換え系（下で述べます） |
タロウくん：
・・・「計算機科学の形式化」というのは、何ですか。
専任講師：
公式論文が、arend-lib の内容の３番目として挙げています。
（原文引用）
- Computer science. Currently this part consists of formalization of high-order term rewriting systems. The planned future formalizations include fragments of computational complexity theory.
（筆者による日本語訳）
- 計算機科学。現在、この部は高階項書き換え系の形式化から成る。将来の形式化として、計算量理論の断片が計画されている。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第１節
「数学の形式化のみ」ではありません。しかし、これは計算機科学の理論の形式化であって、実務のソフトウェアが仕様どおりに動くかを検証した事例とは違います。
タロウくん：
・・・他の処理系では、そうした事例があるのですか。
専任講師：
あります。対比の表を置きます。
| Rocq／Coq | Lean 4 | Isabelle/HOL | Arend 1.10 | |
|---|---|---|---|---|
| 数学の形式化 | Mathematical Components | Mathlib | AFP | arend-lib |
| コード抽出 | OCaml、Haskell、C++（Crane） | 抽出ではなく、Lean 4 自身がコンパイルできる | SML、Scala、OCaml、Haskell | なし |
| ソフトウェア検証の実績 | CompCert、CertiCoq | AWS Cedar | seL4 | 確認できなかった |
| REPL での計算 | あり | あり | あり | あり |
出典
- Welcome to a World of Rocq
- LLM＋Rocq＋C++ 抽出の事例："Trustworthy Software Project Generation: a Case Study with an Interactive Theorem Prover", arXiv:2605.26017, 2026年5月
タロウくんの質問 ── コード抽出とは何か
タロウくん：
コード抽出はなにを意味していますか？
専任講師：
証明支援系のなかで書いた定義を、普通のプログラミング言語のコードに変換して、実行できるようにすることです。
タロウくん：
・・・証明支援系のコードは、そのままでは実行できないのですか。
専任講師：
実行できる処理系もあります。しかし、証明支援系のコードには、証明の部分が含まれています。
証明は、プログラムの正しさを保証するためのものであって、実行時には使われません。
📌 厳密性を担保した説明をすると ── 「証明は実行時には使われない」とはどういう意味か
厳密には、証明が実行時に絶対に関与しない、というわけではありません。処理系ごとに事情が違います。
Coq の抽出（extraction）は、Prop に属する証明部分を消去して OCaml や Haskell のコードを取り出します。Agda には、実行に影響しない引数に消去の印を付ける仕組みがあります。Lean 4 はコンパイラを持ち、Prop の証明はコンパイル時に消去されます。いずれも「証明を消しても実行結果が変わらない」ことが理論的に保証されている範囲で消去します。
一方で、証明の中身が計算に使われる設計もありえます。たとえば、存在証明から具体的な値を取り出して実行に使う場合、その証明は消去できません。消去できるかどうかは、証明がどの階層（Prop か Type か、Arend なら \Prop か \Set か）に置かれているかで決まります。
本文の「実行時には使われません」は、「消去可能な階層に置かれた証明は、抽出・コンパイルの際に消去される」という意味の、入門向けの言い方です。
タロウくん：
・・・証明を取り除いて、実行に必要な部分だけを取り出す。
専任講師：
そのとおりです。それが、コード抽出です。
| 処理系 | 抽出先 |
|---|---|
| Rocq／Coq | OCaml、Haskell、C++（外部ツール Crane） |
| Isabelle/HOL | SML、Scala、OCaml、Haskell |
| Lean 4 | 抽出ではなく、Lean 4 自身がコンパイルされて実行される |
| Agda | Haskell、JavaScript |
| Arend 1.10 | なし |
「Lean 4 は抽出ではなくコンパイル」という区別に、注意してください。Lean 4 のコードは、Lean 4 自身のコンパイラで実行可能なバイナリになります。別の言語へ変換する抽出とは、仕組みが違います。
タロウくん：
・・・なぜ、抽出が必要なのですか。
専任講師：
ソフトウェア検証で使うためです。
「このプログラムは仕様どおりに動く」と証明したら、その証明済みのプログラムを実際に動かしたい。
CompCert という C コンパイラは、Rocq で正しさが証明され、OCaml に抽出されて動いています。
タロウくん：
・・・Arend には、それがない。
専任講師：
1.10 の CLI を実機で確認しました。オプションは -i（REPL）、-p（印字）、-t（テスト）、-r（再コンパイル）、-c（二重検査）などで、extract、compile、run に相当するものはありません。
REPL で項を正規化する意味での計算はできます（第４部で suc (suc zero) が 2 に評価されました）。しかし、外部の言語へ抽出して実行する仕組みは備わっていません。
arend-lib にも、ソフトウェア検証の形式化はありません。公式論文も、ソフトウェア検証とコード抽出には触れていません。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"
Arend は、数学の形式化を主目的に設計されています。ソフトウェア検証は、設計の目的に入っていません。この点を、欠陥として読まないでください。目的の違いです。
タロウくん：
・・・第２回目の記事で、Arend は「計算しきる力」を手放したと伺いました。
専任講師：
関係があると、筆者は考えます。
計算しきる力を手放したことと、コード抽出を備えていないことは、どちらも「実行」より「証明」を優先した設計の帰結である、というのが筆者の解釈です。
タロウくん：
・・・設計の目的が、一貫している。
第７部 ── 連載の総括 ── 使わない道具から、何を持ち帰るか
連載を通じて訂正した誤りの一覧
本連載では、実機検証と一次資料の精読によって、筆者自身の記述を何度も訂正しました。
総括の最初に、この一覧を置きます。
| 回 | 訂正した内容 | どうやって見つけたか |
|---|---|---|
| 第５回目 |
same (a b k : Nat) の k に 0 を渡せるため、Q が潰れる |
Arend 1.10 で実機検証。q 1 2 = q 3 5 が通ってしまった |
| 第５回目 |
record Group に群の法則がなかった |
第４回目の記事との整合を確認して気づいた。Arend 1.10 で修正したコードを検証 |
| 第６回目 | 第５回目の予告「Agda や Lean では証明を持ち回る」の Lean が誤り | Lean 4.33.1 で実機検証。rfl が通った |
| 第６回目 | 第４回目の「可述的とは、自分自身を含む集まりを禁じる立場」が不正確 | 公式ドキュメントとの照合 |
| 第６回目 | 第４回目の「ホモトピーレベルとは、等しさの根拠が何本ありうるか」が不正確 | Awodey の定義との照合 |
| 第６回目 | 第４回目の「宇宙とは、型を集めたもの」が不正確 | 公式ドキュメントとの照合 |
| 第６回目 | コラムで「\Prop が証明無関係でない理由を、公式資料に確認できなかった」と書いたが、論文第2.2節(2)(e)に理由があった |
第７回目の記事の執筆前に、論文を全文精読した |
| 第７回目の執筆前 | 「arend-skills は存在しない」と一度は判断した |
論文の脚注14 で、リポジトリの URL を見つけた |
これらの訂正のうち実機検証によるものは、すべて Arend 1.10（および Lean 4.33.1、Agda 2.6.3）で発見した。
Arend 1.12.0 で同じ結果になるかどうかは、確認できていない。
最後の２行について、補足します。
「arend-skills は存在しない」という判断は、GitHub の検索で JetBrains のリポジトリだけを探し、開発者個人のリポジトリ（sxhya/arend-skills）を見落としたことによる誤りでした。論文を最後まで読み、脚注14 の URL を見つけて訂正できました。
出典：
sxhya/arend-skills, GitHub、Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第５節
Web 検索だけでは見落とし、一次資料を読んで訂正できた。「一次資料を読む」という本連載の方法論が、最終回の執筆でも機能しました。
訂正の一覧を置く理由 ── 本連載と AI の、同じ構図
この一覧を置く理由は、連載の方法論そのものが、AI による証明検証の構図と同じだからです。
| 生成する側 | 弾く側 | |
|---|---|---|
| AI による定理証明 | AI が証明を生成する | 検証器が弾く |
| 本連載 | 筆者が記述を書く | 実機が弾く |
「同じ構図」であって「同じもの」ではありません。比喩として述べています。
「実機で確かめることで、誤りが見つかる」という経験が、本連載の最も具体的な成果です。
そして、その経験は読者にも再現できます。各回の Appendix に手順を載せてきた理由が、ここにあります。
連載の総括の表 ── 何を手放して、何を得たか
本連載シリーズの各回で見てきた設計判断を、一覧にします。今回は「AI にとって」の列を加えます。
| 回 | 手放したもの | 得たもの | AI にとって |
|---|---|---|---|
| 第２回目 | 計算しきる力 | 仕様の単純さ | 生成する構文が単純になる |
| 第４回目 | 土台の小ささ | 階層を組み上げる自由 | 変換関数を生成せずに済む |
| 第５回目 | ── | 高次帰納型の定義の単純さ（第２回目の見返り） |
data に２行加えれば済む |
| 第６回目 | 宇宙の仕様の単純さ | 証明を持ち回らずに済むこと | 生成するトークンが減る |
「AI にとって」の列は、すべて筆者の推測です。第３部で、実機で検証できる範囲（コードの長さ）は検証しました。それ以外は、推測のまま残ります。
そして、各回の設計判断を、公式論文の記述と突き合わせます。開発者たちが、それぞれの判断について何と述べているかです。
第２回目の「計算しきる力」について。
（原文引用）
the MLTT property that every closed term of type Nat evaluates to a canonical number does not hold in Arend
（筆者による日本語訳）
Nat 型のすべての閉じた項が標準形の数に評価される、という MLTT の性質は、Arend では成り立たない。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover 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
（筆者による日本語訳）
Lean、Coq、Agda といった MLTT 族の主要な定理証明支援系の開発は、コア理論において包摂的部分型付けとマニフェストフィールドを避けてきた。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第2.3.5節
主要な処理系が避けてきた仕組みを、Arend はあえてコアに入れました。第４回目の記事で見た階層の支え方は、その帰結です。
第５回目の「高次帰納型の定義の単純さ」について。
（原文引用）
the HoTT book style proof of T² ≅ S¹ × S¹ is rather involved
（筆者による日本語訳）
トーラスが円周２つの直積と同値であることの、HoTT book 流の証明は、かなり込み入っている。
出典：
Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第2.4節
論文は、この同値が Arend では構成子ごとの idp で証明できることを、同じ節で述べています。第５回目の記事で見た「data に道の構成子を並べられる」設計の見返りです。
設計判断を読む目は、道具を選ぶ目になる
本連載の読者として想定してきたのは、Haskell を学び始めて３か月のプログラマです。
その読者が Arend を実務で使う可能性は、低いと筆者は考えます。第４回目・第６回目の記事で述べた見解（いま定理証明支援系をひとつ選ぶなら、Lean 4 を選ぶのが現実的である）を、最終回でも維持します。
しかし、６回かけて読んだ設計判断は、Lean を使うときにも効きます。
| Arend で学んだこと | Lean を使うときに |
|---|---|
| 区間を型の中に置くか、外に置くか | Lean が計算しきる力を持つ理由と、Arend がそれを手放した理由が分かる |
| 階層をどこで支えるか | Mathlib の型クラス階層が、なぜあの形なのかが分かる |
| 証明を引数で運ぶか、型に語らせるか | Lean で isSet を持ち回らずに済む理由（UIP）が分かる |
| 何を手放して、何を得たか | Lean が UIP を認めた代償（HoTT を扱えない）が分かる |
設計判断を読む目は、道具を選ぶ目になる。
それが、本連載を通じて読者に持ち帰ってほしいことです。
第１回目の記事の問いへの、６回分を踏まえた答え
第１回目の記事で、「なぜ Arend が生まれたのか」と問いました。
６回分を踏まえた答えは、こうなります。
Coq・Lean・Agda が避けてきた仕組み（区間を型の中に置くこと、包摂的部分型付け、宇宙の２つ目の軸）を、「形式化の実践」という基準で選び直すためです。
その選択の結果、Arend は、HoTT と高次帰納型を基礎にした合成ホモトピー論の形式化（円周、トーラス、Hopf、Blakers–Massey）を arend-lib に持っています。この形の形式化は、Lean 4 の Mathlib にはありません。
AI の主流が Lean であることは、この先も変わらないと筆者は考えます。しかし、AI が HoTT の定理を証明する場面が来たとき、Lean 4 の標準的な型理論では、Arend や Cubical Agda のように HoTT と高次帰納型をそのまま扱うことはできません（第５回目・第６回目の記事で実機で示しました）。選択肢は Cubical Agda か Arend になります。そして、そのとき第６回目の記事で見た「証明を持ち回らない」設計の違いが効きます。
📌 厳密性を担保した説明をすると ── Lean 4 で HoTT は「使えない」のか
「AI が HoTT の定理を証明するなら Lean 4 は使えない」と言い切るのは強すぎます。
正確には、次のようになります。
Lean 4 の標準的な型理論は、Prop の proof irrelevance から UIP が従う設計です。
このため、円周のような高次帰納型をそのまま定義しても、パスの構造が潰れます（第５回目の記事の実機検証）。「そのまま扱うことはできない」は、この意味です。
ただし、公理を追加したり、等式型を使わずにパス構造を別の方法で記述したりする形で、Lean の上に HoTT 的な体系を構築する試みは存在します。
「Lean で HoTT 関連の数学が一切できない」という意味ではありません。
本文が述べているのは、Arend や Cubical Agda が処理系の設計としてネイティブに持っている扱いを、Lean 4 の標準の型理論は持たない、という比較です。
「AI × HoTT」という場面が現実になるかどうかは、分かりません。その保証はどこにもありません。しかし、その場面が来たとき、Arend の設計判断が意味を持ちます。
仕様が正しいかどうかは、形式的ではない
最後に、もうひとつだけ、本連載の枠を超える論点に触れます。
別の連載の記事で、次を述べました。
証明支援系が保証するのは「この証明は、この仕様を満たす」こと。
保証しないのは「この仕様は、人間が望んでいることを表している」こと。
この論点を、Arend の文脈で再訪します。
連載を通じて、Arend の設計判断を見てきました。区間の置き場所、階層の支え方、宇宙の軸。
どの判断も、「形式化の実践」という人間の判断でした。「何を形式化したいか」「どの性質を優先するか」を決めるのは、検証器ではありません。
そして、Arend 公式論文の著者たちが下した判断を、本連載は追体験してきました。AI が証明の生成を担うようになっても、この部分は残ります。
【本記事執筆者の見解】── Arend を学ぶ価値は、どこにあるのか
筆者の見解を、３点にまとめます。
第１に、Arend を学ぶ価値は、Arend を使うことにはありません。AI の主流は Lean であり、実務で定理証明支援系を選ぶなら Lean 4 が現実的です。この見解は、第４回目の記事から変わっていません。
第２に、Arend を学ぶ価値は、設計判断を読む経験にあります。「何を手放して、何を得たか」を６回分読んだ経験は、Lean を含むどの道具を選ぶときにも効きます。
第３に、JetBrains が一般向けの普及活動をしていないということは、日本語の入門記事が存在する意味が、より大きいということでもあります。本連載が、Arend という設計判断の記録への、日本語で読める入口になっていれば、筆者としては目的を果たせたと考えます。
なお、本連載で扱った HoTT には、さらに先の研究があります。道を一方向の矢印に一般化する「有向 HoTT」です。本稿末尾のコラム欄（有向 HoTT への展望）をご参照ください。
６回、お付き合いいただき、ありがとうございました。
本連載シリーズは、本記事で完結します。
コラム
📌 中上級者向け：有向 HoTT への展望
第１回目の記事の予告に記した「有向 HoTT への展望」を、このコラムで扱います。研究段階の理論であり、確定した事実ではなく展望として読んでください。
有向 HoTT（directed HoTT）とは、通常の HoTT の「道」（対称な等しさ）を、「矢印」（非対称な射）に一般化する理論です。
なぜ必要とされるのでしょうか。圏論では、射は一方向です。$A$ から $B$ への射があっても、$B$ から $A$ への射があるとは限りません。通常の HoTT の道は対称であるため、圏を型理論の内部で直接扱うことに向いていません。道を矢印に一般化できれば、型そのものが圏（さらには∞-圏）として振る舞います。
主要な研究を挙げます。
| # | 著者 | タイトル | 年 |
|---|---|---|---|
| ① | Emily Riehl, Michael Shulman | A type theory for synthetic ∞-categories（arXiv:1705.07442） | 2017 |
| ② | Paige Randall North | Towards a directed homotopy type theory（arXiv:1807.10566） | 2019 |
| ③ | Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz | Directed univalence in simplicial homotopy type theory（arXiv:2407.09146） | 2024 |
| ④ | Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz | The Yoneda embedding in simplicial type theory（arXiv:2501.13229） | 2025 |
| ⑤ | Jacob Neumann | A Judgmental Construction of Directed Type Theory（arXiv:2510.17494） | 2025 |
| ⑥ | Andrea Laretto, Fosco Loregian, Niccolò Veltri | Di- is for Directed: First-Order Directed Type Theory via Dinaturality（POPL 2026） | 2026 |
出典：
directed homotopy type theory, nLab
実装も、実験的なものが現れています。
| 名前 | 内容 | 出典 |
|---|---|---|
| rzk | simplicial type theory の実験的な証明支援系。Riehl らの形式化に使われている | arXiv:2604.18668, 2026年4月 |
| Narya | Shulman による高次元型理論の証明支援系 | Michael Shulman: Papers |
実用的な証明支援系に有向 HoTT が組み込まれた例は、2026年9月時点ではありません。
では、Arend との関係はどうでしょうか。ここに、注目すべき一節があります。Arend の公式論文が、将来の方向として有向 HoTT を明記しているのです。
（原文引用）
Recently, proposals for directed HoTT [8, 7], where types are ∞-categories, have emerged. Future versions of Arend are expected to support a variant of directed HoTT.
（筆者による日本語訳）
最近、型が ∞-圏である有向 HoTT の提案が現れた。Arend の将来のバージョンは、有向 HoTT の変種を支援すると期待される。
出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend", 第１節
本連載との接続を述べます。第４回目の記事で、圏を Arend のクラスとして扱いました。有向 HoTT は、その圏を型理論の内部で自然に扱うための試みです。Arend が実際にこの方向へ進むかどうかは、今後のリリースを待つほかありません。
Appendix ── 実機検証の記録
本記事に掲載したコードは、すべて次の環境で検証しました（2026年9月5日）。
| 処理系 | リリースバージョン |
|---|---|
| Arend | 1.10（Java 21。GitHub releases/latest の Arend.jar） |
| arend-lib | 1.10 |
| Agda | 2.6.3（本記事の執筆環境に apt で導入し、CARRY10.agda の型検査を実施。2026年9月6日） |
| Lean | 4.33.1（第４部の比較対象） |
A-1. 検証環境の再構築手順
# Arend 1.10
curl -sSL -o /tmp/Arend.jar https://github.com/JetBrains/Arend/releases/latest/download/Arend.jar
# arend-lib 1.10
curl -sSL -o /tmp/arend-lib.zip https://github.com/JetBrains/arend-lib/releases/latest/download/arend-lib.zip
mkdir -p /tmp/libs2 && cd /tmp/libs2 && unzip -q /tmp/arend-lib.zip -d arend-lib && mkdir -p arend-lib/test
# プロジェクト（arend-lib あり）
mkdir -p /tmp/aproj/src && cd /tmp/aproj && printf 'sourcesDir: src\ndependencies: [arend-lib]\n' > arend.yaml
# 実行（arend-lib あり）
java -Xmx4g -jar /tmp/Arend.jar -L /tmp/libs2 -l arend-lib src/FILE.ard
# 実行（arend-lib なし）
java -jar /tmp/Arend.jar src/FILE.ard
# REPL
java -jar /tmp/Arend.jar -i
A-2. META1.ard ── contradiction メタ（第５部）
\import Logic.Meta
\import Logic
\lemma equality {x y : Nat} (p : x = y) (q : Not (x = y)) : Empty => contradiction
\lemma usingTest (P Q : \Prop) (q : Q) (e : P -> Empty) (p : P) : Empty => contradiction
結果：Done (150ms)。arend-lib の読み込みが必要。
A-3. META2.ard ── \meta の直接定義（第５部）
\meta double x => x Nat.+ x
\func four : Nat => double 2
\func check : four = 4 => idp
結果：Done (137ms)。arend-lib は不要。
A-4. CARRY10.ard ── \Set0 で済ませる10関数（第３部）
\import Paths
\import Logic
\func useIsSet1 (A : \Set0) (x y : A) (p q : x = y) : p = q => prop-isProp p q
\func useIsSet2 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet1 A x y p q
\func useIsSet3 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet2 A x y p q
\func useIsSet4 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet3 A x y p q
\func useIsSet5 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet4 A x y p q
\func useIsSet6 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet5 A x y p q
\func useIsSet7 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet6 A x y p q
\func useIsSet8 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet7 A x y p q
\func useIsSet9 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet8 A x y p q
\func useIsSet10 (A : \Set0) (x y : A) (p q : x = y) : p = q => useIsSet9 A x y p q
結果：Done (102ms)。856文字。isSet の証明を引数に取る箇所は０。
A-5. CARRY10.agda ── isSet を10関数で持ち回る（第３部）
{-# OPTIONS --without-K #-}
module CARRY10 where
open import Agda.Builtin.Equality
isSet : Set → Set
isSet A = (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet1 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet1 A h x y p q = h x y p q
useIsSet2 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet2 A h x y p q = useIsSet1 A h x y p q
useIsSet3 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet3 A h x y p q = useIsSet2 A h x y p q
useIsSet4 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet4 A h x y p q = useIsSet3 A h x y p q
useIsSet5 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet5 A h x y p q = useIsSet4 A h x y p q
useIsSet6 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet6 A h x y p q = useIsSet5 A h x y p q
useIsSet7 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet7 A h x y p q = useIsSet6 A h x y p q
useIsSet8 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet8 A h x y p q = useIsSet7 A h x y p q
useIsSet9 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet9 A h x y p q = useIsSet8 A h x y p q
useIsSet10 : (A : Set) → isSet A → (x y : A) (p q : x ≡ y) → p ≡ q
useIsSet10 A h x y p q = useIsSet9 A h x y p q
結果：型検査を通過（Agda 2.6.3、--without-K。本記事の執筆環境で2026年9月6日に実施）。1,372文字。h の出現20回（署名10＋本体10）。
A-6. AI1.ard ── 課題①：加法の交換法則（第４部、２回目で通過した出力）
\func pmap {A B : \Type} (f : A -> B) {a a' : A} (p : a = a') : f a = f a' => path (\lam i => f (p @ i))
\func \infixr 9 *> {A : \Type} {a a' a'' : A} (p : a = a') (q : a' = a'') : a = a'' \elim q | idp => p
\func plus-zero (n : Nat) : n Nat.+ 0 = n => idp
\func zero-plus (n : Nat) : 0 Nat.+ n = n \elim n
| 0 => idp
| suc n => pmap suc (zero-plus n)
\func plus-suc (n m : Nat) : n Nat.+ suc m = suc (n Nat.+ m) => idp
\func suc-plus (n m : Nat) : suc n Nat.+ m = suc (n Nat.+ m) \elim m
| 0 => idp
| suc m => pmap suc (suc-plus n m)
\func plus-comm (n m : Nat) : n Nat.+ m = m Nat.+ n \elim m
| 0 => inv (zero-plus n)
| suc m => pmap suc (plus-comm n m) *> inv (suc-plus m n)
\where \func inv {A : \Type} {a a' : A} (p : a = a') : a' = a \elim p | idp => idp
結果：Done (254ms)。１回目は Termination check failed。
A-7. AI4.ard ── 課題②：円周と loop（第４部、２回目で通過した出力）
\data S1 | base | loop : base = base
\func inv {A : \Type} {a a' : A} (p : a = a') : a' = a \elim p | idp => idp
\func loop-inv : base = base => inv loop
\func loop-twice : base = base => path (\lam i => loop @ i) *> loop
\where \func \infixr 9 *> {A : \Type} {a a' a'' : A} (p : a = a') (q : a' = a'') : a = a'' \elim q | idp => p
結果：Done (171ms)。１回目は Cannot resolve reference 'inv' in Path。
A-8. AI1.lean ── 課題①の Lean 4 での比較（第４部、２回目の出力）
theorem plus_comm (n m : Nat) : n + m = m + n := Nat.add_comm n m
結果：通過（Lean 4.33.1）。１回目は simp の警告つきで通過。
A-9. arend-lib 1.10 の実測（第２部）
$ find arend-lib/src -name '*.ard' | wc -l
233
$ find arend-lib/src -name '*.ard' -exec cat {} + | wc -l
41316
$ ls arend-lib/src/Homotopy/
Connected.ard Cube.ard Fibration.ard Hopf.ard Image.ard Join.ard K1.ard
Localization Loop.ard Pointed.ard Pushout.ard Space.ard Sphere Sphere.ard
Square.ard Suspension.ard Torus.ard Truncation.ard
分野別のファイル数：Algebra 73、Topology 34、Homotopy 24、Logic 20、Category 19、Arith 11、Set 10、Data 10、Order 7、Analysis 5、Equiv 5。
A-10. REPL の評価（第４部）
$ java -jar Arend.jar -i
>suc (suc zero)
2
Mathlib の公式統計（Counts）
Definitions: 136,422 / Theorems: 287,051 / Contributors: 772
出典：
Mathlib statistics, Lean Community（2026年9月6日に筆者取得）
Gitter は Matrix（Element）へ移行しており、筆者の環境（JavaScript を実行しない取得）ではルーム arend-lang/community の投稿履歴を読めませんでした。ルームの存在と、2020年頃の質疑が検索エンジンのキャッシュに残っていることのみ確認しています。