Lean の仕組み — 来歴と、検証が働く仕組み

この考えは、離れた場所から来た二本の筋が合流したものです。

一本目は、証明を機械で扱える対象として書けること。関数に型を付ける仕組みと、含意「A ならば B」を証明する仕組みが同じ形をしている——この対応は Curry–Howard 対応と呼ばれます。名前の一方は、1934 年の Curry の論文「組み合わせ論理における関数性」に由来します。この対応があると、証明は読んで納得するものではなく、型の合った項という具体的な書き物になります。

二本目は、確かめる側は小さいほうがよいこと。1972 年、Milner は Stanford で LCF という証明検査系を実装しました。LCF の系統では、証明を組み立てる道具（tactic）はメタ言語で自由に書ける一方、出来上がったものを認めるかどうかは小さな中核だけが決めます。道具がいくら増えても、信頼しなければならない部分は増えません。

この二本を最初に本格的に合流させたのが、de Bruijn の Automath です。数学の証明を書き下し、機械に検査させるための言語として設計され、1970 年に報告されました。数学の証明を機械検査にかけるための、最初の全面的な試みです。1970 年代には、Jutting が Landau の『解析学の基礎』をこの言語で検査しています。

ここから出てきた設計方針が、のちに de Bruijn の基準と呼ばれるものです。証明を「検査の途中経過」としてではなく、それ自体で完結した項として残し、小さな独立の検査器で読み直せるようにする。証明支援系を比較する古典的な一覧表では、これが「小さな証明核（証明対象を持つこと）」という一項目として立てられています。Lean の公式文書も同じことを述べています——「証明項は定理の真理性の十分な証拠であり、独立した検証にかけられる」。

型理論の側では、Martin-Löf の直観主義型理論（1975 年）が数学の基礎を型の上に置き直そうとし、それを踏まえて Coquand が 1985 年に Calculus of Constructions の最初の版を出しました。最初の実装は 1984 年に Huet と Coquand が始めたもので、その中核は Constructive Engine と呼ばれる型検査器でした。1989 年に Coquand と Paulin が帰納的定義を加え、Calculus of Inductive Constructions になります。これが Coq の論理であり、そして Lean の論理の土台でもあります。

この系統で実際に検査された大きな定理を、年表に混ぜて並べます。

Lean はこの表の続きに位置します。土台の型理論は Coq と同系統で、設計方針は LCF 系統の「小さな中核」を引き継いでいます。

Lean は 2013 年、Microsoft Research の de Moura が始めました。最初のコミットは同年 7 月です。以後、記法と実装は何度も入れ替わりました。

最初の公開版は 0.1（2014 年）です。版 0.2 は標準の論理に加えてホモトピー型理論のモードを持っており、Lean 2 という名の別リポジトリに凍結されています。Lean 3（2017 年 1 月）で利用者が増え、同年 7 月に数学ライブラリ mathlib が作られます。2018 年 4 月に Lean 4 の開発が始まり、2023 年 9 月に正式版が出ました。

Lean 4 の特徴のひとつは、Lean 自身で書き直されていることです。parser も elaborator も tactic も Lean で書かれており、利用者がそれらを Lean のまま拡張できます。前の版で C++ を書かないと足せなかった部分が、ライブラリと同じ言語で書けるようになりました。

mathlib のほうは、個人の作業ではなく共同体の作業として育ちました。設計の記録は 2019 年の論文にまとめられており、いまでは 100 万行を超える規模になっています。Lean 3 から Lean 4 への移植は 2023 年 7 月に完了しました。

同じ 2023 年 7 月、Lean の開発体制そのものが変わります。de Moura と Ullrich が Lean FRO（Focused Research Organization）を設立し、Lean は非営利組織の下で開発される道具になりました。

Lean を使った形式化で、規模の目印になるものを二つ挙げます。Liquid Tensor Experiment は、2020 年 12 月に「この定理を形式化できるか」という挑戦として出され、第一目標の証明が 2021 年 5 月 28 日に予告され、2022 年 7 月 14 日に全体が完了しました。多項式 Freiman–Ruzsa 予想のほうは、証明の論文が 2023 年 11 月に出た直後に形式化のプロジェクトが立ち上がり、第一段階は完了しています。

利用者が書いた文字列が定理として認められるまでに、Lean は次の段を通ります。

ここで効いているのは、核となる型理論が、利用者が書く言語よりずっと単純であることです。公式文書の言い方では、「この核の理論はずっと単純であり、それによって信頼される kernel を非常に小さく保てる」。elaborator がどれだけ賢くなっても、kernel が読むのは単純な言語のままです。

compiler は検証の列に入っていません。実行できるプログラムを作るための別系統で、定理が正しいかどうかには関わりません。例外は native_decide で、そのときだけ compiler の出した結果が公理として論理の側に入ります（01）。

核の型理論のほうも、名前だけ押さえておきます。

最後にひとつ、区別を。mathlib は kernel の一部ではありません。ライブラリ——つまり Lean で書かれた定義と定理の集まりであって、立場としては利用者が書くファイルと同じです。mathlib に誤った証明が混ざったとしても、それが kernel を通っていることに変わりはなく、逆に mathlib を全部外しても kernel は同じように働きます。

ここがこのページの中心です。Lean を触ったことがなくても追えるように、たとえ話から始めて、実物を一歩ずつ見ていきます。

窓口のたとえ

証明を記入済みの書類だと思ってください。命題は書類の様式で、証明はその様式を埋めた一枚です。

kernel は記入の規則だけを知っている窓口です。窓口は、書類が誰の手で書かれたか、手書きか印字か、下書きを何枚捨てたかを見ません。見るのは、様式の欄が規則どおりに埋まっているかだけ。埋まっていれば受け取り、埋まっていなければ突き返します。

この「見ないこと」が要点です。証明を組み立てる道具（tactic）も、探索のプログラムも、人の勘も、窓口の外側にあります。窓口が見るのは、最後に提出された一枚だけです。

一歩目 — 計算で閉じる

いちばん小さい書類を見ます。

theorem two_add_two : 2 + 2 = 4 := rfl

: の後が様式（命題）、:= の後が記入（証明）です。rfl は「両辺を計算すると同じものになる」という一語の記入で、これを受け取った kernel は、実際に両辺を計算します。

計算の規則は、自然数の加法の定義そのものです。Lean にはこう入っています。

#check @Nat.add_zero
#check @Nat.add_succ

Nat.add_zero : ∀ (n : ℕ), n + 0 = n
Nat.add_succ : ∀ (n m : ℕ), n + m.succ = (n + m).succ

「何かに 0 を足すとそれ自身」と「何かに『次の数』を足すと、足した結果の次の数」。この二本しかありません。succ は「次の数」を作る操作で、2 + 2 の右の 2 は 0 の次の次です。だから kernel の手は三手で済みます。

example : 2 + 2 = Nat.succ (2 + 1) := rfl
example : 2 + 1 = Nat.succ (2 + 0) := rfl
example : 2 + 0 = 2 := rfl
example : Nat.succ (Nat.succ 2) = 4 := rfl

四行とも検査を通ります。一行目と二行目が Nat.add_succ、三行目が Nat.add_zero、四行目は「4 という書き方が 2 の次の次を指している」ことです。この四つをつなげると 2 + 2 から 4 に着きます。最初の定理で kernel がしているのは、これと同じことです。

二歩目 — 「かつ」の証明は組

計算で閉じない命題も、同じ枠に収まります。「A かつ B」の様式を見ます。

#check @And.intro

@And.intro : ∀ {a b : Prop}, a → b → a ∧ b

読み方は「命題 a と b について、a の証明と b の証明を受け取ると、a ∧ b の証明になる」。つまり a ∧ b の証明とは、a の証明と b の証明の組です。

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

(hp : p) は「p の証明を hp という名前で受け取る」という宣言、⟨ ⟩ は組を作る記法です。片方に間違ったものを入れると、窓口は理由を添えて突き返します。

example (p q : Prop) (hp : p) : p ∧ q := ⟨hp, hp⟩

error: Application type mismatch: The last
  hp
argument has type
  p
but is expected to have type
  q
in the application
  ⟨hp, hp⟩

「二つ目の欄には q の証明が来るはずなのに、p の証明が入っている」。書類の不備の指摘です。rfl の側でも同じです。

example : 2 + 2 = 5 := rfl

error: Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

この二つの指摘を出しているのは、正確には kernel ではなく elaborator です。elaborator は項を組み立てながら自分でも型を見ているので、不備はたいてい kernel に届く前に見つかります。kernel は同じ規則で、出来上がった項をもう一度通す最後の関門です。

三歩目 — 「ならば」の証明は関数

「A ならば B」の記入は、A の証明を受け取って B の証明を返す関数です。

example (p : Prop) : p → p := fun hp => hp

example (p q : Prop) (h : p → q) (hp : p) : q := h hp

一行目は「p ならば p」——受け取ったものをそのまま返す関数です。二行目は「p ならば q」の証明 h と p の証明 hp があれば q の証明が得られる、を h hp（関数に引数を当てる）と書いています。論理の一歩が、関数の呼び出しと同じ形をしている。これが Curry–Howard 対応の手触りです。

四歩目 — tactic で書いても、最後は項になる

実際の証明は、こんなに短くは書けません。そこで by の後に tactic を並べ、項を代わりに組み立ててもらいます。

theorem and_swap (p q : Prop) (h : p ∧ q) : q ∧ p := by
  constructor
  · exact h.2
  · exact h.1

constructor は「q ∧ p を作るには q と p が要る」と目標を二つに割る tactic、exact はその欄に手持ちのものを入れる tactic です。組み立てた結果は #print で見えます。

#print and_swap

theorem and_swap : ∀ (p q : Prop), p ∧ q → q ∧ p :=
fun p q h => ⟨h.right, h.left⟩

四行の tactic が消えて、一行の項が残りました。しかも中身は、二歩目と三歩目で見た形そのものです——引数を受け取る関数（fun）と、二つの証明の組（⟨ ⟩）。tactic はこの項を書くための道具であって、kernel が受け取るのはこの一行だけです。

なぜ信じられるのか

ここまでを踏まえると、信じなければならないものと、信じなくてよいものが分かれます。

それでも「kernel の実装」は残ります。そこで、出来上がった証明を読み直す手立てが用意されています。Lean の公式文書は、確かめ方を強さの順に並べています。

三つ目の leanchecker は Lean の kernel をもう一度走らせる道具なので、kernel 自体の不具合は捕まえられません。捕まえるのは、kernel の状態を扱う周辺の不具合や、メタプログラムが検査を迂回して宣言を足す類のことです。

四つ目が、いま用意されているいちばん強い形です。証明を隔離した環境で組み立て、証明項を書き出し、その外側で——つまり証明の側のプログラムが手を出せない場所で——Lean の kernel と、独立に書かれた別の検査器の両方に通します。公式文書が名を挙げている外部検査器は Rust で独立に実装されたもので、ほかにも検査器を並べて比べる場が作られています。これが、de Bruijn の基準が実際に払っている配当です。証明が項として残っているから、別の検査器で読み直せる。

それでも前提は残ります。公式文書はそれも列挙しています——Lean の論理そのものが健全であること、書き出しと照合の配管が正しいこと、隔離環境が破られないこと、用いたすべての検査器に同時に効く不具合が無いこと、そして言明に人の誤りや誤解を招く書き方が無いこと。

それでも間違えうる所

誰が何を保証するか

機械検査が動かしたのは、確かめる対象と確かめる手段の境目です。「証明が正しいか」は機械に渡せる。「その定理が言いたかったことか」は渡せない。後者が残ることは弱点ではなく、前者が片付いたおかげで前面に出てきた仕事です。

文献・出典

Lean の初歩は 01 Lean とは何か、手元で動かすところは 02 使い方の入口、語の意味は 12 用語集。