Lean 4 & 定理証明支援系 2026 — mathlib / Rocq (旧 Coq) / Agda / Isabelle / FStar / AlphaProof / AIMO 深掘りガイド

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

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

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

これに加え、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 と Zulip チャットは事実上 24/7 生きている。質問を投げれば 1 時間以内に誰かが返してくる。

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

mathlib とは

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

• 1,000,000+ 定理 / 補題 / 定義の合計(2026 年初に突破)
• 約 30 万行の定義、80 万行の証明
• git log で 600+ 名の貢献者
• 群・環・体・位相・測度・圏論・解析・代数幾何 — 学部から大学院まで、ほぼ全ての数学

構造と記法

import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.MeasureTheory.Integral.SetIntegral

-- 実解析: 積分の単調性
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 予想 を、約 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 は入口の敷居が低い。新規貢献者向けのガイドが用意されている。定理 1 つ、定義 1 つ、補助補題 1 つでも歓迎される。

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

なぜ名前が変わったか

2024 年 3 月、Coq 開発チームは公式スレッドで Coq を Rocq へリブランドすると発表した。理由は 2 つに要約される。

1. 「Coq」が一部の言語で卑語に聞こえ、新規ユーザの障壁になっていた
2. 新世代のアイデンティティ — Lean にユーザが流れる中、自らを再定義する時期に来ていた

ドメインは coq.inria.fr 経由で 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 が死んだわけではない — 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)— この分野の最高峰の学習資料

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 は依存型入門書の標準

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 に整理されている。

F* 対 Lean

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 証明そのものは、人間が読んでも極めて非人間的 — 100% 形式化された一行ごと。

2025〜2026 年の続き

• 2025 年 IMO でも非公式に同等の成果が報告された
• DeepMind は AlphaProof + LLM のペア作業を継続
• 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)

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

Anthropic の参戦

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

• Claude は自然言語数学解答を生成し、Lean に形式化するときに人間介入を徐々に減らしている
• Lean InfoView を Claude がコンテキストとして受け取り、1 段ずつ tactic を提案するワークフローが mathlib コミュニティで定着しつつある(例: Lean Copilot)
• 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 予想を 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 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 は、約 9,000 行の C マイクロカーネルを 20 万行以上の Isabelle/HOL 証明で検証した史上初の本格 OS カーネルだ。証明内容:

• 機能的正しさ — C コードが abstract spec とまったく同じ挙動を示す
• 完全性 — 権限のないアクセスが不可能
• 機密性 — 情報流制約が保たれる

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

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

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

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

IronFleet / IronClad

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

KLEE — シンボリック実行

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

まとめ

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

韓国

• KAIST 情報学科 PL / Verification グループ — Software Reliability Lab(SRL、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 を 1 週間遊び、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 のゲームから始めよ。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 を 1 時間遊んでみてほしい。

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

参考 / References

• Lean Prover 公式 — lean-lang.org
• Lean Community — leanprover-community.github.io
• mathlib4 GitHub — github.com/leanprover-community/mathlib4
• Mathematics in Lean — leanprover-community.github.io/mathematics_in_lean
• Lean Game Server(Natural Number Game ほか)— adam.math.hhu.de
• Theorem Proving in Lean 4 — leanprover.github.io/theorem_proving_in_lean4
• Leonardo de Moura、Lean FRO — lean-fro.org
• Rocq Prover(旧 Coq)— rocq-prover.org
• Coq → Rocq 改名発表(2024.3)— coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243
• mathcomp / Ssreflect — math-comp.github.io
• Software Foundations(Pierce 他、Coq/Rocq)— softwarefoundations.cis.upenn.edu
• Agda 公式 — wiki.portal.chalmers.se/agda
• PLFA(Programming Language Foundations in Agda)— plfa.github.io
• Idris 2 — idris-lang.org
• Edwin Brady、Type-Driven Development with Idris(Manning)
• Isabelle 公式 — isabelle.in.tum.de
• Archive of Formal Proofs — isa-afp.org
• F*(FStar)— fstar-lang.org
• HACL* / EverCrypt / Project Everest — project-everest.github.io
• Liquid Haskell — ucsd-progsys.github.io/liquidhaskell
• DeepMind AlphaProof IMO 2024 — deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level
• AIMO(AI Mathematical Olympiad)— aimoprize.com
• LeanDojo — leandojo.org
• Lean Copilot — github.com/lean-dojo/LeanCopilot
• Terence Tao ブログ — terrytao.wordpress.com
• PFR 予想(Gowers、Green、Manners、Tao 2023)— arxiv.org/abs/2311.05762
• Z3 公式 — github.com/Z3Prover/z3
• CVC5 公式 — cvc5.github.io
• SMT-LIB 標準 — smt-lib.org
• seL4 Foundation — sel4.systems
• CompCert(Xavier Leroy、INRIA)— compcert.org
• IronFleet / Ironclad(Microsoft)— microsoft.com/en-us/research/project/ironclad
• Dafny 公式 — dafny.org
• KLEE Symbolic Execution Engine — klee-se.org
• TLA+(Leslie Lamport)— lamport.azurewebsites.net/tla/tla.html
• AWS Automated Reasoning — aws.amazon.com/security/provable-security
• AWS Zelkova(IAM ポリシー検証、Z3)— Provable Security ブログ
• KAIST PSL — psl.kaist.ac.kr
• ETRI 形式検証グループ — etri.re.kr
• 京都大学 五十嵐研究室 — fos.kuis.kyoto-u.ac.jp
• AIST サイバーフィジカルセキュリティ — aist.go.jp
• Kevin Buzzard、Xena project ブログ — xenaproject.wordpress.com
• ITP(Interactive Theorem Proving 学会)— itp-conference.org
• CICM(Conferences on Intelligent Computer Mathematics)— cicm-conference.org