Lean

https://lean-lang.org/

証明支援系です。leanを用いて我々は定理とその証明を書くことができます。

Leanは「証明が正しいかどうかを判定する」こと、「どうすれば正しくなるかを提示する」ことで、証明の手助けを行います。

インストール

Leanをインストールする

https://lean-lang.org/install/

1. VSCode の拡張機能「Lean 4」をインストールする
2. 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
3. プロジェクトが作られる。必要に応じて色々インストールされる。

プロジェクトに Mathlib を導入する

https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

lake exe cache get　してビルド済みファイルをダウンロードしておきましょう。 その後 lean build を実行しておきましょう。

Lean InfoView

これを確認しながら、"Goals accomplished!" を見ることが目標のようです。

.lean ファイルを開くと自動で開かれる。

または、Lean 4 のメニューから Toggle InfoView を選択して開く。

やること

関数を定義する

def

定理を証明する

theorem

証明する（名前なし）

example

評価する

#eval

型

Prop

命題

証明する

構文

:= by

証明を開始します

定理や仮定を使う

rw [h]

h を使ってゴールを書き換えます

intro h

前件(A→B においては A)を h という名前で導入します。

名前は何でもよく、前から順番に導入されるらしい。

exact h

先ほど導入したh: Aを除去して、A→B を導きます。

構成的証明

exists A

∃を示すのに、これを満たすAを具体的に指定します

リンク集

Lean by Example