目次
2026 年 3 月、株式会社ネクストビートのテクノロジー・エバンジェリスト水島氏が、Scala 3 で定理証明支援系「sroof」を設計し、Claude CodeやCodex CLIに実装させた話を公開した。
間違った証明がコンパイルエラーになる ── Claude Code / Codex CLI で Scala 3 定理証明系 sroof を実装した
「定理証明支援系」と聞くと、数学者が使う難解なツールを想像するかもしれない。でも実は、プログラマーにとって非常に親しみやすい視点からアプローチできる。
その視点とは、**「間違った証明は型検査で弾かれる」**というものだ。
本稿はこの sroof の概要、技術的な仕組み、そして開発の背景を解説する。
型チェッカーが証明の正しさを検査する世界
sroof では、こんなコードが書ける。
// 自然数の定義
enum Nat {
case zero: Nat
case succ(n: Nat): Nat
}
// 加算の定義
def plus(n: Nat, m: Nat): Nat {
n match {
case Nat.zero => m
case Nat.succ(k) => Nat.succ(plus(k, m))
}
}
// 「n + 0 = n」という命題の証明
defspec plus_zero(n: Nat): plus(n, Nat.zero) = n {
by induction n {
case zero => trivial
case succ k ih => simplify [plus, ih]
}
}
defspecというキーワードが定理の宣言だ。plus(n, Nat.zero) = nという等式が型になっている。そして{ ... }の中身がその型を持つプログラム、つまり証明だ。
この証明が間違っていたら？型検査で弾かれる。
ここでいうカーネルとは、証明が本当に正しいかを最後にチェックする中核部分のことだ。逆に言えば、カーネルが健全で、採用している公理系に矛盾がない限り、この証明を受理した時点で、この等式は成り立つとみなせるわけだ。
「証明の正しさ」が「型検査の通過」と等しい。これが依存型を持つ定理証明支援系の核心だ。
カリーハワード同型対応（型 = 命題、値 = 証明）という考え方は、古くから知られていた。ただし「plus(n, Nat.zero) = n のような命題を、値 n に応じて変わる型としてプログラムの中に持ち込む」には、依存型が必要だ。依存型があると、等式型や全称命題を型理論の中で自然に扱えるようになる。
sroof が実装しているのは、この依存型を含むCIC（Calculus of Inductive Constructions）系の型理論だ。
なぜ Scala 3 で取り組もうと思ったか
Onion を作り始めて 20 年が経つという水島氏。Scala のコミュニティ活動については裏方なものの（Japan Scala Association）、Scala 3 の型システムの表現力にはずっと感動させられてきたという。
ある日、ふと思ったそうだ。
Scala ライクな構文を持っていて、Scala コードを extract できる定理証明支援系がないな、と。
Rocq は OCaml 製で、extraction の出力先も OCaml、Haskell、Scheme が中心だ。Lean 4 は Lean 自身で大部分が実装されており、コード生成の主なターゲットは C だ。
つまり、Scala に近い見た目で証明を書けて、そのまま Scala コードへつなげられる系は、少なくとも知る限り見当たらなかったという。
Scala 向けの既存の検証ツールも存在する。LISA は一階述語論理ベースで、Stainless は SMT ソルバーによる自動検証だ。どちらもすばらしいが、依存型の構成的型理論を中核に据えた系とはアプローチが異なる。
であれば、自分で設計して AI コーディングエージェントに実装させてみよう、と考えた。
依存型と CIC とは何か
sroof の技術的な核心はCIC（Calculus of Inductive Constructions）という型理論だ。Rocq の理論的基盤であり、Lean 4 も近縁の依存型理論を採用している。
普通の型システム（Java や Scala の List
依存型はここが違う。型が値に依存できる。
例えばVec(n: Nat)は「ちょうど n 個の要素を持つベクタ型」だ。n が 3 なら 3 要素のベクタ型、5 なら 5 要素のベクタ型という具合に、値によって型が変わる。
sroof ではPi 型（全称型）がその代表例だ。
// 型として書かれた命題：すべての自然数 n について plus(n, zero) = n
∀ n: Nat, plus(n, Nat.zero) = n
これが型だ。そしてこの型を持つ値（プログラム）が、その命題の証明になる。
型 = 命題、値 = 証明。
この対応関係がカリーハワード同型であり、CIC はこれを帰納型まで含めて体系化した型理論だ。
帰納型（Inductive Types）とは、Nat や List のようにコンストラクタの有限の組み合わせで定義される型だ。CIC では帰納型に対する帰納法の原理が導かれるため、sroof のby induction nタクティクはこの構造を利用して証明のケース分割を行う。
変数束縛と De Bruijn インデックス
sroof の AST を設計するにあたって最初の難関が「変数束縛をどう表現するか」だ。ここでよく使われるのがDe Bruijn インデックスだ。
関数型言語の処理系や定理証明系ではおなじみのテクニックだが、初見だと少し独特なので簡単に説明する。
普通の処理系では、変数名を使って束縛を管理する。でもこれは「α等価性」という問題を生む。λx.xとλy.yは意味的に同じだが、文字列としては異なる。
De Bruijn インデックスはこれをindex（位置）で解決する。
// 通常の表現 → De Bruijn
// λx.x → λ. Var(0) // 0 = 直近の束縛変数
// λx.λy.x → λ. λ. Var(1) // 1 = 1 個外の束縛変数
// λx.λy.y → λ. λ. Var(0) // 0 = 直近の束縛変数
Var(0)は「いま一番内側で束縛されている変数」だ。名前がないので、λx.xとλy.yは同じ構造になる。α等価性が消える。
sroof のコア AST（Term.scala）はこうなっている。
enum Term:
case Var(idx: Int) // De Bruijn index
case App(fn: Term, arg: Term) // 関数適用
case Lam(name: String, tpe: Term, body: Term) // λ抽象（name はデバッグ用。tpe は Scala の予約語 type を避けた命名）
case Pi(name: String, dom: Term, cod: Term) // 依存関数型
case Let(name: String, tpe: Term, def_: Term, body: Term) // let 束縛（def_は Scala の予約語 def を避けた命名）
case Uni(level: Int) // Type₀, Type₁, ...
case Ind(name: String, ...) // 帰納型
case Con(name: String, indRef: String, args: List[Term]) // コンストラクタ
case Mat(scrutinee: Term, cases: List[Case], returnTpe: Term)
case Fix(name: String, tpe: Term, body: Term) // 再帰関数
case Meta(id: Int) // メタ変数（型推論用）
NbE で型の等価性を判定する
型チェッカーの心臓部はNbE（Normalization by Evaluation）だ。
型チェック中に「この 2 つの型は等しいか？」を判定する必要がある。でもplus(zero, n)とnは構文的に全然違うのに、plus を展開すれば等しくなる。
NbE 自体はすでに古典的だが、中核となるアイデアは「一度意味の世界に上げてから、正規形に戻す」だ。
Term ──eval──▶ Semantic（意味の世界）
│
▼ 正規化は意味の世界で
Term ◀──quote── Semantic（正規形）
evalが項を Semantic ドメインの値へ評価する操作、quoteが正規形を Term に戻す操作だ。Semantic ドメインではラムダ項は Scala の関数Semantic => Semanticとして表現されるので、β簡約は関数適用そのものになる。
これにより、plus(zero, n)とnは同じ正規形になり、型の等価性が判定できる。
Scala 3 と FP ライブラリでの実装
sroof を実装していく中で、Scala 3 の機能と FP ライブラリの組み合わせが非常にマッチしていることを実感したという。特に以下の要素が活躍している。
enum による直和型は Term の AST 定義にそのまま使える。
using（contextual parameters）でグローバル環境を暗黙に渡せる。型チェッカー全体でシグネチャが非常にすっきりする。
def check(ctx: Context, term: Term, tpe: Term)(using env: GlobalEnv): Either[TypeError, Unit]
TacticMは cats の EitherT と State を組み合わせたものだ。
type TacticM[A] = EitherT[State[ProofState, *], TacticError, A]
証明状態（未解決のゴール一覧、メタ変数の割り当て）を State で持ち、タクティクの失敗を Either で扱う。flatMapでタクティクを合成できるので、haveやinductionのような複合タクティクが自然に書ける。
sroof の「哲学」── 構文という UI
定理証明支援系がプログラマーになかなか普及しない原因は何か。本質的には証明自体が難しいからというのが一般的な考えだろう。しかし、水島氏は他にも原因があると思っている。
それは見慣れない構文だ。
Rocq のコードを見てみよう。
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Theorem plus_O_n : forall n : nat, plus n O = n.
Proof.
intros n. induction n as [| n' IHn'].
- reflexivity.
- simpl. rewrite -> IHn'. reflexivity.
Qed.
Fixpoint、Theorem、Proof.、Qed.、intros、reflexivity、simpl、rewrite ->、これらはプログラマーが普段書くどの言語とも似ていない。Java でも Python でも Rust でもない、完全に独自の世界観だ。
問題はキーワードが略語かどうかではない。構文全体が見たことのない形をしていることだ。Proof. で始まり Qed. で終わる証明ブロック、. で文を区切るスタイル、これらはどのメジャー言語にも存在しない。初見で「これは何？」となるのは当然だ。
sroof は違うアプローチを取る。Scala プログラマー（あるいは通常のプログラミング言語の経験がそれなりにある人）を目標にした。
// sroof のコード。Scala 3 を知っていれば読める
enum Nat {
case zero: Nat
case succ(n: Nat): Nat
}
defspec plus_zero(n: Nat): plus(n, Nat.zero) = n {
by induction n {
case zero => trivial
case succ k ih => simplify [plus, ih]
}
}
ブレース構文、case によるパターンマッチ、enum による型定義は見慣れた形だ（少なくとも、Scala プログラマにとっては）。タクティクという概念については、プログラマにとって見慣れない形になるのは仕方がないことだが、by induction nという風に可能な限り読みやすくした。
本質的な難しさ（依存型、CIC）だけを残して、不必要な難しさ（見慣れない構文、独自の世界観）は取り除くことを目指して開発を進めている。
まとめ
現在 sroof は数百件のテストが通っており、CLI から.sroof ファイルをチェックできる。構文は Scala 3 に近い設計で、enum、given、後置 match など、Scala プログラマーが馴染みやすい形にしている。
なお、水島氏は定理証明支援系については門外漢なので、用語の使い方や理解、専門家から見た場合の誤りがあるかもしれないという。その場合、遠慮なくツッコミをいただければとのことだ。
参考：
引用元・参考リンク
免責事項 — 掲載情報は執筆時点のものです。料金・機能は変更される場合があります。最新情報は各公式サイトをご確認ください。