Lean

https://lean-lang.org/

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

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

インストール

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

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

Lean InfoView

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

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

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

やること

関数を定義する

def

定理を証明する

theorem

評価する

#eval

型

Prop

命題