Lean (証明アシスタント)
Lean は純粋関数型プログラミング言語のひとつである。また、同時に証明支援系(theorem prover)でもある。帰納型を伴うCalculus of constructionsと呼ばれる型システムに基づいている。
 Leanのロゴ | |
| パラダイム | 関数型プログラミング |
|---|---|
| 登場時期 | 2013年 |
| 開発者 |
Leonardo de Moura LeanFRO |
| 最新リリース | v4.7.0/ 2024年4月3日 |
| 型付け | 推論される, 強い, 静的 |
| 影響を受けた言語 |
ML Coq Haskell |
| プラットフォーム | クロスプラットフォーム |
| ライセンス | Apache License 2.0 |
| ウェブサイト |
lean-lang |
歴史 編集
Lean はGitHubでホストされているオープンソースプロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた[1]。Lean 2 では Homotopy Type Theory (HoTT) をサポートしていた。[2] しかし後の Lean 3 以降ではHoTT のサポートは Lean 言語の標準ライブラリから削除された。[3]
最初にリリースされた比較的安定したバージョンは Lean 3 で、2017年の1月20日にリリースされた。[4]一部の機能は Lean 自身で実装されていたが、主に C++ で実装されていた。バージョン3.4.2以降、Lean 3の開発は正式に終了し、Lean 4の開発が始まった。
2021年、Lean 4の最初のマイルストーンリリースが発表された。[5]C++ではなく Lean 自身によって再実装され、「Lean は定理証明支援系であると同時に、汎用プログラミング言語でもある」と標榜するようになった。Lean 3 は全体的に書き換えられ、型クラスのインスタンス検索やメモリ管理手続きなどが改善された。また、Lean 自身によって再実装されたため、Lean の構文をユーザが改変する際に C++ コードに触れる必要がなくなったものも Lean 4 の利点である。
Lean 4 には Lean 3 との後方互換性はない。Lean3 で開発されていた主要なライブラリとして、2017年ごろから開発が行われていた[6]mathlib が挙げられるが、コミュニティにより Lean4 への書き直しが行われた。これには100万行以上のコードを書き換える必要があったが、この移行作業は2023年7月に完了した。[7]
2023年7月、Lean Focused Research Organization (FRO) が設立された。[8]形式数学革命のために、証明のUI改善、スケーラビリティの改善、証明の自動化といった問題に取り組むとしている。また2023年9月、最初のLean 4 の公式リリースが発表された。[9]
利用 編集
- Kevin Buzzard は、数学者や数学科の学部生の間で Lean のような定理証明支援系を普及させることを目指す Xena プロジェクトを主導している。[10]Xena プロジェクトの目標の1つは、インペリアル・カレッジ・ロンドンの学部生の数学カリキュラムにあるすべての定理と証明をLeanで書き直すことである。
- 2020年12月、数学者の Peter Scholze は自身の liquid vector space に関する定理を Lean で形式化することは可能かという挑戦状を Lean コミュニティに持ち込んだ。この挑戦は Liquid Tensor Experiment と呼ばれ、2022年7月に完了が宣言された。[11]
- フィールズ賞受賞者の Terence Tao は、2023年10月のSNSへの投稿で、自身の論文を Lean 4 で形式化する過程で小さな（しかし非自明な）ミスを見つけることができたと明かしている。[12]
Lean の言語仕様と機能の概要 編集
正格評価 編集
同じく純粋関数型言語である Haskell とは異なり、Lean は正格評価である。つまり、関数を評価する前に関数に渡された引数をすべて評価する。
/-- 条件 `cond` が true なら最初の引数を，
false なら2番目の引数を返す関数 -/
def selectFst (cond : Bool) (fst snd : Nat) :=
if cond then
fst
else
snd
/-- 与えられた自然数をそのまま返す関数.
実行されると infoview に表示が出る. -/
def trace (n : Nat) : Nat :=
dbg_trace "trace is called"
n
/-
trace is called
10
-/
#eval selectFst true 10 (trace 20)
帰納型 編集
自然数は帰納型として定義することができる。この定義はペアノの公理に基づいており、すべての自然数はゼロもしくは他の自然数の後者であると述べている。
inductive Nat : Type where
| zero : Nat
| succ : Nat → Nat
自然数の加算はパターン・マッチングを使用して、再帰的に定義できる。
def Nat.add (n m : Nat) : Nat :=
match n with
| zero => m
| succ n => succ (add n m)
対話的実行 編集
プログラミング言語としての Lean は、関数などの式を部分的に実行して評価することが容易にできるように設計されている。#eval というコマンドが存在し，関数などをその場で評価することができる。
def frac (n : Nat) : Nat :=
match n with
| 0 => 1
| n + 1 => (n + 1) * frac n
-- エディタ上でコードを開いているとき
-- `#eval` の上にマウスオーバーすると 120 と表示される
#eval frac 5
証明 編集
Lean ではカリーハワード同型対応を利用して証明を行う。ある命題 P の証明 h は，型 P を持つような項 h : P と同一視される。したがって、Lean を仲介することによって「証明する」ということは、「正確にある型を持つような項を作る」ということに言い換えられる。
これは Lean で簡単な命題の証明項を実際に構成した例である。
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P :=
fun h => { left := h.right, right := h.left }
Lean の機能として、タクティクによって証明項を構成することができる。by キーワードによってタクティクモードに入ることができる。タクティクモードの中では、「現在利用できる仮定や命題」「今示すべきこと」が常に infoview に表示され、対話的に証明を書くことができる。
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
-- P ∧ Q と仮定する
intro h
-- Q ∧ P を示すには Q と P をそれぞれ示せばよい
constructor
-- Q を示す
case left =>
exact h.right
-- P を示す
case right =>
exact h.left
依存型 編集
Lean は依存型を持つ。つまり、関数 f : A → B があったときに、f による t : A の返り値 f t の型が t に依存していてもよい。このとき f の型を f : (t : A) → B のように表記する。これにより、たとえば全称命題に正しく型を付けることが可能である。
theorem one_add : ∀ n, n + 1 ≥ 1 := by simp_arith
/-
one_add 1 : 1 + 1 ≥ 1
-/
#check one_add 1
/-
one_add 3 : 3 + 1 ≥ 1
-/
#check one_add 3
拡張可能性 編集
Lean は強力なメタプログラミング機能を持っており、新しい記法の定義や証明の自動化が行えるようになっている。以下は、二項関係らしい記法をマクロとして定義した例である。ここで詳しくは述べないが、新しいタクティクやコマンドを定義することも可能である。
def modulo (k n m : Int) : Prop := k ∣ (n - m)
-- modulo を二項関係らしく書けるようにする
notation:55 x " ≃ " y " mod " k => modulo k x y
#check (1 ≃ 6 mod 5)
自動証明 編集
Lean は対話的に証明を書くことをサポートするだけでなく、タクティクによる自動証明機能も提供する。以下は複雑な命題に見えるが、たった一つのタクティクで証明が終了する例である。
example (a₁ a₂ a₃ : Nat) : 3 ∣ a₁ + 10 * a₂ + 100 * a₃ ↔ 3 ∣ a₁ + a₂ + a₃ := by
omega
脚注 編集
- ^ “Lean Prover About Page”. 2023年7月7日閲覧。
- ^ “leanprover/lean2”. GitHub. 2024年4月27日閲覧。
- ^ “leanprover/hott3”. GitHub. 2024年4月27日閲覧。
- ^ “Releases/v3.0.0”. GitHub. 2024年4月27日閲覧。
- ^ “Release v4.0.0-m1 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ “The Lean Mathematical Library”. mathlib community. 2024年3月25日閲覧。
- ^ “Mathlib porting status”. 2024年3月25日閲覧。
- ^ “Mission - Lean FRO”. Lean FRO. 2024年3月28日閲覧。
- ^ “Release v4.0.0 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ “What is the Xena project?”. Kevin Buzzard. 2024年4月27日閲覧。
- ^ “Completion of the Liquid Tensor Experiment”. leanprover community. 2024年4月10日閲覧。
- ^ “@tao@mathstodon.xyz”. mathstodon.xyz. 2024年4月10日閲覧。
関連項目 編集
外部リンク 編集
- Lean Website Lean の公式サイト。
- Lean 4 Web Lean のオンラインエディタ。
- Reservoir Lean のパッケージレジストリ。パッケージをインデックスするだけでなく、ビルドとテストも行う。
- vscode-lean4 VSCode に Lean 言語のサポートを追加する拡張機能。Unicode 記号をサポートしていて、
×に対する\timesのようなLaTeXに似たシーケンスを使用して入力ができるようにする。