証明支援系
証明支援系 (proof assistant / ITP) は数学的言明を厳密に検証する対話的定理証明器。Curry-Howard 対応により命題＝型、証明＝関数の定義として証明を構築する。依存型や高階述語論理を基盤とし、ソフトウェア正当性証明や数学の形式化に使われる（形式手法の証明系側）。
主要システム
- Coq: SSReflect/MathComp で解析学の形式化など。tactic ベース。
- Agda: 依存型を持つ Haskell 風言語。命題を型、証明を関数定義として書く。
- Lean (Lean 4): 内部言語は依存型λ計算の Calculus of Constructions。データ型・値・命題・証明がすべて同一の項。強力なメタプログラミングを持つ。
- Isabelle/HOL、Idris（依存型・正格評価の Haskell 風言語）。
自動化と等式飽和
- 等式的推論の冗長さを軽減するため等式飽和を統合する動き。Lean の
lean-eggタクティクはeggをバックエンドにし、定義上の等価性 (β/η/δ 変換) と束縛変数 (De Bruijn) の不一致を lowering/reconstruction で橋渡しする。最終証明は Lean カーネルが検証するため健全性が保たれる。 - これが束縛変数を第一級に扱う slotted e-graph (PLDI 2025) を生み、Terence Tao 主導の Equational Theories Project を支えた。
関連
- 型の背景はtype-theory-lambda-cube、自動化技術はequality-saturation。
- Lean 学習例はlean-natural-number-game。
- _moc-prog-lang