【翻訳】Lean定理証明機（システム記述）

はじめに

最近Leanに興味を持ち始めました。手始めに本を買ってみました。現在読んでいる途中です。

• 井上亜星 著 ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ

本格的に始める前に、概要をもう少し知りたいと思ったので、以下の論文をgeminiを使って翻訳しました。例によって、意味わかってないところが多数あるので、誤訳あると思います。気づいたら適宜直します。

• Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover. In Automated Deduction - CADE-25, 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, 2015.

※古かったので新しいこちらを訳せばよかったかも。

• Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction -- CADE 28, pages 625--635, Cham, 2021. Springer International Publishing.

---

Lean定理証明器（システム記述）

Leonardo de Moura¹、Soonho Kong²、Jeremy Avigad²、Floris van Doorn²、Jakob von Raumer²

概要

Leanは、Microsoft Researchとカーネギーメロン大学で開発されている新しいオープンソースの定理証明器であり、依存型理論に基づいた小さな信頼されたカーネルを備えている。これは、ユーザーとの対話や完全に指定された公理的証明の構築をサポートする枠組みの中に自動化ツールや手法を配置することで、対話型定理証明と自動定理証明の間の溝を埋めることを目指している。Leanは進行中かつ長期的な取り組みであるが、既に多くの有用なコンポーネント、統合開発環境、および他のシステムに組み込むために使用できる豊富なAPIを提供している。現在は、圏論、ホモトピー型理論、および抽象代数学の形式化に使用されている。本稿では、プロジェクトの目標、システムアーキテクチャ、主要な機能について述べ、アプリケーションと継続的な作業について議論する。

1 導入

形式検証には、正確な数学的用語で表現された主張を確立するための論理的および計算的手法の使用が含まれる。これには、通常の数学的定理だけでなく、ハードウェアやソフトウェアの断片、ネットワークプロトコル、機械的およびハイブリッドシステムがそれらの仕様を満たしているという主張も含まれる。実際には、数学の検証とシステムの正しさの検証の間に明確な区別はない。形式検証には、ハードウェアやソフトウェアシステムを数学的用語で記述することが必要であり、その時点でそれらの正しさに関する主張を確立することは定理証明の一形態となる。逆に、数学的定理の証明には長い計算が必要な場合があり、その場合、定理の正しさを検証するには、計算が意図した通りに行われていることを検証する必要がある。

自動定理証明は「発見」の側面に焦点を当て、しばしば健全性の保証を犠牲にしてパワーと効率を追求する。そのようなシステムにはバグがある可能性があり、通常、それらが出力する結果が正しいことを保証するものは、作者の善意以外にはほとんどない。対照的に、対話型定理証明は定理証明の 検証（verification） 側面に焦点を当て、すべての主張が適切な公理的基礎における証明によって裏付けられることを要求する。これは非常に高い基準を設定することになる。すべての推論規則と計算のすべてのステップは、基本的な公理や規則に至るまで、先行する定義や定理を引用することで正当化されなければならない。実際、そのようなシステムの多くは、他のシステムに伝達し独立してチェックできる、完全に詳細化された 証明対象（proof objects） を提供する。このような証明を構築するには通常、ユーザーからのより多くの入力と対話が必要だが、これにより、より深く複雑な証明を得ることが可能になる。

Lean定理証明器³ は、ユーザーとの対話や完全に指定された公理的証明の構築をサポートするフレームワークの中に自動化ツールと手法を配置することで、対話型と自動定理証明の間の溝を埋めることを目指している。その目標は、数学的推論と複雑なシステムに関する推論の両方をサポートし、両方の領域における主張を検証することである。LeanはApache 2.0ライセンスの下でリリースされており、他者がコードや数学ライブラリを自由に使用し拡張することを許可する寛容なオープンソースライセンスである。カーネギーメロン大学では、Leanはすでに圏論、ホモトピー型理論、抽象代数学の形式化に使用されている。Leanは進行中の長期的な取り組みであり、自動化の可能性の多くは時間の経過とともに徐々に実現されるであろう。

Leanの小さく信頼されたカーネルは、いくつかの設定オプションを持つ依存型理論に基づいている。Calculus of Inductive Constructions（CIC）[5,6]のバージョンを提供することは、非可述的なソートまたは命題である Prop を用いてインスタンス化することができるようになる。さらに、Prop は必要に応じて証明無関係（proof-irrelevant）としてマークできる。非可述的な Prop がない場合、カーネルはマーティン＝レーフ型理論[12,23]のバージョンを実装する。どちらの場合も、Leanは宇宙多相性（universe polymorphism）を伴う、非累積的型宇宙の配列（a sequence of non-cumulative type universes）を提供する。

Leanは、スタンドアロンシステムとしてもソフトウェアライブラリとしても使用されることを意図している。SMTソルバはLeanのAPIを使用して、独立してチェック可能な証明項を作成できる。APIを使用して、Leanの証明を同様の基礎に基づいた他のシステム（例：Coq[3]やMatita[1]）にエクスポートできる。また、Leanは効率的な証明チェッカーとしても使用でき、定義や定理はホストマシンの利用可能なすべてのコアを使用して並列にチェックできる。証明アシスタントとして使用される際、Leanは高階ユニフィケーション、定義上の簡約、型強制（coercion）、オーバーロード、型クラスを統合した方法で処理できる強力なエラボレーターを提供する。Leanは、Mizar[20]やIsabelle/Isar[24]に似た宣言的スタイルを用いて定義や定理を提供することを可能にする。また、Coq、HOL-Light[10]、Isabelle[17]、PVS[19]のように、（証明）項を構築するための代替的（より命令的）なアプローチとしてタクティクも提供する。さらに、宣言的スタイルとタクティクスタイルは自由に混ぜ合わせることができる。Leanには、形式的に検証された数学と基本的なデータ構造の2つのライブラリが含まれている。標準ライブラリは、非可述的で証明無関係な Prop でインスタンス化されたカーネルを使用する。このライブラリは構成的および古典的なユーザーをサポートし、命題完全性、関数外延性、強い非限定記述といった公理をオプションで使用できる。Leanには、述語的で証明に関係するカーネルのインスタンス化を使用した、ホモトピー型理論（HoTT）[23]に特化したライブラリも含まれている。HoTTをサポートするための将来の計画には、高次帰納型（HITs）やfibrant型宇宙のためのソートが含まれている。

2 カーネル

Leanの信頼されたカーネルは2つのレイヤーで実装されている。第1レイヤーには型チェッカーと、項、宣言、環境を作成・操作するためのAPIが含まれている。このレイヤーは6,000行のC++コードで構成されている。第2レイヤーは、帰納的族（さらに700行のコード）などの追加コンポーネントを提供する。カーネルがインスタンス化される際に、これらのコンポーネントのどれを使用するかを選択する。カーネルが操作するオブジェクトの数を最小限に抑えるよう努めており、そのリストは項（terms）、宇宙項（universe terms）、宣言（declarations）、環境（environments）で構成されている。識別子は、x.y.1のような文字列/数値のリストである階層名としてエンコードされる。

項（Terms）

項言語は依存λ計算である。項は、自由変数（ローカル定数とも呼ばれる）、束縛変数、定数（宇宙項によってパラメータ化される）、関数適用 $f\ t$、ラムダ抽象 $\lambda x : A; t$、関数空間 $\Pi x : A, B$、ソート $Type\ u$（$u$ は宇宙項）、メタ変数、またはマクロ $m[t_1,... t_n]$ のいずれかになる。

ソート（Sorts）

ソート Type u は、宇宙の無限の配列 $Type_0$、$Type_1$、$Type_2, \dots$ をエンコードするために使用される。明示的（explicit） 宇宙項は $s^k z$（$k \ge 0$）の形式であり、z は基底宇宙ゼロを、s は 後続（successor） 宇宙演算子を表す。それをサポートするカーネルのインスタンス化では、Type z を使用して Prop を表す。宇宙多相性をサポートするために、宇宙パラメータ（識別子）と、演算子 max u₁ u₂ および imax u₁ u₂ も備えている。宇宙項 max u₁ u₂ は u₁ と u₂ 以上であり、そのいずれかに等しい宇宙を表す。宇宙項 imax u₁ u₂ は、u₂ がゼロを表す場合は宇宙ゼロを、それ以外の場合は max u₁ u₂ を表す。演算子 imax は、非可述的な Prop を持つカーネルのインスタンス化にのみ必要である。これらのカーネルでは、A : Type u₁ と B : Type u₂ が与えられたとき、Πx : A, B の型は Type (imax u₁ u₂) となる。imax 演算子は、B が命題であるときに Πx : A, B が確実に命題になるようにする。

自由変数と束縛変数（Free and bound variables）

自由変数は一意の識別子と型を持ち、束縛変数は単なる数値（de Bruijnインデックス）である。各自由変数に型を保存することで、型チェッカーや正規化器でコンテキストを持ち運ぶ必要がなくなる。この表現は実装を大幅に簡素化し、de Bruijnインデックスの計算が必要な箇所を最小限に抑える。

メタ変数（Metavariables）

Leanでは、ユーザーは 部分的構成（partial construction）、つまりシステムによって埋められるべき「穴（holes）」を含む構成を提供できる。これらの穴（プレースホルダー（placeholders）とも呼ばれる）は、内部的にはシステムによって合成された閉じた項で置き換えられるべきメタ変数として表現される。閉じた項のみがメタ変数に割り当てられるため、コンテキスト内に現れるメタ変数はそれが依存するパラメータを記録する。たとえば、コンテキスト $(x : nat)\ (y : bool)$ における穴を $?m\ x\ y$ としてエンコードする（$?m$ は新しいメタ変数）。自由変数と同様に、すべてのメタ変数は型を持つ。また、宇宙項の「穴」を表すための宇宙メタ変数も存在する。

マクロ（Macros）

手続き的なアタッチメントとも見なせるマクロは、項を保存し操作するためのより効率的な方法を提供する。各マクロは、型推論とマクロ展開の2つの手続きを提供しなければならない。型推論手続き minfer はマクロ適用 $m[t_1,\dots, t_n]$ の型を計算する責任があり、マクロ展開手続き mexpand はマクロ適用を展開・除去しなければならない。ポイントは、$m[t_1,\dots , t_n]$ という形式の項 $t$ が与えられたとき、minfer(t) はカーネルの型チェッカーよりも効率的に mexpand(t) の型を推論できる可能性があり、また $t$ は mexpand(t) よりもコンパクトである可能性があるということである。
また、リライターや決定手続きなどの自動化ツールで使用される注釈やヒントを保存するためにもマクロを使用する。各マクロには自然数で表される 信頼レベル（trust level） がある。Leanカーネルが初期化される際、ユーザーは信頼レベル $\ell$ を提供しなければならず、カーネルは信頼レベルが $\ell$ 以上のマクロを含むいかなる項も拒否する。信頼レベル0で初期化されたカーネルはマクロを一切受け入れず、宣言に含まれるあらゆるマクロの展開を強制する。その考え方は、マクロは信頼されたコードベースの一部ではないが、システムや定理を形式化する際に、ユーザーは「ほとんどの場合」それらを信頼することを選択できるというものである。なお、Leanの独立した型チェッカーは、メタ変数やマクロのサポートを実装する必要はない。

環境（Environments）

環境は宣言のシーケンスを保存する。カーネルは現在、公理（axioms）、定義（definitions）、帰納的族（inductive families）の3種類の宣言をサポートしている。それぞれが一意の識別子を持ち、宇宙パラメータのシーケンスによってパラメータ化できる。すべての公理は型を持ち、すべての定義は型と値を持つ。
Leanにおける定数は、単に宣言への参照である。カーネルの主なタスクは、これらの宣言を型チェックし、型が正しくないものを拒否することである。カーネルは、メタ変数や自由変数を含む宣言が環境に追加されることを許可しない。環境は決して破壊的に更新されることはなく、純粋な赤黒木を使用して実装されている。

帰納的族（Inductive families）

帰納的族[8]は、型だけでなく値によってもパラメータ化できる、同時に定義された代数的データ構造の集合の一形態である。各帰納的族の定義は、[8]で記載されているように、導入規則、除去規則、および計算規則を生成する。CICと同様に、帰納的族のインスタンスは Prop に入ることができ、除去器が証明無関係性と互換性があることを保証するために特別な規則が使用される。最後に、カーネルで証明無関係性が有効になっている場合、公理 K [22]がLeanで「計算」される（同様の機能はAgda[18]でも利用可能である）。Coqとは対照的に、Leanのカーネルには不動点式、match式、または停止性チェッカーはない。代わりに、再帰的定義とパターンマッチングは、カーネルの外側で除去器へとコンパイルされる。

型チェッカー（The type checker）

コードの重複を最小限に抑えるために、型チェッカーは2つの役割を果たす。第一に、環境に追加する前にカーネルに送られたあらゆる宣言を検証するために使用される。第二に、ユーザーによって提供された項の穴を合成しようとするエラボレーション手続きによって使用される。その結果、型チェッカーはメタ変数を含む項を処理することができる。項にメタ変数が含まれている場合、型チェッカーはユニフィケーション制約を生成することがあり、その場合、結果として得られる型はユニフィケーション制約が解決できる場合にのみ正しくなる。

3 エラボレーション（Elaboration）

エラボレーターのタスクは、部分的に指定された式を、完全に指定された型的に正しい項に変換することである。項を入力する際、ユーザーはアンダースコア（つまり「穴」）を入力することで引数を暗黙のままにし、適切な値を推論することをエラボレーターに委ねることができる。関数を定義する際に引数を波括弧で囲むことで、それらを暗黙的としてマークすることもできる。これは、それらが一般的に明示的に入力されるのではなく推論されるべきであることを示す。例えば、標準ライブラリは恒等関数を次のように定義している。

definition id {A : Type} (a : A) : A := a

その結果、ユーザーは id A a ではなく id a と書くことができる。a : A が与えられたときに型 A を推論することはごく普通のことである。多くの場合、エラボレーターはΠ型の要素を推論する必要があり、これは 高階の（higher-order） 問題を構成する。たとえば、e : a = b がある型 A の2つの項の等式の証明であり、H : P が a を含むある式の証明である場合、項 subst e H は P 内の a の一部またはすべての出現を b で置き換えた結果の証明を表す。ここでは型 A だけでなく、置換のコンテキストを表す式 C : A → Prop、つまり C a が P に「簡約」されるという性質を持つ式も推論される。そのような式は曖昧になる可能性がある。たとえば、H が型 R (f a a) a を持つ場合、subst e H を用いてユーザーは R (f b b) b や R (f a b) a などの解釈を意図している可能性があり、エラボレーターは文脈とバックトラッキング探索に頼って、適合する解釈を見つけなければならない。同様の問題は帰納法による証明でも発生し、システムが帰納法述語を推論することを必要とする。エラボレーターは項の計算的解釈も尊重すべきである。それは、ベータ簡約下での項 (λx, t)s と t[s/x] の同等性や、ペアの簡約規則下での (s, t).1 と s の同等性を認識すべきである。（このような簡約の下で同等な項は、定義上等しい（definitionally equal） と言われる）。定義を展開し射影を簡約することは、代数的構造を扱う際に特に重要である。そこでは、多くの基本的な式は、そのような簡約を行わない限り型的に正しいことさえ確認できないからである。

Leanのエラボレーターはアドホック・オーバーロードもサポートしている。たとえば、自然数、整数、加法群の加法に対して同時に記法 a + b を使用できる。可能な各解釈は、エラボレーション・プロセスにおける選択ポイントになる。エラボレーターは、たとえば nat から int へ、あるいは環のクラスから加法群のクラスへの型強制（coercion）を挿入する必要性を検出することもできる。

LeanはHaskellスタイルの 型クラス（type classes） の使用もサポートしている。たとえば、関連する乗算演算子を持つ型 A のクラス has_mul A や、半群構造を持つ型 A のクラス semigroup A を次のように定義できる。

structure has_mul [class] (A : Type) :=
(mul : A → A → A)

structure semigroup [class] (A : Type) extends has_mul A :=
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))

その後、これらのクラスの適切なインスタンスを宣言し、記法 a * b や汎用的な定理 mul.assoc を処理する際にそのようなインスタンスを合成するようエラボレーターに指示できる。

最後に、定義や証明は タクティク（tactics）、すなわち様々な部分項を構築するユーザー定義または組み込みの手続きを呼び出すことができる。エラボレーターは、項の対応するコンポーネントを埋めるために、エラボレーション・プロセスの適切なタイミングでこれらの手続きを呼び出す必要がある。
これらのコンポーネント間の相互作用は微妙であり、主な困難は、エラボレーターがそれらすべてを同時に処理しなければならないことである。定義や証明は、高階ユニフィケーション、オーバーロードされた記号の曖昧さ解消、型強制の挿入、型クラス推論、および計算的簡約の混合を必要とする数千の制約を生じさせる可能性がある。これらを解決するために、エラボレーターは非時系列的バックトラッキングと慎重に調整されたアルゴリズム[7]を使用する。

再帰方程式（Recursive equations）

Leanは、再帰関数を定義し、パターンマッチングを行い、帰納的な証明を書くための自然な方法を提供する。舞台裏では、これらは帰納的族を宣言するたびにLeanによって自動的に生成される除去器と補助的な定義へと「コンパイル」される。このコンパイラは [13, 9, 21, 4] のアイデアに基づいている。デフォルトのコンパイル方法は構造的再帰、つまり引数の1つが左辺の対応する項の部分項であるような再帰適用をサポートしている。Leanは、整礎再帰を用いた再帰方程式をコンパイルすることもできる。デフォルトのコンパイル方法の主な利点は、再帰方程式が定義上成り立つことである。コンパイラは、インデックス付き帰納的型族に対する依存パターンマッチングもサポートしている。たとえば、型 A で長さ n のベクトルの型 vector A n を次のように定義できる。

inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero
| cons : Π{n : nat}, A → vector A n → vector A (succ n)

次に、型 A と B のベクトルの要素に二項関数 f を適用して、型 C の要素のベクトルを生成する関数 map を定義できる。

definition map {A B C : Type} (f : A → B → C) :
  Π{n : nat}, vector A n → vector B n → vector C n
| map nil nil := nil
| map (a::va) (b::vb) := f a b :: map va vb

入力ベクトルの長さが同じであるため、map nil (a :: va) のような「到達不能な」ケースは省略できることに注意してほしい。舞台裏では、これらの定義を帰納的族の除去器に還元するために、多くのボイラープレート・コードが必要とされる。

型クラス（Type classes）

帰納的型のいかなる族も 型クラス（type class） としてマークできる。その後、型クラスの特定の要素を インスタンス（instances） として宣言できる。これらはエラボレーターへのヒントを提供する。エラボレーターが型クラスの要素を探しているときはいつでも、宣言されたインスタンスのテーブルを参照して適切な要素を見つけることができる。型クラス推論を強力にしているのは、インスタンスを連鎖させることができること、すなわちインスタンス宣言がさらに他のインスタンスに依存できることである。これにより、クラス推論はインスタンスを通じて再帰的に連鎖し、必要に応じてバックトラッキングを行う。Leanの型クラス解決手続きは、ユーザーが宣言したインスタンスがホーン節となる、単純な λ-Prolog インタプリタ[15]と見なすことができる。
たとえば、標準ライブラリは、少なくとも1つの要素を含む型の「デフォルト」または「任意の」要素を型クラス推論が推論できるようにするために、型クラス inhabited を定義している。

inductive inhabited [class] (A : Type) : Type :=
mk : A → inhabited A

クラス inhabited A の要素は、ある要素 a : A に対して inhabited.mk a の形式になる。次の関数は対応する要素を取り出す。

definition default (A : Type) [H : inhabited A] : A :=
inhabited.rec (λa, a) H

注釈 [H : inhabited A] は、H がインスタンス宣言から型クラス解決を用いて合成されるべきであることを示す。その後、nat や Prop のような型に対して適切なインスタンスを宣言できる。次の宣言は、2つの型 A と B が inhabited であれば、それらの積も同様であることを示す。

definition prod.is_inhabited [instance] {A B : Type}
  (H1 : inhabited A) (H2 : inhabited B) : inhabited (A × B) :=
inhabited.mk (default A, default B)

宣言的証明（Declarative Proofs）

Leanは豊富な記法宣言システム[2]を備えており、MizarやIsabelle/Isarに見られるものと同様の人間が読みやすい証明をサポートするために使用されている。たとえば、have 構文は長い証明の中に補助的なサブゴールを導入する。内部的には、記法 have H : p, from s, t は項 (λ (H : p), t) s を生成する。同様に、show p, from t は t に期待される型 p を注釈する以上のことはしない。Leanはまた、ラムダ抽象のためのMizar/Isarに触発された代替構文 assume H : p, t および take x : A, t も提供する。キーワード calc で始まる計算証明は、等号の推移律のような基本的な原理によって構成されることが意図されている中間結果を連鎖させるための便利な記法である。計算証明でサポートされる二項関係述語のセットは、ユーザーによって自由に拡張できる。以下の例においては、これら特徴のいくつかを実証している。

theorem le.antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b :=
take a b : ℤ, assume (H₁ : a ≤ b) (H₂ : b ≤ a),
obtain (n : ℕ) (Hn : a + n = b), from le.elim H₁,
obtain (m : ℕ) (Hm : b + m = a), from le.elim H₂,
have H₃ : a + of_nat (n + m) = a + 0, from
... --紙面の都合により、証明は省略
have H6 : n = 0, from nat.eq_zero_of_add_eq_zero_right H₅,
show a = b, from
  calc
    a = a + 0      : add_zero
    ...   = a + n  : H₆
    ...   = b      : Hn

名前空間（Namespaces）

Leanは、定義や、記法宣言、型強制、書き換え規則、型クラスなどのメタオブジェクトを、入れ子になった階層的な 名前空間（namespaces） にグループ化する機能を提供する。open コマンドは、短い名前とすべてのメタオブジェクトを現在のコンテキストに取り込む。

タクティク・フレームワーク（The tactic framework）

タクティクは項を構築するための代替アプローチを提供する。項を構成や数学的証明の表現と見なすことができ、タクティクはそのような項をどのように構築するかを記述するコマンド、または指示である。Leanで利用可能な自動化のほとんどは、タクティクとしてシステムに統合されている。たとえば、Leanには書き換えを行うための基本的なメカニズムを提供する rewrite タクティクが含まれている。タクティク・フレームワークは、メタ変数を合成するための一般的なメカニズムを提供する。このフレームワークでは、メタ変数は ゴール（goal） であると言う。 証明状態（proof state） には、ゴールのシーケンス、延期されたユニフィケーション制約、および既に割り当てられたメタ変数を保存する代入が含まれる。 タクティク（tactic） は、証明状態を証明状態のストリームへとマップする関数であり、遅延リスト[16]として実装されている。これは、一部のタクティクが無制限の証明状態のストリームを生成する可能性があるため重要である。Leanは、他の対話型定理証明器で利用可能な andthen、orelse、try といったすべての通常のコンビネータ（ タクティカル（tacticals） とも呼ばれる）を提供する。また、複数のコアでタクティクを並列実行するための par や、タクティク T が n ミリ秒以内に終了しない場合に失敗する tryfor T n といったタクティカルも提供する。Leanには apply、intro、generalize、rewrite などの基本的なタクティクも備わっている。タクティクの完全なリストは[2]に記載されている。項が期待される場所であればどこでも、Leanは代わりにカンマで区切られたタクティクのシーケンスで構成される begin ... end ブロックを挿入することを許可する。以下はタクティクを用いた短い例である。

theorem test (p q : Prop) : p → q → p ∧ q ∧ p :=
begin
  intro Hp, intro Hq,
  apply and.intro, exact Hp, apply and.intro,
  exact Hq, exact Hp
end

4 ユーザーインターフェース

Leanの標準的な統合開発環境（IDE）[11]はEmacsエディタに基づいており、継続的なエラボレーションとチェックを提供する。バックグラウンドでは、ユーザーによって編集されているソーステキストが継続的に分析され、意味情報が付加される。エディタと証明器の間の対話は、並列性、マルチコアハードウェア、およびインクリメンタルコンパイルを活用する非同期プロトコルによって行われる。ネイティブインターフェースは、ハイパーリンク、オートコンプリート、構文ハイライト、エラーハイライトなど、高度なIDEに見られるすべての標準機能を提供する。ユーザーは、自動的に合成された項、暗黙の型強制、およびオーバーロード解決を表示できる。ユーザーが依存チェーンのより上位にあるファイルを変更した場合、すべてがバックグラウンドで再コンパイルされ、キャッシュによって変更はほぼ即座に伝播される。
LeanのJavascriptバインディングにはネイティブコードが含まれておらず、現代的なウェブブラウザであればどれでも使用できる。これらは、ウェブIDE⁴、 「ライブ」なチュートリアル/ドキュメント⁵、オンライン演習などのウェブアプリケーションを意図している。このインフラを用いて、CMUに2015年の春に行われた対話的定理証明コース⁶の教材を開発した。

5 結論

Leanは、以下のすべての機能を備えた定理証明システムを得ることを目標に設計された。数学的仕様と証明を書くための表現力豊かな論理的基礎、対話的で支援的なユーザーインターフェースと環境、自動化をサポートするための柔軟なフレームワーク、そしてこの機能を他のシステムに組み込むために使用できる豊富なAPIである。Leanは、高階ユニフィケーション、定義上の簡約、型強制、オーバーロード、および型クラスを統合的な方法で処理できる斬新なエラボレーション手続きをすでに提供している。比較的小さな信頼されたカーネルを持っており、Leanのためのリファレンス/独立した型チェッカーを実装するタスクをはるかにシンプルにしている。また、マルチコアマシンのサポートと粗い粒度および細かい粒度の並列処理により、非常に高速である。Leanは進行中の長期的な取り組みであり、将来の計画には広範な探索手続き、決定手続き、ホモトピー型理論のより良いサポート、および独立した型チェッカーが含まれている。

参考文献

1. A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. The Matita Interactive
   Theorem Prover. In Automated Deduction – CADE-23, pages 64–69. Springer Berlin Heidelberg, 2011.
2. J. Avigad, L. de Moura, and S. Kong. Theorem Proving in Lean. http: //leanprover.github.io/tutorial/tutorial.pdf, 2015.
3. B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Gimenez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, et al. The Coq proof assistant reference manual: Version 6.1. 1997.
4. J. Cockx, D. Devriese, and F. Piessens. Pattern matching without K. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pages 257–268. ACM, 2014.
5. T. Coquand and G. Huet. The calculus of constructions. Inform. and Comput., 76(2-3):95–120, 1988.
6. T. Coquand and C. Paulin. Inductively defined types. In COLOG-88 (Tallinn, 1988), pages 50–66. Springer, Berlin, 1990.
7. L. de Moura, J. Avigad, S. Kong, and C. Roux. Elaboration in dependent type theory. In preparation.
8. P. Dybjer. Inductive families. Formal aspects of computing, 6(4):440–465, 1994.
9. H. Goguen, C. McBride, and J. McKinna. Eliminating dependent pattern matching. In Algebra, Meaning, and Computation, pages 521–540. Springer, 2006.
10. J. Harrison. HOL light: An overview. In Theorem Proving in Higher Order Logics, pages 60–66. Springer, 2009.
11. S. Kong and L. de Moura. User Interaction in the Lean Theorem Prover. In preparation.
12. P. Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984.
13. C. McBride, H. Goguen, and J. McKinna. A few constructions on constructors. In Types for Proofs and Programs, pages 186–200. Springer, 2006.
14. C. McBride and J. McKinna. Functional pearl: I am not a number–I am a free variable. In Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell ’04, pages 1–9, New York, NY, USA, 2004. ACM.
15. D. Miller and G. Nadathur. Programming with Higher-Order Logic. Cambridge, 2012.
16. T. Nipkow and L. C. Paulson. Isabelle-91. In Automated Deduction - CADE-11, pages 673–676, 1992.
17. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002.
18. U. Norell. Dependently typed programming in Agda. In Advanced Functional Programming, pages 230–266. Springer, 2009.
19. S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. Automated Deduction—CADE-11, pages 748–752, 1992.
20. P. Rudnicki. An overview of the Mizar project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 311–330, 1992.
21. K. Slind. Function definition in higher-order logic. In Theorem Proving in Higher Order Logics, pages 381–397. Springer, 1996.
22. T. Streicher. Investigations Into Intensional Type Theory. PhD thesis, LMU, 1993.
23. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.
24. M. M. Wenzel. Isabelle/Isar - a versatile environment for human-readable formal proof documents, 2002.

1. Microsoft Research ↩

2. Carnegie Mellon University ↩ ↩² ↩³ ↩⁴

3. http://leanprover.github.io ↩

4. http://leanprover.github.io/live ↩

5. http://leanprover.github.io/tutorial ↩

6. http://www.cs.cmu.edu/~emc/15815-s15 ↩