1章 · 2026 年の定理証明支援系マップ — 7 つの陣営

2026 年、定理証明支援系(proof assistant、theorem prover)のエコシステムはかつてないほど活気に満ちている。10 年前には「数学者の玩具」と呼ばれていた道具が、今では**世界トップクラスの数学者の日常ノート**であり、**OS カーネルや暗号ライブラリの安全証明書**となっている。

現在生きている主要な陣営は次の通り。

| 陣営 | 核心 | 作者 | 色合い |

| --- | --- | --- | --- |

| **Lean 4** | mathlib(100 万定理超) | Leonardo de Moura(AWS) | 数学中心、爆発的成長 |

| **Rocq**(旧 Coq) | 25 年史、CompCert | INRIA(フランス) | 古典、産業検証 |

| **Agda** | 依存型の典型 | Chalmers(スウェーデン) | 学術 / 型理論 |

| **Idris 2** | プログラミング志向 | Edwin Brady | 実用的依存型 |

| **Isabelle/HOL** | seL4 を証明 | Cambridge / TUM | 古典 HOL、自動化が強い |

| **F*(FStar)** | HACL* 暗号検証 | Microsoft Research | 実用 + Z3 |

| **Liquid Haskell** | refinement types | UCSD | Haskell 上の SMT |

これに加え、2 つの潮流が 2026 年の空気を変えている。

1. **AI 補助** — DeepMind の AlphaProof は IMO 2024 で銀メダル相当の点数(6 問中 4 問、28/42 点)を獲得し、Anthropic は AI 数学オリンピアード($5M 賞金)や mathlib 検索・自動証明に参加。Claude・GPT 系 LLM は Lean tactic 生成器として日常的に使われる。

2. **一流現役数学者の参戦** — Terence Tao(2006 年フィールズ賞)は自分の論文(PFR 予想など)を公開で Lean に形式化し、Kevin Buzzard(Imperial College)は「数学科の学部生は皆 Lean を学ぶべきだ」と公開講演する。

本記事は上記の 7 陣営を 1 つずつ、続いて AI・SMT・産業事例の順に追う。

> **用語**: proof assistant とは「人間が証明を書き、コンピュータが 1 行ずつ検査する」道具。SMT solver とは「論理式が充足可能かを自動判定する」バックエンドエンジン(Z3、CVC5)。両者が組み合わさると、F\* や Liquid Haskell のように普通のコードも検証できる。

2章 · Lean 4 — Leonardo de Moura、AWS、爆発的成長

Lean の短い歴史

Lean は Microsoft Research で **Leonardo de Moura**(Z3 のあの人)が 2013 年に始めたプロジェクトだ。Lean 2(2015)、Lean 3(2017)を経て、Lean 4 が 2021 年に安定化した。2023 年、de Moura は Microsoft を離れ、**Amazon Web Services** の Automated Reasoning Group に合流。AWS は Lean 4 コンパイラの開発と mathlib インフラを支援している。

Lean 4 の正体

Lean 4 は単なる定理証明支援系ではなく、**完全な依存型関数型プログラミング言語**でもある。

-- 自然数の足し算の交換則

theorem add_comm (a b : Nat) : a + b = b + a := by

induction b with

| zero => simp

| succ b ih => rw [Nat.add_succ, ih, Nat.succ_add]

`theorem` が命題、`:=` が証明。`by ... ` ブロックの中で `induction`、`simp`、`rw`(rewrite)などの tactic を呼んで一段ずつゴールを解いていく。

Lean 4 が速い理由

- **自己ホスティングのコンパイラ**: Lean 4 自体が Lean で書かれている(self-hosting)。C にコンパイルされ、ネイティブ性能で走る。

- **マクロシステム**: Racket 風のマクロでドメイン特化構文をユーザが作れる。mathlib はこれで数学記法をそのまま使う。

- **型クラス**: Haskell 風の型クラスで抽象化が綺麗。

インストールと最初の証明

elan: Lean のバージョンマネージャ(rustup 的なもの)

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

新規プロジェクト

lake new my_first_lean

cd my_first_lean

lake build

VS Code の Lean 4 拡張をインストールし、マウスをホバーするだけで現在のゴールと型がリアルタイムに見える。この InfoView が Lean ユーザに最初に愛される機能だ。

2026 年現在のステータス

- Lean 4.10+ 安定

- mathlib は 100 万定理突破(次章)

- 学部講義に採用: Imperial College、Brown、Berkeley、CMU

- 産業: AWS Automated Reasoning、Galois、Kestrel Institute

> Lean Community サイト [leanprover-community.github.io](https://leanprover-community.github.io/) と [Zulip チャット](https://leanprover.zulipchat.com/)は事実上 24/7 生きている。質問を投げれば 1 時間以内に誰かが返してくる。

3章 · mathlib — 100 万定理、Terence Tao のノート

mathlib とは

**mathlib4**(Lean 4 用)は人類史上最大の形式化された数学ライブラリだ。2026 年 5 月時点で:

- **1,000,000+ 定理 / 補題 / 定義の合計**(2026 年初に突破)

- 約 30 万行の定義、80 万行の証明

- `git log` で 600+ 名の貢献者

- 群・環・体・位相・測度・圏論・解析・代数幾何 — 学部から大学院まで、ほぼ全ての数学

構造と記法

-- 実解析: 積分の単調性

theorem integral_mono (f g : ℝ → ℝ)

(hf : Integrable f) (hg : Integrable g)

(h : ∀ x, f x ≤ g x) :

∫ x, f x ≤ ∫ x, g x := by

exact MeasureTheory.integral_mono hf hg h

普通の数学とほぼ同じ記法で書けるのが mathlib の核心だ。`ℝ`、`∫`、`≤` は単なる Unicode 文字。Lean 4 のマクロシステムがこれを可能にしている。

Terence Tao と PFR Project

2023 年 11 月、Terence Tao(フィールズ賞)は Tim Gowers、Ben Green、Freddie Manners と共同で証明した [Polynomial Freiman-Ruzsa 予想](https://arxiv.org/abs/2311.05762) を、**約 3 週間で** Lean に形式化するプロジェクトを開始した。経過は彼のブログ `terrytao.wordpress.com` で公開された。

中心メッセージ: **「今や数学者の形式化が 1 か月もかからない。AI 補助がどんどん増えている」**

2026 年現在、Tao は自身の新しい論文の一部を最初から Lean で書き始めている。

mathlib の貢献者

- Imperial College(Kevin Buzzard のグループ)

- Brown University(Heather Macbeth)

- Carnegie Mellon(Jeremy Avigad)

- 多数の博士課程・学部生・趣味の数学者

- そして AI 補助(後の章)

最初の PR ガイド

mathlib は入口の敷居が低い。新規貢献者向けの[ガイド](https://leanprover-community.github.io/contribute/index.html)が用意されている。定理 1 つ、定義 1 つ、補助補題 1 つでも歓迎される。

4章 · Rocq(旧 Coq、2024.3 リブランド)— 25 年の古典

なぜ名前が変わったか

2024 年 3 月、Coq 開発チームは[公式スレッド](https://coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243)で **Coq を Rocq へリブランド**すると発表した。理由は 2 つに要約される。

1. 「Coq」が一部の言語で卑語に聞こえ、新規ユーザの障壁になっていた

2. 新世代のアイデンティティ — Lean にユーザが流れる中、自らを再定義する時期に来ていた

ドメインは `coq.inria.fr` 経由で [`rocq-prover.org`](https://rocq-prover.org/) に移行。コードベース自体は 25 年の歴史をそのまま継承する(Coq 1.0 は 1989 年)。

Rocq の強み

- **強固な産業検証実績** — CompCert(後述)、seL4 補助、Verdi(分散システム)、CertiCrypt、Iris ほか

- **Coq Standard Library** が極めて安定

- **Ssreflect / mathcomp** — Gonthier が四色定理や Feit-Thompson 定理(255 ページ)を証明する過程で作った戦略ライブラリ。mathlib より古い。

- **OCaml ベース** — INRIA の OCaml エコシステムと強く結びつく

短い Rocq の例

Theorem add_comm : forall a b : nat, a + b = b + a.

Proof.

intros a b.

induction a as [| a' IH].

- simpl. rewrite <- plus_n_O. reflexivity.

- simpl. rewrite IH. rewrite plus_n_Sm. reflexivity.

Qed.

`intros`、`induction`、`simpl`、`rewrite`、`reflexivity`。Lean と形は似ているが構文がより LISP 寄り(`Qed.` で閉じる)。

2026 年の Rocq 対 Lean

| 項目 | Rocq | Lean 4 |

| --- | --- | --- |

| 歴史 | 1989~ | 2013~ |

| ライブラリ | mathcomp、stdlib | mathlib(100 万 +) |

| 新規採用 | 横ばい〜減少 | 爆発的 |

| 産業 | CompCert、ProofGeneral | AWS Automated Reasoning |

| 入門難易度 | 急 | 急、ただし Lean Game あり |

Rocq が死んだわけではない — 25 年蓄積された産業コードベースはどこにも消えず、INRIA と多くの大学が今も強くサポートする。

5章 · Agda — 依存型の典型

Agda の位置

Agda はスウェーデンの Chalmers 工科大学発の**純粋な依存型関数型言語**だ。Lean と比べて「プログラミング言語としてのアイデンティティ」がより強い — すなわち全ての関数は停止性が必要(totality check)であり、型と値の区別がほぼない。

Agda の記法 — Unicode 天国

data ℕ : Set where

zero : ℕ

suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ

zero + n = n

suc m + n = suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

+-comm zero n = sym (+-identity n)

+-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (+-suc n m))

`ℕ`、`≡`、`∀`、`→` — すべて Unicode。入力は Emacs/VS Code の Agda モードが `\to`、`\equiv`、`\forall` を変換してくれる。

Agda の強み

- **型と値が完全に同一視される** — Lean よりさらに一段純粋

- **Cubical Agda** — Homotopy Type Theory の標準実装

- **PLFA**([Programming Language Foundations in Agda](https://plfa.github.io/))— この分野の最高峰の学習資料

Agda の弱み

- 大きな標準ライブラリがない(`agda/stdlib` はあるが mathlib に及ばない)

- 産業採用がほぼない

- 自動化(tactic)が非常に弱い — ほぼ手作業

2026 年に Agda を学ぶべきか

目的が**型理論の学習**、**HoTT 研究**、**プログラミング言語研究**ならイエス。産業検証や大きな数学ライブラリが目的なら Lean 4 のほうがいい。

6章 · Idris 2 — Edwin Brady の実用的依存型

Idris 2 の正体

Idris は英国 St Andrews の **Edwin Brady** が作った依存型関数型言語だ。Idris 1(2011)が Haskell 製の学術プロトタイプだったのに対し、**Idris 2**(2020 〜)は Idris 自身で書き直した self-hosting 版で、決定的に **Quantitative Type Theory**(QTT、Bob Atkey 提案)を採用した。

Idris 2 の核 — Quantitative Types

data List : (a : Type) -> Type where

Nil : List a

(::) : a -> List a -> List a

length : List a -> Nat

length [] = 0

length (_ :: xs) = 1 + length xs

-- コンパイル時のみ存在するインデックス(quantity 0)

data Vect : Nat -> Type -> Type where

Nil : Vect 0 a

(::) : a -> Vect n a -> Vect (S n) a

QTT は各引数に **0 / 1 / many** の量を割り当てる。`0` はコンパイル時のみ、`1` はちょうど一度、`many` は普通の変数。これで依存型と線形型を同時に扱う。

Idris 2 が狙う場所

Idris は「プログラミングのための依存型」をもっとも直截に狙う。Lean が数学寄り、Agda が PL 理論寄りなのに対し、Idris は**実際のソフトウェア開発**を意識している。

- 欠点: コミュニティが小さい、ライブラリが少ない

- 長所: Brady の書籍 [*Type-Driven Development with Idris*](https://www.manning.com/books/type-driven-development-with-idris) は依存型入門書の標準

7章 · Isabelle/HOL — seL4 を証明した道具

Isabelle の正体

Isabelle は英 Cambridge の Larry Paulson と独 TUM の Tobias Nipkow が 1986 年から開発してきた**古典 HOL(High-Order Logic)ベース**の証明支援系だ。Lean/Coq/Agda が**構成的論理 + 依存型**を使うのに対し、Isabelle/HOL は**古典論理 + 単純型**を使う。

Isabelle の強み — 自動化

Isabelle は自動化が圧倒的に強い。

- `auto` — 最強の汎用自動証明

- `metis` — first-order ATP バックエンド

- `sledgehammer` — **外部 SMT/ATP**(Z3、CVC4、E、Vampire など)にゴールを投げ、見つかった証明を Isabelle 内で再構成

theorem add_comm: "(a::nat) + b = b + a"

by (induct a) auto

1 行。Lean なら `simp` や `omega` を呼ぶか、もっと長く induction を書く。Isabelle は「自動化第一」の哲学だ。

Isabelle の代表的業績

- **seL4 マイクロカーネル** — NICTA(現 CSIRO Data61)と UNSW が約 20 万行の Isabelle 証明で 9,000 行の C カーネルの機能的正しさ、完全性、機密性を証明。**人が書いた OS コードの中で最も強く検証された**コード。

- **Archive of Formal Proofs(AFP)** — Isabelle 証明のキュレーションリポジトリ。2026 年現在 700+ 項目。

2026 年の Isabelle の位置

産業検証と OS セキュリティに最も深く入り込んでいる道具。mathlib のような数学ライブラリは小さいが、自動化の深さは抜きん出ている。seL4 を触るなら事実上 Isabelle が強制される。

8章 · F*(FStar、Microsoft)— HACL* 暗号検証

F\* の正体

F\*(発音「Fスター」)は Microsoft Research が作った**依存型 + SMT 自動化 + ML 系構文**の証明指向プログラミング言語だ。依存型の側面では Coq/Lean と同じ系統だが、**Z3 SMT ソルバを第一級市民**として組み込み、日常的な証明負担の多くを自動化する。

短い F\* の例

val sorted_insert: x:int -> l:list int{sorted l}

-> Tot (l':list int{sorted l' /\ Set.equal (set_of (x::l)) (set_of l')})

let rec sorted_insert x = function

| [] -> [x]

| y :: tl -> if x <= y then x :: y :: tl

else y :: sorted_insert x tl

型の中に直接仕様(`sorted l`、`Set.equal …`)を埋め込む。F\* はこれを Z3 に投げて自動で解こうとし、解けないときはユーザが補題を補強する。

HACL\* — 実際に出荷された検証済み暗号

F\* の最も有名な産業事例が **HACL\*** — Curve25519、Poly1305、ChaCha20、SHA-2、HKDF、AES-GCM など標準暗号アルゴリズムを F\* で検証し、C に抽出(extract)したライブラリだ。このコードは:

- **Firefox** の NSS ライブラリ(署名、TLS)に入る

- **Linux カーネル**の WireGuard VPN に入る

- **Windows / Azure** の一部 TLS 処理で使われる

つまりあなたが今日 HTTPS を使うとき、F\* で検証されたコードがその回線のどこかで動いている可能性が極めて高い。

EverCrypt / EverParse / Project Everest

HACL\* はさらに大きな傘である **Project Everest** の下にある。EverCrypt(マルチアルゴリズム dispatch)、EverParse(検証済みメッセージパーサ)などが一緒に束ねられている。[`project-everest.github.io`](https://project-everest.github.io/) に整理されている。

F\* 対 Lean

| 項目 | F* | Lean 4 |

| --- | --- | --- |

| 自動化 | Z3 が第一級 | tactic + SMT は別途 |

| 抽出 | C、OCaml、.NET、JS | C、IR(作業中) |

| 産業 | HACL*、Project Everest | mathlib、AWS |

| 数学ライブラリ | 小さい | 巨大(mathlib) |

9章 · Liquid Haskell — refinement types

Liquid Haskell の正体

Liquid Haskell は UCSD の **Ranjit Jhala** グループによる **Haskell 用 refinement type システム**だ。新しい言語を学ばず、普通の Haskell コードに仕様注釈を書けば SMT ソルバ(主に Z3)が検証する。

短い例

{-@ type Pos = {v:Int | v > 0} @-}

{-@ divide :: Int -> Pos -> Int @-}

divide :: Int -> Int -> Int

divide x y = x `div` y

{-@ measure size @-}

size :: [a] -> Int

size [] = 0

size (_:xs) = 1 + size xs

{-@ type NonEmpty a = {v:[a] | size v > 0} @-}

{-@ head :: NonEmpty a -> a @-}

head :: [a] -> a

head (x:_) = x

`{-@ ... @-}` の中の注釈が **refinement spec**。コンパイラは普通の Haskell だけを見るが、`liquid` ツールが SMT で仕様を検証する。

強みと弱み

- **強み**: 依存型言語を学ばずに Haskell コードを検証できる。入口の敷居が低い。

- **弱み**: Haskell の中に閉じている。一般的な定理証明には使えない。Z3 で解けない仕様には手詰まり。

「産業の検証済み Haskell」を狙うなら Liquid Haskell が現実的な最初の選択。

10章 · AI 補助 — DeepMind AlphaProof(IMO 2024 銀メダル)

AlphaProof とは

2024 年 7 月、DeepMind は **AlphaProof** と **AlphaGeometry 2** が IMO 2024(国際数学オリンピック)6 問中 4 問(28/42 点)を解き、**銀メダル相当の点数**を獲得したと発表した。4 問とも正答に到達するのに数日かかったが(人間の参加者は試験時間内に解かねばならない)、最難問の P6(組合せ論)を含む 4 問を正答したのは大事件だった。

中心構造:

1. **自然言語の IMO 問題 → Lean 4 定理**への自動翻訳(auto-formaliser)

2. **Lean 4 内で強化学習による証明探索**(AlphaProof = AlphaZero + Lean)

3. 幾何問題は **AlphaGeometry 2**(2023 年 AlphaGeometry の後継)が別途処理

DeepMind が公開した [Lean 証明そのもの](https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html)は、人間が読んでも極めて非人間的 — 100% 形式化された一行ごと。

2025〜2026 年の続き

- 2025 年 IMO でも非公式に同等の成果が報告された

- DeepMind は [AlphaProof + LLM のペア](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)作業を継続

- Lean 4 との結合がさらに深まる

意義

LLM が自然言語の解答を生成するだけの時代を超え、**形式的に検証された解答**を生成する時代に入った。正解か否かをコンパイラが即座に判定する — hallucination が原理的にブロックされる。

11章 · Anthropic + AIMO($5M 賞金)

AI Mathematical Olympiad(AIMO)

**AIMO** は XTX Markets が後援する $10M 規模の AI 数学オリンピアード・チャレンジだ。そのうち **Grand Prize $5M** は IMO 級の 50 問のうち一定精度を超えた AI モデルに贈られる。(参照: AIMO 公式サイト [aimoprize.com](https://aimoprize.com/))

2024〜2025 年に行われた Progress Prize ラウンドで NuminaMath ほか多数のオープンソースモデルが急速に進化した。2026 年現在 Grand Prize はまだ授与されていない(公開ベースで)が、差が縮まっているとの観測が多い。

Anthropic の参戦

Anthropic は 2024 年後半から、**数学的推論と Lean 形式化**を Claude モデルの明示的評価項目に含めている。Anthropic 公開報告によると:

- Claude は自然言語数学解答を生成し、Lean に形式化するときに人間介入を徐々に減らしている

- Lean InfoView を Claude がコンテキストとして受け取り、1 段ずつ tactic を提案するワークフローが mathlib コミュニティで定着しつつある(例: [Lean Copilot](https://github.com/lean-dojo/LeanCopilot))

- LLM 補助で書かれた mathlib への PR が 2025〜2026 年に増えた

LeanDojo / LeanCopilot / ntp

学界も同じ潮流。

- **LeanDojo**(CMU)— Lean 環境を LLM が扱えるようにした RL / ツール環境

- **LeanCopilot** — Lean 内で直接 LLM tactic 提案

- **ntp-toolkit** — Next-tactic prediction 標準評価

これらが融合し、「AI 補助の形式化」が mathlib 日常になった。

12章 · Terence Tao + Lean — 一流数学者の参戦

Tao が Lean を触り始めた契機

Terence Tao(UCLA、2006 年フィールズ賞)は一世代を代表する解析学者だ。2023 年から自身のブログ `terrytao.wordpress.com` で Lean 形式化の結果を定期的に共有している。

代表的な出来事:

1. **2023.11 — PFR Project** — Tim Gowers、Ben Green、Freddie Manners と共同で証明した [Polynomial Freiman-Ruzsa 予想](https://arxiv.org/abs/2311.05762)を Lean で形式化。約 3 週間で 20+ 名の協力者と完成。Tao はこれを「blueprint workflow」の模範として紹介。

2. **2024 — Magma 方程式分類プロジェクト** — 4,694 個の magma 方程式を Lean で系統的に分類。数学問題を Lean blueprint に細分化し分散協業で解決した事例。

3. **2025〜2026** — Tao は自分の新論文の一部を最初から Lean で書き始め、GitHub Copilot / Claude 補助の使用を公開。

Tao が強調する変化

Tao 自身が IAS や Joint Mathematics Meetings などの講演で強調したメッセージ:

- 「10 年前は 1 ページの証明の形式化に 1 年かかった。今は 1 週間。あと 5 年で同日に終わる」

- 「検証済みライブラリは数学者のユニットテストだ。我々が引用する結果が本当に正しいという保証」

- 「AI は形式化の最も退屈な部分を持ち去る。数学者はもっと上に上る」

Kevin Buzzard と学部教育

Imperial College London の Kevin Buzzard は学部 1 年生にブラウザベースの [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4) Lean パズルをやらせ、「**数学科の学部生は皆 Lean を学ぶべきだ**」と公言する。この流れは 2026 年には 5〜10 のトップ大学で学部正規科目として定着した。

13章 · Z3 + CVC5 — その下の SMT ソルバ

SMT solver とは

SMT(Satisfiability Modulo Theories)ソルバは「この 1 階論理式が充足可能か」を自動で判定するエンジンだ。証明支援系が「人間が 1 行ずつ書く」道具なら、SMT ソルバは「数式 1 塊を丸投げすると自動で答える」道具。

Z3

**Z3** は Microsoft Research(2007 〜、Leonardo de Moura が筆頭著者)発、最も影響力のある SMT ソルバ。無料/オープンソース(MIT)。代表事例:

- F\* / Liquid Haskell のバックエンド

- Microsoft Driver Verifier

- AWS Zelkova(S3 ポリシー検証)

- コンパイラ検証、モデルチェッカ、静的解析器の標準バックエンド

CVC5

**CVC5**(Stanford ほか、CVC4 の後継、2022 〜)は Z3 の最強ライバル。一部の領域(特に文字列、データ型)で Z3 より速い。SMT-COMP のような大会では Z3 と CVC5 が 1、2 位を競う。

短い例 — SMT-LIB

(set-logic QF_LIA)

(declare-const x Int)

(declare-const y Int)

(assert (> x 0))

(assert (> y 0))

(assert (= (+ x y) 10))

(check-sat)

(get-model)

`QF_LIA` は「quantifier-free linear integer arithmetic」。両ソルバとも同じ標準入力を受け取る。

2026 年の位置

- **F\***、**Dafny**(MS)、**Why3**(INRIA)など検証言語のバックエンド

- **Sledgehammer**(Isabelle)が外部に投げるソルバ候補の一つ

- **AWS Zelkova / Tiros** — IAM ポリシーの安全性を SMT で検証してリアルタイム警告

- **Java PathFinder、KLEE** — シンボリック実行の path constraint solver

> SMT ソルバは証明支援系のユーザがあまり意識しない「機関室」だが、ほぼ全ての自動化の裏でこの 2 つのいずれかが回っている。

14章 · 形式検証の産業事例 — seL4 / CompCert / IronFleet / KLEE

seL4 — 検証済みマイクロカーネル

2009 年に NICTA(現 CSIRO Data61)と UNSW が発表した [seL4](https://sel4.systems/) は、約 **9,000 行の C マイクロカーネル**を **20 万行以上の Isabelle/HOL 証明**で検証した史上初の本格 OS カーネルだ。証明内容:

- **機能的正しさ** — C コードが abstract spec とまったく同じ挙動を示す

- **完全性** — 権限のないアクセスが不可能

- **機密性** — 情報流制約が保たれる

このカーネルは軍用航空、衛星、一部の自動運転システムで実際に動いている。seL4 Foundation がオープンソースで維持する。

CompCert — 検証済み C コンパイラ

Xavier Leroy(INRIA、コレージュ・ド・フランス)の [CompCert](https://compcert.org/) は **Coq(現 Rocq)で書かれ検証された C コンパイラ**だ。C 標準のほぼ全部分集合を受け取り、PowerPC / ARM / x86 アセンブリにコンパイルしながら「ソース C の意味 == 出力アセンブリの意味」を Rocq で証明する。

CSmith ファジング研究が GCC/Clang で数十のコンパイラバグを発見した一方、CompCert では**一つのコンパイラバグも発見できなかった**(spec gap が一部見つかったのみ)。Airbus など航空産業で実際に使われている。

IronFleet / IronClad

Microsoft Research の [IronFleet](https://www.microsoft.com/en-us/research/project/ironclad/) は分散システム(Paxos、ロックサービス)を **Dafny**(Z3 バックエンド)で end-to-end 検証した。非ビザンチン環境で安全性・活性・線形化可能性を同時に証明した初の本格事例。

KLEE — シンボリック実行

[KLEE](https://klee-se.org/) は LLVM IR 上で動くシンボリック実行エンジン。検証とは性質が異なる(部分的経路探索)が、実コードのバグ発見に極めて効果的。coreutils、BusyBox などで多数のバグを発見した。

まとめ

| 道具 | 検証対象 | バックエンド |

| --- | --- | --- |

| seL4 | OS カーネル | Isabelle/HOL |

| CompCert | C コンパイラ | Rocq |

| IronFleet | 分散システム | Dafny + Z3 |

| HACL* / EverCrypt | 暗号ライブラリ | F* + Z3 |

| KLEE | 一般 LLVM | SMT(Z3/STP) |

| AWS Zelkova | IAM ポリシー | Z3 |

15章 · 韓国 / 日本 — KAIST、ETRI、京都大学、東京大学、AIST

韓国

- **KAIST 情報学科 PL / Verification グループ** — Software Reliability Lab(SRL、[psl.kaist.ac.kr](https://psl.kaist.ac.kr/))などで Coq/Rocq ベースの形式検証研究。Kang Jeehoon 教授グループは CompCert 拡張で知られる。

- **POSTECH**、**Seoul National University PL 研** — 関数型 / 型理論 / 検証研究が継続。

- **ETRI 形式検証グループ** — 政府課題による OS / セキュリティ検証研究。

- 学部講義に Coq/Lean を正規導入した例はまだ少ないが、2024〜2026 年に増加傾向。

日本

- **京都大学 五十嵐研 / 木下研** — PL / 型理論で日本の伝統的強豪。Coq 多用。

- **東京大学 蓮尾研 / 小林研** — 形式検証、モデル検査。

- **産業技術総合研究所(AIST)Cyber Physical Security Research Center** — Z3 / CVC5 / Isabelle 活用のセキュリティ検証。

- **国立情報学研究所(NII)** — 数理論理 / 型理論研究。

- オートマトン理論と定理証明を結ぶ ALGI のような学会の流れが生きている。

韓国語 / 日本語の資料

- 韓国語: Kang 教授の KAIST CS220 資料、一部のブログ(`hyperpolyglot`、Jaesun Kim ブログなど)。絶対量は少ない。

- 日本語: `qnighy`(Microsoft、Rust/Coq)、`mzp` など日本人 Coq/Lean ユーザのブログ。韓国より活発。

> 両国とも英語資料(mathlib zulip、Coq Discourse、FStar GitHub)で入るのが事実上の標準。

16章 · 誰が定理証明支援系を学ぶべきか

学部数学生

**Lean 4 + mathlib** が断トツの 1 番手。Imperial College のブラウザベース [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4) を 1 週間遊び、[`Mathematics in Lean`](https://leanprover-community.github.io/mathematics_in_lean/) を 1 章ずつ追えば、6 か月で自分の学部科目の定理を形式化できる。

大学院数学者 / 研究者

目的が**自分の論文の形式化 + mathlib への貢献**なら Lean。Tao を見よ。ただし自分の分野が既に Coq/Rocq や Isabelle に厚く(数論の一部、位相の一部など)あるなら、その流れに従うほうが効率的。

PL 研究者 / コンパイラ / 型システム

**Rocq(Coq)**または **Agda**。CompCert、Iris、Software Foundations の流れがここにある。HoTT / Cubical に関心があるなら Agda は必須。

セキュリティエンジニア / 暗号エンジニア

**F\***または **Isabelle/HOL**。HACL\* / EverCrypt に入りたいなら F\*。OS / マイクロカーネルセキュリティなら seL4 → Isabelle ルート。

バックエンド / 一般開発者

**Dafny**、**Liquid Haskell**、または **TLA+**(Lamport)から始める。本格定理証明支援系より入口の敷居が低く、コード / 仕様にすぐ適用できる。

「なんとなく気になる」人

[Lean Game Server](https://adam.math.hhu.de/) のゲームから始めよ。Natural Number Game、Set Theory Game、Cantor's World などがブラウザで動く。1 時間あれば最初の証明を解ける。

17章 · まとめ — 形式化はもう未来の話ではない

2026 年の風景をまとめると:

1. **Lean 4 + mathlib** が数学形式化の事実上の標準。100 万定理、一流数学者の日常の道具。

2. **Rocq(旧 Coq)**は産業検証(CompCert、seL4 補助)を強固に維持し、25 年の歴史を継ぐ。

3. **Agda / Idris 2** は型理論・PL 研究の道具として位置を保つ。

4. **Isabelle/HOL + sledgehammer** は自動化の深さで seL4 のような産業検証を可能にする。

5. **F\* + Z3 + HACL\*** はあなたが今日使う HTTPS の中にすでに入っている。

6. **DeepMind AlphaProof、Anthropic AIMO** が AI 補助形式化の時代を開いた。Lean と LLM が日常的にペアプログラミングする。

7. **seL4、CompCert、IronFleet** が「形式検証は学界の話」という言い訳を粉砕した。実システムで回っている。

10 年前に「もうすぐ形式化が標準になる」と言ったら笑われただろう。2026 年に同じことを言えば**もうそうなっている**と答えるしかない。

数学者へ: Lean 4 を始めよう。Tao がすでにやっている。

セキュリティエンジニアへ: あなたの次の暗号コードは F\* 検証を通すべきだ。

システムエンジニアへ: seL4 の上にコンポーネントを組む時代がもうすぐ来る。

好奇心ある全員へ: [Lean Game Server](https://adam.math.hhu.de/) を 1 時間遊んでみてほしい。

証明はもはや紙の上のものではない。

参考 / References

- Lean Prover 公式 — [lean-lang.org](https://lean-lang.org/)

- Lean Community — [leanprover-community.github.io](https://leanprover-community.github.io/)

- mathlib4 GitHub — [github.com/leanprover-community/mathlib4](https://github.com/leanprover-community/mathlib4)

- Mathematics in Lean — [leanprover-community.github.io/mathematics_in_lean](https://leanprover-community.github.io/mathematics_in_lean/)

- Lean Game Server(Natural Number Game ほか)— [adam.math.hhu.de](https://adam.math.hhu.de/)

- Theorem Proving in Lean 4 — [leanprover.github.io/theorem_proving_in_lean4](https://leanprover.github.io/theorem_proving_in_lean4/)

- Leonardo de Moura、Lean FRO — [lean-fro.org](https://lean-fro.org/)

- Rocq Prover(旧 Coq)— [rocq-prover.org](https://rocq-prover.org/)

- Coq → Rocq 改名発表(2024.3)— [coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243](https://coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243)

- mathcomp / Ssreflect — [math-comp.github.io](https://math-comp.github.io/)

- Software Foundations(Pierce 他、Coq/Rocq)— [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/)

- Agda 公式 — [wiki.portal.chalmers.se/agda](https://wiki.portal.chalmers.se/agda/pmwiki.php)

- PLFA(Programming Language Foundations in Agda)— [plfa.github.io](https://plfa.github.io/)

- Idris 2 — [idris-lang.org](https://www.idris-lang.org/)

- Edwin Brady、Type-Driven Development with Idris(Manning)

- Isabelle 公式 — [isabelle.in.tum.de](https://isabelle.in.tum.de/)

- Archive of Formal Proofs — [isa-afp.org](https://www.isa-afp.org/)

- F*(FStar)— [fstar-lang.org](https://www.fstar-lang.org/)

- HACL* / EverCrypt / Project Everest — [project-everest.github.io](https://project-everest.github.io/)

- Liquid Haskell — [ucsd-progsys.github.io/liquidhaskell](https://ucsd-progsys.github.io/liquidhaskell/)

- DeepMind AlphaProof IMO 2024 — [deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)

- AIMO(AI Mathematical Olympiad)— [aimoprize.com](https://aimoprize.com/)

- LeanDojo — [leandojo.org](https://leandojo.org/)

- Lean Copilot — [github.com/lean-dojo/LeanCopilot](https://github.com/lean-dojo/LeanCopilot)

- Terence Tao ブログ — [terrytao.wordpress.com](https://terrytao.wordpress.com/)

- PFR 予想(Gowers、Green、Manners、Tao 2023)— [arxiv.org/abs/2311.05762](https://arxiv.org/abs/2311.05762)

- Z3 公式 — [github.com/Z3Prover/z3](https://github.com/Z3Prover/z3)

- CVC5 公式 — [cvc5.github.io](https://cvc5.github.io/)

- SMT-LIB 標準 — [smt-lib.org](https://smt-lib.org/)

- seL4 Foundation — [sel4.systems](https://sel4.systems/)

- CompCert(Xavier Leroy、INRIA)— [compcert.org](https://compcert.org/)

- IronFleet / Ironclad(Microsoft)— [microsoft.com/en-us/research/project/ironclad](https://www.microsoft.com/en-us/research/project/ironclad/)

- Dafny 公式 — [dafny.org](https://dafny.org/)

- KLEE Symbolic Execution Engine — [klee-se.org](https://klee-se.org/)

- TLA+(Leslie Lamport)— [lamport.azurewebsites.net/tla/tla.html](https://lamport.azurewebsites.net/tla/tla.html)

- AWS Automated Reasoning — [aws.amazon.com/security/provable-security](https://aws.amazon.com/security/provable-security/)

- AWS Zelkova(IAM ポリシー検証、Z3)— Provable Security ブログ

- KAIST PSL — [psl.kaist.ac.kr](https://psl.kaist.ac.kr/)

- ETRI 形式検証グループ — [etri.re.kr](https://www.etri.re.kr/)

- 京都大学 五十嵐研究室 — [fos.kuis.kyoto-u.ac.jp](https://www.fos.kuis.kyoto-u.ac.jp/)

- AIST サイバーフィジカルセキュリティ — [aist.go.jp](https://www.aist.go.jp/)

- Kevin Buzzard、Xena project ブログ — [xenaproject.wordpress.com](https://xenaproject.wordpress.com/)

- ITP(Interactive Theorem Proving 学会)— [itp-conference.org](https://itp-conference.github.io/)

- CICM(Conferences on Intelligent Computer Mathematics)— [cicm-conference.org](https://cicm-conference.org/)