LabHub

ブログ

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

2026-05-16 · 35 分で読めます · #lean-4#lean#mathlib#rocq#coq#agda#idris-2#isabelle-hol#fstar#liquid-haskell#ats#theorem-prover#proof-assistant#formal-methods#alphaproof#aimo#terence-tao#z3#cvc5#sel4#compcert#deep-dive#japanese

한국어English日本語

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

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

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

陣営核心作者色合い
Lean 4mathlib(100 万定理超)Leonardo de Moura(AWS)数学中心、爆発的成長
Rocq(旧 Coq)25 年史、CompCertINRIA(フランス)古典、産業検証
Agda依存型の典型Chalmers(スウェーデン)学術 / 型理論
Idris 2プログラミング志向Edwin Brady実用的依存型
Isabelle/HOLseL4 を証明Cambridge / TUM古典 HOL、自動化が強い
F(FStar)*HACL* 暗号検証Microsoft Research実用 + Z3
Liquid Haskellrefinement typesUCSDHaskell 上の 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 が速い理由

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

# 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 Community サイト leanprover-community.github.io と Zulip チャットは事実上 24/7 生きている。質問を投げれば 1 時間以内に誰かが返してくる。

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

mathlib とは

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

構造と記法

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 の貢献者

最初の 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 の強み

短い 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

項目RocqLean 4
歴史1989~2013~
ライブラリmathcomp、stdlibmathlib(100 万 +)
新規採用横ばい〜減少爆発的
産業CompCert、ProofGeneralAWS 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 の強み

Agda の弱み

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 は実際のソフトウェア開発を意識している。

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

Isabelle の正体

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

Isabelle の強み — 自動化

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

theorem add_comm: "(a::nat) + b = b + a"
  by (induct a) auto

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

Isabelle の代表的業績

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)したライブラリだ。このコードは:

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

EverCrypt / EverParse / Project Everest

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

F* 対 Lean

項目F*Lean 4
自動化Z3 が第一級tactic + SMT は別途
抽出C、OCaml、.NET、JSC、IR(作業中)
産業HACL*、Project Everestmathlib、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」を狙うなら 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 年の続き

意義

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 公開報告によると:

LeanDojo / LeanCopilot / ntp

学界も同じ潮流。

これらが融合し、「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 などの講演で強調したメッセージ:

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)。代表事例:

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 年の位置

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

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

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

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

このカーネルは軍用航空、衛星、一部の自動運転システムで実際に動いている。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 などで多数のバグを発見した。

まとめ

道具検証対象バックエンド
seL4OS カーネルIsabelle/HOL
CompCertC コンパイラRocq
IronFleet分散システムDafny + Z3
HACL* / EverCrypt暗号ライブラリF* + Z3
KLEE一般 LLVMSMT(Z3/STP)
AWS ZelkovaIAM ポリシーZ3

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

韓国

日本

韓国語 / 日本語の資料

両国とも英語資料(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

コメント

まだコメントはありません。

ログインするとコメントできます