Lean (証明アシスタント)

純粋関数型言語として

プログラミング言語としての Lean は、純粋関数型言語である。この点では Haskell と似ているが、Haskell とは異なる点として以下が挙げられる。

• Lean は依存型を持つ。
• Haskell は遅延評価であるが、Lean は正格評価である。
• Lean の do 構文はより柔軟で、for / while ループや break / continue が自然に表現できる。
• Lean は Functional but in-place と呼ばれる参照カウントに基づく最適化を行う。

マクロを持つ言語として

また、プログラミング言語としての Lean は、真のマクロを持つ拡張性の高い言語でもある。この特徴は Common Lisp、Rust、Julia 等と似ているが、これらの言語とは異なる点として以下が挙げられる。

• まず Common Lisp と比較すると、Lean のマクロは衛生的 (hygienic) である。これは、マクロ処理の過程で識別子の名前が衝突しないことを意味する。
• Rust や Julia と比較すると、Lean のマクロは「言語に最初から搭載されていたかのように」ユーザ定義の構文やコマンドを追加できるという点が異なる。Rust のマクロは macro! という形でなければならず、Julia のマクロは @macro という形でなければならないが、Lean のマクロにそのような制約はない。

定理証明支援系として

Lean は定理証明支援系でもあるが、その基盤は依存型にある。依存型があるということは、カリー・ハワード同型対応によって「高階述語論理を型として表現できる」ということを意味する。これにより、Lean は数学の証明をプログラムとして表現できる。これは他の依存型に基づく定理証明支援系（Rocq や Agda や Idris）と同様である。また、逆に言えば同じく定理証明支援系である Isabelle とは Lean は理論的基盤が異なる。

「依存型に基づく定理証明支援系」の中でも、Lean は以下の特徴によって他と区別される。

• Agda や Idris とは異なり、Lean にはタクティクフレームワークが存在し、対話的な定理証明と自動証明を強力にサポートしている。
• Rocq は Lean と同様 CIC(Calculus of Inductive Constructions) をベースにしており型システムは似ているが、Lean はメタプログラミングフレームワークがより強力である他、Rocq は Lean のように汎用言語としてはデザインされていない。

プログラム検証器として

Lean はプログラミング言語でもあるため「Lean で書いたプログラムを Lean で検証する」ことが可能であり、これに命令的コードが書けることを併せると「命令的なコードを Lean で書いて Lean で検証する」ことが可能である。これは Dafny を想起させる性質だが、Dafny は de Bruijn 基準を満たしていない、つまり「独立に検査可能な証明項を生成しない」ため Lean に比べて信頼性が低いという違いがある。

2013年: 開発開始

Lean はGitHubでホストされているオープンソースプロジェクトである。2013年にMicrosoft Researchのレオナルド・デ・モウラ（英語版）によって立ち上げられた。

Lean の開発時点で Coq や Agda など他の定理証明支援系は存在していた。Lean の言語仕様はそれらから大きく逸脱したものではないが、新しい証明支援系を考案した理由として、次の2点がある。

• 証明のホワイトボックス自動化ツールを開発するためのプラットフォームを作成すること- Lean の開発者である Leonardo de Moura は、Z3 SMT ソルバの開発者でもある。Moura は標準的な SMT 実装の長所と同時に限界も認識していた。SMT ソルバは設定を自由に変更することができず、フリーサイズ(one-size-fits-all)な設計となっている。簡単な問題の場合にはこれは問題にならないのだが、問題の難しさがあるラインを超えると「ユーザには証明がわかっているのにそれをシステムに納得させられない」というストレスを生むことになった。この SMT ソルバーの限界を乗り越えるために、ホワイトボックスアプローチが必要であった。ホワイトボックスアプローチとは、ここでは証明システムを構成する要素をユーザが必要に応じて組み替えたり再構成したりできるように公開することを指す。対話的定理証明支援系(interactive theorem prover、 ITP)のタクティク言語は、ホワイトボックス化を実現する手段として位置づけられ、オーダーメイドの自動化を段階的に開発できるものとされた。これは SMT と対話的定理証明の間のギャップを埋めることを目的としていた。
• 小さな型理論とカーネル - Lean という名前には、英語で「痩せている」とか「贅肉がない」という意味がある。Lean の基礎としては標準的な依存型理論(dependent type theory)を最小限の理論に圧縮したものが採用されているが、これが Lean という名前の由来である。Lean では、タクティクを発展・洗練させる一方で、タクティクの出力を検証するシステムの実装を可能な限り単純に保つことが設計方針とされた。Lean の設計方針は、依存型理論の他の実装と比較して「より複雑な論理を、より単純なシステムで表現する」ことにあると説明されている。Lean が影響を受けかつ最も Lean に近い型理論を採用している Coq と比較すると、Lean は fixpoint 演算子や型システムに埋め込まれたモジュールシステムがないなどの違いがある。

2014年: Lean 0.1

最初のプロトタイプは Lean 0.1 (2014 年) である。Lean 0.1 では ML ライクな構文が導入され、それは後のすべての Lean のバージョンで継承されることになる。単純な simp タクティクが既にこのバージョンから存在した。帰納型のサポートはまだなく、手で公理(axiom)を追加する必要があった。Lean 0.1 では、Lua スクリプトによる構文と戦術の拡張がサポートされていたが、この部分は後の Lean 3 で削除されることになる。

2015年: Lean 2

2015 年、Lean の最初の公式リリースである Lean 2 が発表された。帰納型の適切なサポートや組み込みタクティクの拡張など、欠けていた重要な機能が追加されたほか、主要な機能として Lean 2 ではホモトピー型理論 (HoTT) のサポートが追加された。

2017年: Lean 3

最初にリリースされた比較的安定したバージョンは Lean 3 で、2017年の1月20日にリリースされた。Lean 3 では、あまり使用されていなかった Lua による構文拡張機能が削除され、根本的に異なるアプローチが採用された。Lean 自体がプログラミング言語とされ、Lean 自体によりタクティクの定義やそのほかのメタプログラミングが可能になった。Lean 2 からのもう一つの大きな変更は、ホモトピー型理論 (HoTT) のサポートの廃止である。HoTT のサポートが廃止された理由としては、

• 証明無関係(proof irrelevance) の公理がないと、タクティクを効率的に実装するのが難しくなり、コードの重複が生じるという問題
• 当時 「book HoTT」と最近の計算的な Cubical Type Theory のどちらが望ましいか不明だったという問題

が挙げられる。また、Lean で数学を形式化するライブラリである mathlib がコミュニティ管理の 独立したプロジェクトとして分離された。

バージョン3.4.2以降、Lean 3の開発は正式に終了し、Lean 4の開発が始まった。

2021年: Lean 4

2021年、Lean 4の最初のマイルストーンリリースが発表された。C++ではなく Lean 自身によって再実装され、定理証明支援系であると同時に汎用プログラミング言語でもあるという位置づけが強められた。

Lean 4 より以前のバージョンでは、次のような問題点が認識されており、Lean 4 ではそれらへの対応が行われた。

• Lean 3 での経験から、定理証明を実用的に行うためにはメタプログラミングフレームワークを備え、高い拡張性を備えていることが重要だとわかっていた。しかし Lean 3 のシステムの多くの部分が、C++ で書かれた Lean 3 のソースコードを変更しない限り、ユーザには変更できなかった。
• Lean 3 メタプログラミングは仮想マシン解釈のオーバーヘッドにより非効率だった。これにより Lean 3 での自動証明は、C++ や OCaml のような効率的なコンパイラを持つ言語で実装された同様の自動証明とは競合できなかった。

Lean 4 は完全に拡張可能であり、パーサ、エラボレータ、タクティク、決定手続き(decision procedure)、プリティプリンタ、コードジェネレータを変更・拡張することができる。また Lean 4 は対話的証明のためにカスタマイズされた衛生的なマクロ(hygienic macro)を持つ。Lean の構文をユーザが改変する際に C++ コードに触れる必要はなくなった。

さらに Lean 4 ではメモリ管理手続きが改善されたほか、テーブル解決に基づく新しい型クラス解決アルゴリズムが使用され、パフォーマンスが改善された。また、Lean 4 は functional but in-place と呼ばれる新しいプログラミングパラダイムに基づくようになった。

Lean 4 には Lean 3 との後方互換性はない。Lean3 で開発されていた主要なライブラリとして、2017年ごろから開発が行われていたmathlib が挙げられるが、コミュニティにより Lean4 への書き直しが行われた。これには100万行以上のコードを書き換える必要があったが、この移行作業は2023年7月に完了した。

2023年: Lean FRO設立

2023年7月、Lean Focused Research Organization (FRO) が設立された。形式数学の発展に向けて、証明のUI改善、スケーラビリティの改善、証明の自動化といった問題に取り組むとしている。また2023年9月、最初のLean 4 の公式リリースが発表された。

無矛盾性

非形式的な数学において一般的に基礎理論として採用されているのは ZFC 集合論と呼ばれる理論であるが、Lean で採用されている基礎理論は Calculus of Inductive Constructions (省略して CIC と呼ばれる) であって、これとは異なる。

Lean の型システムの無矛盾性については、Lean 3 の時代の結果として、「ZFC_ω が無矛盾であることと、 Lean_ω が無矛盾であることが同値であること」が知られている。ただし ZFC_ω とは、「ZFC に、任意の有限個の到達不能基数が存在するという仮定を足したもの」を指し、 Lean_ωとは「Lean 3の型システムに、任意の有限個の universe があるという仮定を足したもの」を指すものとする。 これは、ZFC の中で Lean 3 のモデルが構築でき、Lean 3 の中で ZFC が構築できるためである。

Lean 4 については、入れ子帰納型 (nested inductive type) や構造体のη変換 (η for structures) が導入されたことが型システムに大きな影響を及ぼしており、Lean 3 に対する無矛盾性の証明はそのまま適用できなくなった。

型付けの一意性

Lean では項の型は一意である。つまり、項 e の型が α であり同時に β であるとき、α と β は（どこかの型宇宙において）等しい。

なお、これは「型とは、集合のようなもの」という、型に対する素朴な理解とは矛盾することに注意が必要である。集合の場合は、${\displaystyle U\subseteq V}$ かつ ${\displaystyle x\in U}$ であるならば、${\displaystyle x\in V}$ が成り立つ。しかし、Lean では型 U の項を他の型の項であると直接見なすことはできない。

Coqとの差異

旧Coq (現在のRocq) は、Lean と同じくCalculus of Inductive Constructions (CIC) を採用しているという点で、Lean とよく似ているが、以下のような点で異なる。

• Lean では定義は宇宙多相(universe polymorphic) であることができる。つまり、一つの定義ですべての宇宙レベルを賄うことができる。しかし、Coq では定義は不定宇宙(indefinite universe)に棲んでいる。つまり、それぞれの定義は特定の宇宙に棲んでいるが、その宇宙レベルはグローバルに可変になっている。
• Coq では余帰納型(coinductive type)がサポートされているが、v4.31.0 の時点で Lean 4 は coinductive data type をサポートしていない。coinductive predicate のサポートは存在する。
• Lean では証明無関係(proof irrelevance)を definitional equality としてサポートしているが、Coq では propositional equality としてこれを主張する公理が用意されている。証明無関係は HoTT（ホモトピー型理論）の一価性公理（Univalence Axiom）と矛盾するため、特にこの事実の帰結として Lean では HoTT を素朴には実装することができない。

対話的実行

プログラミング言語としての Lean は、関数などの式を部分的に実行して評価することが容易にできるように設計されている。#eval というコマンドが存在し、関数などをその場で評価することができる。これにより、エディタ上で「コードを編集している最中に」式の評価結果のフィードバックを得ることができる。

def frac (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * frac n

-- エディタ上でコードを開いているとき
-- `#eval` の上にマウスオーバーすると 120 と表示される
#eval frac 5

なお、「エディタ上でコードを編集している間もエラボレーションが実行されてゴールが確認できる」というのは対話的な定理証明支援系にはよく見られる機能で、Agda や Isabelle、Rocq でも同様。

フィールド記法

Lean はオブジェクト指向言語ではないとされている。しかし、関数適用を「まるでフィールドにアクセスするかのように」書くことができる記法が用意されている。これは Nim 言語における Uniform Function Call Syntax に似ている。

structure Point (α : Type) : Type where
  x : α
  y : α

-- アクセサ
#check (Point.x : {α : Type} → (Point α) → α)
#check (Point.y : {α : Type} → (Point α) → α)

def origin : Point Int := { x := 0, y := 0 }

-- 通常の関数適用の書き方
#guard Point.x origin = 0

-- フィールド記法。`.x` を付けるだけで値にアクセスできる
#guard origin.x = 0

テーブル化型クラス解決(Tabled Typeclass Resolution)

型クラスは、プログラミングと定理証明の両方において、アドホック多相性 を実現する仕組みである。しかし、数学ライブラリ Mathlib の中で型クラスが広く使われるにつれ、既存の型クラス解決手続きの理論的限界が問題となった。既存の型クラス解決手続きの主要な理論的限界とは、次のようなものである：

• ダイアモンドが存在する場合、指数関数的に実行時間が伸びてしまう
• サイクルが存在する場合に発散が生じる

Lean 4 では、この２つの問題を解決する新しいアルゴリズムであるテーブル化型クラス解決が実装されている。このアルゴリズムは Prolog に対して1998年に 提案された型クラス解決アルゴリズムに基づく。

モナドとモナド変換子

Lean は Haskell の影響を受けており、モナドとモナド変換子が標準ライブラリに深く組み込まれている。

純粋関数型言語において手続き的な計算をエミュレートする方法としてはモナドの他にも代数的エフェクト・ハンドラが知られている。代数的エフェクト・ハンドラはモナドに比べると、たとえばモナドを入れ子にしたときにモナドをリフトするような操作が必要ないという利点がある。

代数的エフェクトについては Lean の開発者たちによって検討されたことがあるが、実行時またはコンパイル時のオーバーヘッドが避けられずパフォーマンス上の懸念があるという理由で採用されなかったという経緯がある。

拡張された do 記法

Lean は純粋関数型言語であるため、手続き型言語では暗黙に扱われる副作用を、モナドという再利用可能な抽象的要素で再定義することで扱っている。この再定義によって、副作用をより厳密に制御したり、派生的な副作用を導入したりすることを可能にしている。モナドは Haskell で広く用いられる抽象化機能であり、その糖衣構文である do 記法と結びついている。

Lean では、メタプログラミングフレームワークを用いて、Haskell の do 記法に由来する構文が拡張されている。具体的には以下のような記法を最初からサポートしている。

• 可変な変数を let mut で宣言できるようにする Rust ライクな記法
• 早期リターン(early return)
• for ループ、break や continue といった制御フロー

たとえば、以下は Lean 4 で実装したエラトステネスの篩である。

/-- `n`以下の素数のリストを `Array Bool` の形で返す。
`i` 番目が `true` ならば `i` は素数で、`false` ならば合成数。 -/
def eratosthenesAux (n : Nat) : Array Bool := Id.run do
  let mut isPrime := Array.replicate (n + 1) true

  isPrime := isPrime.set! 0 false
  isPrime := isPrime.set! 1 false

  for p in [2 : n + 1] do
    if not isPrime[p]! then
      continue

    if p ^ 2 > n then
      break

    -- `p` の倍数を消していく
    let mut q := p * p
    while q ≤ n do
      isPrime := isPrime.set! q false
      q := q + p

  return isPrime

/-- エラトステネスの篩 -/
def eratosthenes (n : Nat) : Array Nat :=
  eratosthenesAux n
  |>.zipIdx
  |>.filterMap fun ⟨isPrime, i⟩ =>
    if isPrime then some i else none

#guard eratosthenes 10 = #[2, 3, 5, 7]

#guard
  let actual := eratosthenes 100
  let expected := #[
    2, 3, 5, 7, 11,
    13, 17, 19, 23, 29,
    31, 37, 41, 43, 47,
    53, 59, 61, 67, 71,
    73, 79, 83, 89, 97
  ]
  expected == actual

Functional but in-place

ほとんどの関数型言語は、メモリ管理を自動で行うためにガベージ・コレクタを利用している。一方で、各値の正確な参照カウントを保持することで、破壊的更新などの最適化が可能になる。Lean は、純粋な関数型言語でありながら参照カウントを利用してメモリ管理を行う。参照カウントがちょうど１の値（つまり共有されていない値）を更新するとき、自動的に破壊的更新が行われる。すなわち、Lean は functional but in-place (FBIP) と呼ばれるプログラミングパラダイムに基づいている。特に、Lean で配列のようなデータ構造を扱うとき、FBIP によりコードの純粋性を保ちながら効率的なコードを生成することが可能である。これにより、Lean のコンパイラが生成するコードの効率化が図られている。

なお、FBIP というプログラミングパラダイムは Perceus アルゴリズムと同時に提案されたものであり、最初から Lean のためだけに開発されたものではない。

Lean が値の破壊的変更を行う例として、次のようなコードがある。

-- Lean のオブジェクトのメモリ上でのアドレスを取得する関数
-- 参照透過性を壊すため，unsafe である
#eval ptrAddrUnsafe #[1, 2, 3]

/-- フィボナッチ数列を計算する -/
def fibonacci (n : Nat) : Array Nat := Id.run do
  -- 可変な配列 `fib` を宣言している
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    -- ここで配列 `fib` のメモリアドレスを表示させている
    dbg_trace unsafe ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

-- 値がコピーされていれば異なるメモリアドレスが表示されるはずだが...?
#eval fibonacci 15

衛生的マクロとメタプログラミング

ITP（対話的定理証明支援系）において、構文を拡張可能にすることは、複雑な数学的対象の表現や、ライブラリ開発における再利用可能な抽象化に関わる。Lean 3 のものを含め、既存の ITP のマクロシステムには、構文拡張の抽象化や名前の衝突に関する課題があった。

問題点は主に以下の２点である：

• マクロの抽象化が弱く、しばしば冗長な定義をせざるをえなかった。
• タクティクを定義する際などに、マクロ展開において名前の偶発的な衝突が起こってバグを生み出していた。

Lean 4 では、Scheme ファミリーに着想を得た新しいマクロシステムが導入された。このマクロシステムは、複数のマクロ抽象化レベルを単一のシステムで扱い、表現力と名前の衝突回避を両立することを目的としている。

たとえば、以下は Coq のライブラリ math-comp における和のΣ記号の定義である。ここでは、少しずつ異なる同様の定義が 12 回繰り返されている。

Reserved Notation "\sum_ i F"
  (at level 41, F at level 41, i at level 0,
           right associativity,
           format "'[' \sum_ i '/  '  F ']'").
Reserved Notation "\sum_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \sum_ ( i  <-  r  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \sum_ ( i  <-  r ) '/  '  F ']'").
Reserved Notation "\sum_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \sum_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \sum_ ( m  <=  i  <  n ) '/  '  F ']'").
Reserved Notation "\sum_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \sum_ ( i  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\sum_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\sum_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \sum_ ( i  <  n  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \sum_ ( i  <  n ) '/  '  F ']'").
Reserved Notation "\sum_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \sum_ ( i  'in'  A  |  P ) '/  '  F ']'").
Reserved Notation "\sum_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \sum_ ( i  'in'  A ) '/  '  F ']'").

ほぼ同じことが Lean の数学ライブラリ mathlib4 では次のように表現されている。

syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?

syntax bigOpBinderParenthesized := " (" bigOpBinder ")"

syntax bigOpBinderCollection := bigOpBinderParenthesized+

syntax bigOpBinders := bigOpBinderCollection <|> (ppSpace bigOpBinder)

syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term

これは Lean では syntax および declare_syntax_cat というコマンドが用意されていることと関係がある。Lean ではユーザが構文カテゴリを定義し、パーサの拡張を抽象化された高水準言語で行うことができる。これは Lean 3 までの静的なマクロでは不可能だった。

自動証明

定理証明支援系のコミュニティにおいて、自動証明は大きな関心事である。典型的なものに SMT ソルバーを使用して証明を自動化しようとする試みがある。有名な例として、Isabelle における Sledgehammer が挙げられる。Lean にも SMT ソルバーに影響を受けた自動証明タクティクである grind が存在する。

grind には以下のような特徴がある。

• grind の中核的な動作原理は合同閉包(congruence closure)であるが、補助定理を E-マッチングを用いてインスタンス化する機能を有しておりユーザが拡張可能である。

• grind は CIC の内部で直接動作し、検証可能な証明項を生成する。Isabelle の hammer が「証明目標を外部の論理体系へ変換して SMT ソルバーを呼び出して解く」のとは対照的である。
• grind は型クラスによってパラメトライズされた補助ソルバーを持ち、適切な代数的インターフェースを実装している任意の型に対して動作する。