Lean (証明アシスタント)

Leanは およびプログラミング言語である。
を伴うに基づく。
解説.
LeanプロジェクトはGitHubでホストされている・プロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた。
Leanには(Visual Studio Code拡張機能およびサーバーとして実装された)インターフェイスがあり、他の対話型定理証明系と区別される。Unicode記号をネイティブでサポートし、「×」に対する「\times」ようなLaTeXに似たシーケンスを使用して入力できる。またLeanはJavaScriptにコンパイルしてWebブラウザからアクセスでき、メタプログラミングを広範囲にサポートする。
2017年からスタートし、ユーザーが管理するライブラリ"mathlib" には、最大規模のLeanで正規化された数学コレクションを含む。2023年2月現在、mathlibは100,000以上の定理と1,000,000行のコードを含む。
Leanの以前のリリースでは、システムロジックのいくつかのコア部分は改造されることに従順ではなかった。システムのこれらの部分を改造したいユーザーはLeanのC++実装を(直接)変更する必要があった。さらに、仮想機械の解釈に伴うオーバーヘッドは、Leanの効率がCoqなどの他の証明アシスタントと競合できないことを意味した。2021年に、Leonardo de MouraとSebastian UllrichはLean 4をリリースした: 前述の2つの批判に対処することを目的として、Lean定理証明系それ自体を自分自身の中で再実装したものである。Lean 4はコンパイルされるCのコードを生成して、効率的なドメイン固有の自動化の開発が可能になった。Lean 4はLean 3との後方互換性はない。
Leanは数学者のとの注目を集めた。ヘイルズはこれを彼のプロジェクト「Formal Abstracts」に使用している。バザードはXenaプロジェクトにそれを使用している。Xenaプロジェクトの目標の1つは、インペリアル・カレッジ・ロンドンの学部生の数学カリキュラムにあるすべての定理と証明をLeanで書き直すことである。
例 (Lean 3向け).
自然数はとして定義することができる。この定義はペアノの公理に基づいており、すべての自然数はゼロもしくは他の自然数の後者であると述べている。
inductive nat : Type
自然数の加算はパターン・マッチングを使用して、再帰的定義することも可能。
definition add : nat → nat → nat
これはLeanのtermモードでの簡単な証明である。
theorem and_swap : p ∧ q → q ∧ p :=
 assume h1 : p ∧ q,
 ⟨h1.right, h1.left⟩
これと同じ証明は戦略を駆使して達成できる。
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
begin
 assume h : (p ∧ q), -- assume p ∧ q is true
 cases h, -- extract the individual propositions from the conjunction
 split, -- split the goal conjunction into two cases: prove p and prove q separately
end